# Library Coqtail.mytheories.myReals.MyRIneq

Require Import RIneq MyNeq.
Require Import Rfunctions.

Require Import Fourier.

Open Scope R_scope.

Implicit Type r : R.

Require Setoid.

Add Parametric Relation : R Rle
reflexivity proved by Rle_refl
transitivity proved by Rle_trans as Rle.

Add Parametric Relation : R Rlt
transitivity proved by Rlt_trans as Rlt.

Lemma Rabs_opp1 : p, Rabs ((- 1) ^ p) = 1.
Proof.
intros ; rewrite <- RPow_abs, Rabs_Ropp, Rabs_R1 ; apply pow1.
Qed.

Lemma Rdiv_eq_0_inv : a b, a / b = 0 → b 0 → a = 0.
Proof.
intros a b Hab Hb ; destruct (Rmult_integral _ _ Hab) as [Ha | Hb'].
apply Ha.
assert (Hb'' : / b 0) by (apply Rinv_neq_0_compat ; assumption).
apply False_ind, Hb'', Hb'.
Qed.

Lemma Rabs_Rdiv : a b, b 0 → Rabs a / Rabs b = Rabs (a / b).
Proof.
intros a b b_neq ; unfold Rdiv ; rewrite Rabs_mult, Rabs_Rinv.
reflexivity.
assumption.
Qed.

Lemma Rplus_pos_lt : x h, 0 < hx < x + h.
Proof.
intros ; fourier.
Qed.

Lemma Rminus_pos_lt : x h, 0 < hx - h < x.
Proof.
intros ; fourier.
Qed.

Lemma Rplus_pos_neq : x h, 0 < hx x + h.
Proof.
intros ; apply Rlt_not_eq, Rplus_pos_lt ; assumption.
Qed.

Lemma Rlt_minus_sort : a b c, a < c + ba - c < b.
Proof.
intros ; fourier.
Qed.

Lemma Rlt_minus_sort2 : a b c, a - c < b- c < b - a.
Proof.
intros ; fourier.
Qed.

Lemma Rminus_lt_compat_l : a b c, a < b + ca - b < c.
intros ; fourier.
Qed.

Lemma Rminus_lt_compat_r : a b c, a + c < ba < b - c.
Proof.
intros ; fourier.
Qed.

Lemma Rminus_lt_compat_l_rev : a b c, a - b < ca < b + c.
Proof.
intros ; fourier.
Qed.

Lemma Rminus_le_compat_l : a b c, a b + ca - b c.
intros ; fourier.
Qed.

Lemma Rminus_le_compat_r : a b c, a + c ba b - c.
Proof.
intros ; fourier.
Qed.

Lemma Rminus_le_compat_l_rev : a b c, a - b ca b + c.
Proof.
intros ; fourier.
Qed.

Lemma Rinv_lt_contravar_rev : x y, 0 < x → 0 < y/x < /yy < x.
Proof.
intros x y x_pos y_pos Hxy ; rewrite <- (Rinv_involutive x), <- (Rinv_involutive y) ;
try (apply Rgt_not_eq ; assumption).
apply Rinv_lt_contravar ; [| assumption] ; apply Rmult_lt_0_compat ;
apply Rinv_0_lt_compat ; assumption.
Qed.

Lemma Ropp_Rdiv_compat_l : a b, b 0 → - a / b = - (a / b).
Proof.
intros ; field ; assumption.
Qed.

Lemma Rle_Rminus : a b, a b → 0 b - a.
Proof.
intros ; fourier.
Qed.

Lemma Rle_Rminus_rev : a b, 0 b - aa b.
Proof.
intros ; fourier.
Qed.

Lemma Rlt_Rminus_rev : a b, 0 < b - aa < b.
Proof.
intros ; fourier.
Qed.

Lemma Rmult_Rinv_lt_compat_r : a b c, 0 < aa × b < cb < c × / a.
Proof.
intros a b c a_pos Habc ; apply Rle_lt_trans with (a × b × / a).
right ; field ; apply Rgt_not_eq ; assumption.
apply Rmult_lt_compat_r ; [apply Rinv_0_lt_compat |] ; assumption.
Qed.

Lemma Rmult_Rinv_lt_compat_r_rev : a b c, 0 < ab < c × / aa × b < c.
Proof.
intros a b c a_pos Habc ; apply Rlt_le_trans with (a × (c × / a)).
apply Rmult_lt_compat_l ; assumption.
right ; field ; apply Rgt_not_eq ; assumption.
Qed.

Lemma Rmult_Rinv_lt_compat_l : a b c, 0 < ca < b × ca × / c < b.
Proof.
intros a b c a_pos Habc ; apply Rlt_le_trans with (b × c × / c).
apply Rmult_lt_compat_r ; [apply Rinv_0_lt_compat |] ; assumption.
right ; field ; apply Rgt_not_eq ; assumption.
Qed.

Lemma Rmult_Rinv_lt_compat_l_rev : a b c, 0 < ca × / c < ba < b × c.
Proof.
intros a b c a_pos Habc ; apply Rle_lt_trans with (a × / c × c).
right ; field ; apply Rgt_not_eq ; assumption.
apply Rmult_lt_compat_r ; assumption.
Qed.

Lemma Rlt_minus_swap: x y z, x - y < zx - z < y.
Proof.
intros ; fourier.
Qed.

Lemma Rdiv_0_l: r, 0 / r = 0.
Proof.
intro r ; unfold Rdiv ; apply Rmult_0_l.
Qed.

Lemma Rmin_opp_opp_Rmax : r1 r2, Rmin (-r1) (-r2) = - (Rmax r1 r2).
Proof.
intros r1 r2 ; unfold Rmin, Rmax ; destruct (Rle_dec r1 r2) as [L1 | R1] ;
destruct (Rle_dec (-r1) (-r2)) as [L2 | R2].
assert (H := Ropp_le_cancel _ _ L2) ; apply Ropp_eq_compat ;
apply Rle_antisym ; assumption.
reflexivity.
reflexivity.
assert (H1 := Rnot_le_lt _ _ R1).
assert (H2 := Ropp_lt_cancel _ _ (Rnot_le_lt _ _ R2)).
apply False_ind ; apply Rlt_irrefl with r1 ; apply Rlt_trans with r2 ;
assumption.
Qed.

Lemma Rmax_opp_opp_Rmin : r1 r2, Rmax (-r1) (-r2) = - (Rmin r1 r2).
Proof.
intros r1 r2.
replace (Rmin r1 r2) with (Rmin (--r1) (--r2)) by (rewrite Ropp_involutive ; intuition).
rewrite Rmin_opp_opp_Rmax ; rewrite Ropp_involutive ; reflexivity.
Qed.

Lemma Rmin_diag : r, Rmin r r = r.
Proof.
intro r ; unfold Rmin ; destruct (Rle_dec r r) ; auto.
Qed.

Lemma Rmin_eq_l : r1 r2, r1 r2Rmin r1 r2 = r1.
Proof.
intros r1 r2 r1_le_r2 ; unfold Rmin ; destruct (Rle_dec r1 r2).
reflexivity.
Qed.

Lemma Rmin_eq_r : r1 r2, r1 r2Rmin r2 r1 = r1.
Proof.
intros r1 r2 r1_le_r2 ; rewrite Rmin_comm ;
apply Rmin_eq_l ; assumption.
Qed.

Lemma Rmax_diag : r, Rmax r r = r.
Proof.
intro r ; unfold Rmax ; destruct (Rle_dec r r) ; auto.
Qed.

Lemma Rmax_eq_l : r1 r2, r2 r1Rmax r1 r2 = r1.
Proof.
intros r1 r2 r1_le_r2 ; unfold Rmax ; destruct (Rle_dec r1 r2).
destruct r.
apply False_ind ; apply Rlt_irrefl with r2 ;
apply Rle_lt_trans with r1 ; assumption.
symmetry ; trivial.
reflexivity.
Qed.

Lemma Rmax_eq_r : r1 r2, r2 r1Rmax r2 r1 = r1.
Proof.
intros r1 r2 r1_le_r2 ; rewrite Rmax_comm ; apply Rmax_eq_l ;
assumption.
Qed.

Lemma Rmin_pos : x y, 0 x → 0 y → 0 Rmin x y.
Proof.
intros x y x_pos y_pos ; unfold Rmin ;
destruct (Rle_dec x y) ; assumption.
Qed.

Lemma Rmin_pos_lt : x y, 0 < x → 0 < y → 0 < Rmin x y.
Proof.
intros x y x_pos y_pos ; unfold Rmin ;
destruct (Rle_dec x y) ; assumption.
Qed.

Lemma Rmax_pos_l : x y, 0 x → 0 Rmax x y.
Proof.
intros x y x_pos ; unfold Rmax ; destruct (Rle_dec x y) ;
[apply Rle_trans with x |] ; assumption.
Qed.

Lemma Rmax_pos_r : x y, 0 y → 0 Rmax x y.
Proof.
intros ; rewrite Rmax_comm ; apply Rmax_pos_l ; auto.
Qed.

Lemma Rmax_pos_lt_l : x y, 0 < x → 0 < Rmax x y.
Proof.
intros x y x_pos ; unfold Rmax ; destruct (Rle_dec x y) ;
[apply Rlt_le_trans with x |] ; assumption.
Qed.

Lemma Rmax_pos_lt_r : x y, 0 < y → 0 < Rmax x y.
Proof.
intros ; rewrite Rmax_comm ; apply Rmax_pos_lt_l ; auto.
Qed.

Lemma Rabs_eq_compat : r1 r2, r1 = r2Rabs r1 = Rabs r2.
Proof.
intros ; subst ; reflexivity.
Qed.

Lemma Rabs_le : r, - Rabs r r.
Proof.
intros r ; unfold Rabs ; destruct (Rcase_abs r) ;
[| apply Rle_trans with 0] ; intuition.
Qed.

Lemma Req_dec : r1 r2, {r1 = r2} + {r1 r2}.
Proof.
intros r1 r2.
destruct (total_order_T r1 r2) as [[Hlt|Heq]|Hgt].
right; intro Hn; apply (Rlt_irrefl r2);
rewrite Hn in Hlt; assumption.
left; assumption.
right; intros Hn; apply (Rlt_irrefl r2);
rewrite Hn in Hgt; assumption.
Qed.

Lemma Req_or_neq : r, {r = 0} + {r 0}.
Proof.
intros r; exact (Req_dec r 0).
Qed.

Lemma Rneq_le_lt: x y, x yx yx < y.
Proof.
intros x y Hneq [] ; intuition.
Qed.

Lemma Rneq_lt_or_gt: x y, x y{x < y} + {y < x}.
Proof.
intros x y x_neq_y.
destruct (Rle_lt_dec x y).
left ; apply Rneq_le_lt ; assumption.
right ; assumption.
Qed.

Lemma Rminus_opp : x y, x - - y = x + y.
Proof.
intros ; unfold Rminus ; rewrite Ropp_involutive ;
reflexivity.
Qed.

Lemma Rplus_eq_compat_r : r r1 r2, r1 = r2r1 + r = r2 + r.
Proof.
intros ; subst ; reflexivity.
Qed.

Lemma Rplus_eq_compat : r1 r2 r3 r4, r1 = r3r2 = r4r1 + r2 = r3 + r4.
Proof.
intros ; subst ; reflexivity.
Qed.

Lemma Rmult_eq_compat_r : r1 r2 r, r1 = r2r1 × r = r2 × r.
Proof.
intros ; subst ; reflexivity.
Qed.

Lemma Rminus_eq_compat : r1 r2 r3 r4, r1 = r3r2 = r4
r1 - r2 = r3 - r4.
Proof.
intros ; subst ; reflexivity.
Qed.

Lemma Rmult_eq_compat : r1 r2 r3 r4, r1 = r3r2 = r4
r1 × r2 = r3 × r4.
Proof.
intros ; subst ; reflexivity.
Qed.

Lemma Rpow_eq_compat : a b d, a = ba ^ d = b ^ d.
Proof.
intros ; subst ; reflexivity.
Qed.

Lemma Rdiv_eq_compat: x y z, x = yx / z = y / z.
Proof.
intros ; subst ; reflexivity.
Qed.

Lemma Rplus_lt_simpl_l : r1 r2, 0 < r2r1 < r1 + r2.
Proof.
intros ; fourier.
Qed.

Lemma Rplus_lt_simpl_r : r1 r2, 0 < r1r2 < r1 + r2.
Proof.
intros ; fourier.
Qed.

Lemma Rplus_le_simpl_l : r1 r2, 0 r2r1 r1 + r2.
Proof.
intros ; fourier.
Qed.

Lemma Rplus_le_simpl_r : r1 r2, 0 r1r2 r1 + r2.
Proof.
intros ; fourier.
Qed.

Lemma Rmax_lt_lt_lt : x y z, Rmax x y < z x < z y < z.
Proof.
intros x y z ; unfold Rmax ; destruct (Rle_dec x y) ; split ; intuition.
apply Rle_lt_trans with y ; assumption.
transitivity x ; [apply Rnot_le_lt |] ; assumption.
Qed.

Lemma Rmax_le_le_le : x y z, Rmax x y z x z y z.
Proof.
intros x y z ; unfold Rmax ; destruct (Rle_dec x y) ; split ; intuition.
transitivity y ; assumption.
transitivity x ; [left ; apply Rnot_le_lt |] ; assumption.
Qed.

Lemma Rmin_lt_lt_lt : x y z, z < Rmin x y z < x z < y.
Proof.
intros x y z ; unfold Rmin ; destruct (Rle_dec x y) ; split ; intuition.
apply Rlt_le_trans with x ; assumption.
transitivity y ; [| apply Rnot_le_lt] ; assumption.
Qed.

Lemma Rmin_le_le_le : x y z, z Rmin x y z x z y.
Proof.
intros x y z ; unfold Rmin ; destruct (Rle_dec x y) ; split ; intuition.
transitivity x ; assumption.
transitivity y ; [| left ; apply Rnot_le_lt] ; assumption.
Qed.

Lemma Rle_neq_lt : x y, x yx yx < y.
Proof.
intros m n Hyp1 Hyp2 ; case Hyp1.
intuition.
intro Hfalse ; apply False_ind ; apply Hyp2 ; exact Hfalse.
Qed.

Lemma Rlt_1_mult_inv : x y, 0 < y
y < x → 1 < x × / y.
intros x y y_pos y_lb ; apply Rle_lt_trans with (y × / y).
right ; symmetry ; apply Rinv_r ; apply Rgt_not_eq ; assumption.
apply Rmult_lt_compat_r ; [apply Rinv_0_lt_compat |] ; assumption.
Qed.

Lemma Rabs_pos_lt_contravar : x, 0 < Rabs xx 0.
Proof.
intros x Hpos ; destruct (Req_or_neq x) as [Heq | Hneq].
rewrite Heq, Rabs_R0 in Hpos ; destruct (Rlt_irrefl _ Hpos).
assumption.
Qed.

Lemma Rmult_Rinv_le_compat : x y z, 0 < y
x y × zx × / y z.
Proof.
intros x y z y_pos Hle.
apply Rle_trans with (y × z × / y).
apply Rmult_le_compat_r.
left ; apply Rinv_0_lt_compat ; assumption.
assumption.
right ; field ; apply Rgt_not_eq ; assumption.
Qed.

Lemma Rmult_Rinv_le_compat_contravar : x y z, 0 < y
x × / y zx y × z.
Proof.
intros x y z y_pos Hle.
apply Rle_trans with (y × (x × / y)).
right ; field ; apply Rgt_not_eq ; assumption.
apply Rmult_le_compat_l ; [left |] ; assumption.
Qed.

Lemma Rmult_minus_distr_r: x y z,
(x - y) × z = x × z - y × z.
Proof.
intros ; ring.
Qed.

Lemma Rneq_lt_gt_dec : a b, a b{ a < b } + { b < a }.
Proof.
intros a b ab_neq ; destruct (Rlt_le_dec a b).
left ; assumption.
right ; apply Rle_neq_lt ; [| symmetry] ; assumption.
Qed.

Lemma Rminus_lt_compat_r_rev : a b c : R, a - c < ba < b + c.
intros ; fourier.
Qed.

Lemma Rminus_lt_compat : a b c, a < ba - c < b - c.
Proof.
intros ; fourier.
Qed.

Lemma Rminus_lt_compat_rev : a b c, a - c < b - ca < b.
Proof.
intros ; fourier.
Qed.

Lemma Rmult_Rdiv_lt_compat_l_rev: a b c : R, 0 < ca < b / cc × a < b.
Proof.
intros ; apply Rlt_le_trans with (c × (b / c))%R.
apply Rmult_lt_compat_l ; assumption.
right ; field ; apply Rgt_not_eq ; assumption.
Qed.

Lemma Rlt_minus_sort3: a b c : R, a - b < - ca + c < b.
Proof.
intros ; fourier.
Qed.

Lemma dist_2_pos : lb ub, lb < ub → (0 < (ub - lb) / 2)%R.
Proof.
intros lb ub lt ; apply Rlt_mult_inv_pos ; fourier.
Qed.