Library Coq.fourier.Fourier_util
Lemmas used by the tactic Fourier
Open Scope R_scope.
Lemma Rfourier_lt :
forall x1 y1 a:
R,
x1 < y1 -> 0
< a -> a * x1 < a * y1.
Lemma Rfourier_le :
forall x1 y1 a:
R,
x1 <= y1 -> 0
< a -> a * x1 <= a * y1.
Lemma Rfourier_lt_lt :
forall x1 y1 x2 y2 a:
R,
x1 < y1 -> x2 < y2 -> 0
< a -> x1 + a * x2 < y1 + a * y2.
Lemma Rfourier_lt_le :
forall x1 y1 x2 y2 a:
R,
x1 < y1 -> x2 <= y2 -> 0
< a -> x1 + a * x2 < y1 + a * y2.
Lemma Rfourier_le_lt :
forall x1 y1 x2 y2 a:
R,
x1 <= y1 -> x2 < y2 -> 0
< a -> x1 + a * x2 < y1 + a * y2.
Lemma Rfourier_le_le :
forall x1 y1 x2 y2 a:
R,
x1 <= y1 -> x2 <= y2 -> 0
< a -> x1 + a * x2 <= y1 + a * y2.
Lemma Rlt_zero_pos_plus1 :
forall x:
R, 0
< x -> 0
< 1
+ x.
Lemma Rlt_mult_inv_pos :
forall x y:
R, 0
< x -> 0
< y -> 0
< x * / y.
Lemma Rlt_zero_1 : 0
< 1.
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.
Lemma Rle_zero_1 : 0
<= 1.
Lemma Rle_not_lt :
forall n d:
R, 0
<= n * / d -> ~ 0
< - n * / d.
Lemma Rnot_lt0 :
forall x:
R,
~ 0
< 0
* x.
Lemma Rlt_not_le_frac_opp :
forall n d:
R, 0
< n * / d -> ~ 0
<= - n * / d.
Lemma Rnot_lt_lt :
forall x y:
R,
~ 0
< y - x -> ~ x < y.
Lemma Rnot_le_le :
forall x y:
R,
~ 0
<= y - x -> ~ x <= y.
Lemma Rfourier_gt_to_lt :
forall x y:
R,
y > x -> x < y.
Lemma Rfourier_ge_to_le :
forall x y:
R,
y >= x -> x <= y.
Lemma Rfourier_eqLR_to_le :
forall x y:
R,
x = y -> x <= y.
Lemma Rfourier_eqRL_to_le :
forall x y:
R,
y = x -> x <= y.
Lemma Rfourier_not_ge_lt :
forall x y:
R,
(x >= y -> False) -> x < y.
Lemma Rfourier_not_gt_le :
forall x y:
R,
(x > y -> False) -> x <= y.
Lemma Rfourier_not_le_gt :
forall x y:
R,
(x <= y -> False) -> x > y.
Lemma Rfourier_not_lt_ge :
forall x y:
R,
(x < y -> False) -> x >= y.