Library Coq.micromega.Fourier_util
Require
Export
Rbase
.
Require
Import
Lra
.
Local Open
Scope
R_scope
.
Lemma
Rlt_mult_inv_pos
:
forall
x
y
:
R
, 0
<
x
->
0
<
y
->
0
<
x
*
/
y
.
Lemma
Rlt_zero_pos_plus1
:
forall
x
:
R
, 0
<
x
->
0
<
1
+
x
.
Lemma
Rle_zero_pos_plus1
:
forall
x
:
R
, 0
<=
x
->
0
<=
1
+
x
.
Lemma
Rle_mult_inv_pos
:
forall
x
y
:
R
, 0
<=
x
->
0
<
y
->
0
<=
x
*
/
y
.