Library Coq.fourier.Fourier_util

Require Export Rbase.

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.