Require Import Reals.
Require Import RIneq.

Axiom Rle_Rmult_plus_distr:forall a b c d e f g h:R,(a<=b)%R->(c<=d)%R->(e<=f)%R->(g<=h)%R->
                           (a*c+e*g<=b*d+f*h)%R.

Theorem Rle_lt_or_eq : forall n m : R, (n <= m)%R -> (n < m)%R \/ n = m.
Proof.
induction 1; auto with arith.
Qed. 

Lemma imp_not_eq : forall a b : nat, a < b \/ a > b -> a <> b.
intros.
auto with *.
Qed.

Lemma eq_INR : forall n m : nat, n = m -> INR n = INR m.
intros.
rewrite H.
auto with *.
Qed.

Lemma Rplus_eq:forall a b c d:R,a=c->b=d->(a+b=c+d)%R.
intros.
rewrite H;rewrite H0.
auto with * .
Qed.

Lemma neq0_sup0:forall r:R, (0<=r)%R->(r<>0)%R->(0<r)%R. 
intros.
generalize (Rtotal_order R0 r).
intro.
elim H1.
auto.
intro.
elim H2.
intro heq;rewrite <-heq in H0;intuition.
intro.
assert (~ (r<0)%R).
apply Rle_not_lt.
auto.
intuition.
Qed.

Lemma not_0_Rlt_0 : forall n : nat, n <> 0 -> (0 < INR n)%R.
intros.
assert (INR n <> 0%R).
auto with *.
auto with *.
Qed.

Lemma O_div_elt : forall a : R, a <> 0%R -> (0 / a)%R = 0%R.
intros.
replace (0 / a)%R with (0 * / a)%R.
apply Rmult_0_l.
auto with *.
Qed.



Lemma Rdiv_Rle :
 forall a b c : R, (0 < c)%R -> (a <= b)%R -> (a / c <= b / c)%R.
intros.
case H0.
intros.
constructor 1.
unfold Rdiv in |- *.
rewrite Rmult_comm.
replace (b * / c)%R with (/ c * b)%R.
apply Rmult_lt_compat_l with (r := (/ c)%R).
apply Rinv_0_lt_compat.
exact H.
exact H1.
apply Rmult_comm.
intros.
constructor 2.
rewrite H1.
reflexivity.
Qed. 


Lemma Rdiv_id : forall a : R, a <> 0%R -> (a / a)%R = 1%R.
unfold Rdiv in |- *. 
intros.
rewrite Rmult_comm.
apply Rinv_l.
exact H.
Qed.

Lemma INR_neq_lt_0 : forall n : nat, INR n <> 0%R -> (0 < INR n)%R.
intros n.
case n.
simpl in |- *.
intros.
absurd (0%R = 0%R).
exact H.
reflexivity.
intros.
apply lt_INR_0.
intuition.
Qed.

Lemma INR_lt_neq_0:forall n : nat, (0 < INR n)%R -> INR n <> 0%R.
intros n.
case n.
simpl in |- *.
intros.
absurd (0<0)%R.
auto with real.
exact H.
intros.
apply not_O_INR.
generalize O_S.
intro.
intuition.
Qed.

Lemma div_simpl :
 forall a b c : R, b <> 0%R -> c <> 0%R -> (a / c / (b / c))%R = (a / b)%R.
intros.
unfold Rdiv in |- *.
replace (/ (b * / c))%R with (/ b * / / c)%R.
transitivity (a * (/ c * (/ b * / / c)))%R.
auto with real.
replace (/ c * (/ b * / / c))%R with (/ c * / b * / / c)%R.
replace (/ c * / b)%R with (/ b * / c)%R.
replace (/ b * / c * / / c)%R with (/ b * (/ c * / / c))%R.
replace (/ c * / / c)%R with 1%R.
auto with real.
auto with real.
auto with real.
auto with real.
auto with real.
symmetry  in |- *.
apply Rinv_mult_distr.
exact H.
apply Rinv_neq_0_compat.
exact H0.
Qed. 

Lemma Rle_div_1 : forall x y : R, (0 < y)%R -> (x <= y)%R -> (x / y <= 1)%R.
unfold Rdiv in |- *.
intros.
replace 1%R with (y * / y)%R.
apply Rmult_le_compat_r.
auto with real.
exact H0.
auto with real.
Qed.

Lemma Rle_0_ :
 forall a b c : R,
 (0 <= a)%R -> (0 <= c)%R -> (0 < b)%R -> (0 <= a / b * c)%R.
intros.
assert (0 < / b)%R.
apply Rinv_0_lt_compat; auto.
replace (a / b)%R with (a * / b)%R.
rewrite Rmult_comm with (r1 := (a * / b)%R).
rewrite <- Rmult_assoc.
assert (0 * 0 <= c * a * / b)%R.
apply
 Rmult_le_compat
  with (r1 := 0%R) (r2 := (c * a)%R) (r3 := 0%R) (r4 := (/ b)%R); 
 auto with *.
assert (0 * 0 <= c * a)%R.
apply Rmult_le_compat with (r1 := 0%R) (r2 := c) (r3 := 0%R) (r4 := a);
 auto with *.
rewrite Rmult_0_l in H3.
try exact H3.
rewrite Rmult_0_l in H3.
try exact H3.
auto with *.
Qed.


Lemma Rmult_ass : forall a b c : R, (a * b * c)%R = (b * a * c)%R.
intros.
rewrite Rmult_assoc.
rewrite Rmult_comm with (r1 := b).
rewrite <- Rmult_assoc.
rewrite Rmult_comm.
auto with *.
Qed.

Lemma Rge_inv_le :
 forall a b : R, (0 < a)%R -> (0 < b)%R -> (a >= b)%R -> (/ a <= / b)%R.
intros.
assert (b <= a)%R.
apply Rge_le.
auto with *.
assert (b * / b <= a * / b)%R.
apply Rmult_le_compat.
auto with *.
assert (0 < / b)%R.
apply Rinv_0_lt_compat.
auto with *.
auto with *.
auto with *.
auto with *.
rewrite Rmult_comm in H3.
rewrite Rinv_l in H3.
rewrite <- Rinv_r_simpl_m with (r1 := a) (r2 := (/ b)%R).
rewrite <- Rmult_1_l with (r := (/ a)%R).
apply Rmult_le_compat; auto with *.
auto with *.
auto with *.
Qed.

Lemma Rge_1_min : forall a b : R, (a <= b)%R -> (1 - a >= 1 - b)%R.
intros.
unfold Rminus in |- *.
apply Rplus_ge_compat_l.
apply Ropp_le_ge_contravar.
auto with *.
Qed.


Lemma Rlt_0 : forall a b : R, (a / b)%R <> 0%R -> b <> 0%R -> a <> 0%R.
intros.
assert ((a / b)%R = (a * / b)%R).
auto with *.
rewrite H1 in H.
auto with *.
Qed.

Lemma Rdiv_Rmult : forall a b : R, (a / b)%R = (a * / b)%R.
intros.
auto with *.
Qed.

Lemma Rplus_mult : forall a b c : R, (a * b + c * b)%R = ((a + c) * b)%R.
intros.
rewrite Rmult_comm.
rewrite Rmult_comm with (r1 := c).
rewrite Rmult_comm with (r1 := (a + c)%R).
rewrite <- Rmult_plus_distr_l.
auto with *.
Qed.

Lemma Rmult_eq : forall a b c : R, b <> 0%R -> (a / b)%R = (c / b)%R -> a = c.
intros.
rewrite Rdiv_Rmult in H0.
rewrite Rdiv_Rmult in H0.
rewrite Rmult_comm in H0.
rewrite Rmult_comm with (r1 := c) in H0.
apply Rmult_eq_reg_l with (r := (/ b)%R).
auto with *.
auto with *.
Qed.



Lemma Rdiv_Rdiv :
 forall a b c : R, (0 < b)%R -> (0 < c)%R -> (a / b / (c / b))%R = (a / c)%R.
intros.
replace (a / b)%R with (a * / b)%R.
replace (c / b)%R with (c * / b)%R.
replace (a * / b / (c * / b))%R with (a * / b * / (c * / b))%R.
rewrite Rinv_mult_distr.
 rewrite Rinv_involutive.
rewrite Rmult_comm with (r1 := (/ c)%R).
rewrite Rmult_comm with (r2 := (b * / c)%R).
apply Rinv_mult_simpl with (r1 := b) (r2 := c) (r3 := a).
apply Rgt_not_eq.
auto with *.
apply Rgt_not_eq.
auto with *.
apply Rgt_not_eq.
auto with *.
assert (0 < / b)%R.
apply Rinv_0_lt_compat.
auto with *.
apply Rgt_not_eq.
auto with *.
auto with *.
auto with *.
auto with *.
Qed.

Lemma Rle_0 : forall a b : R, (0 <= a)%R -> (0 < b)%R -> (0 <= a / b)%R.
intros.
assert (0 < / b)%R.
apply Rinv_0_lt_compat; auto.
replace (a / b)%R with (a * / b)%R.
assert (0 * 0 <= a * / b)%R.
apply Rmult_le_compat with (r1 := 0%R) (r2 := a) (r3 := 0%R) (r4 := (/ b)%R);
 auto with *.
rewrite Rmult_0_l in H2.
try exact H2.
auto with *.
Qed.
 
Lemma Rle_0_l :
 forall (a : nat) (b : R), a <= 0 -> (0 < b)%R -> (INR a / b <= 0)%R.
intros.
assert (0 < / b)%R.
apply Rinv_0_lt_compat; auto.
replace (INR a / b)%R with (INR a * / b)%R.
assert (INR a * / b <= 0 * / b)%R.
apply Rmult_le_compat_r.
apply Rlt_le.
try exact H1.
replace 0%R with (INR 0).
apply le_INR.
try exact H.
auto with *.
rewrite Rmult_0_l in H2.
auto with *.
auto with *.
Qed.
 
Lemma Rmult_plus_min_distr :
 forall a b c d : R, ((a + b - c) * d)%R = (a * d + b * d - c * d)%R.
intros.
rewrite Rmult_comm.
rewrite Rmult_minus_distr_l.
rewrite Rmult_plus_distr_l.
rewrite Rmult_comm.
rewrite Rmult_comm with (r1 := d) (r2 := b).
rewrite Rmult_comm with (r1 := d) (r2 := c).
auto with *.
Qed.
 
Lemma Rdiv_distr :
 forall b c d e : nat,
 e <= c + d ->
 (INR (c + d - e) / INR b)%R =
 (INR c / INR b + INR d / INR b - INR e / INR b)%R.
intros.
rewrite minus_INR.
rewrite plus_INR.
replace ((INR c + INR d - INR e) / INR b)%R with
 ((INR c + INR d - INR e) * / INR b)%R.
replace (INR c / INR b)%R with (INR c * / INR b)%R.
replace (INR d / INR b)%R with (INR d * / INR b)%R.
replace (INR e / INR b)%R with (INR e * / INR b)%R.
apply Rmult_plus_min_distr.
auto with *.
auto with *.
auto with *.
auto with *.
auto with *.
Qed.
 
Lemma Rplus_0 : forall a : R, (0 + a)%R = a.
intros.
assert ((a + 0)%R = a).
auto with *.
auto with *.
Qed.
 
Lemma Rplus_Rmin_0 :
 forall a b c : R, (a + b - 0 + (0 + c))%R = (a + b + c)%R.
intros.
rewrite Rplus_0.
rewrite Rminus_0_r.
auto.
Qed.
 
Lemma Rplus_ass : forall a b : R, (a + b)%R = (b + a)%R.
intros.
auto with *.
Qed.
 
Lemma Rplus_ass_n : forall a b c : R, (a + b + c)%R = (c + b + a)%R.
intros.
rewrite Rplus_ass.
rewrite Rplus_ass with (a := a) (b := b).
auto with *.
Qed.
 
Lemma Rle_mult :
 forall (a b c e : R) (t u : nat),
 (a <= e)%R ->
 (b <= e * INR t)%R ->
 (c <= e * INR u)%R -> (a + b + c <= e * INR (u + (t + 1)))%R.
intros.
replace (e * INR (u + (t + 1)))%R with (e * (1 + (INR t + INR u)))%R.
rewrite Rmult_plus_distr_l.
rewrite Rmult_plus_distr_l.
assert ((e * 1)%R = e).
apply Rmult_1_r.
rewrite <- H2 in H.
replace (a + b + c)%R with (a + (b + c))%R.
apply Rplus_le_compat; auto.
apply Rplus_le_compat; auto.
auto with *.
rewrite Rmult_plus_distr_l.
rewrite Rmult_plus_distr_l.
replace (e * INR (u + (t + 1)))%R with (e * (INR u + (INR t + 1)))%R.
rewrite Rmult_plus_distr_l.
rewrite Rmult_plus_distr_l.
replace (e * 1 + (e * INR t + e * INR u))%R with
 (e * 1 + e * INR t + e * INR u)%R.
replace (e * INR u + (e * INR t + e * 1))%R with
 (e * INR u + e * INR t + e * 1)%R.
apply Rplus_ass_n.
auto with *.
auto with *.
rewrite plus_INR.
rewrite plus_INR.
auto with *.
Qed.
 
Lemma Rle_Rmult :
 forall a b e d : R, (a <= e)%R -> (b <= e * d)%R -> (a + b <= e * (d + 1))%R.
intros.
assert ((e * 1)%R = e).
apply Rmult_1_r.
rewrite <- H1 in H.
rewrite Rmult_plus_distr_l.
rewrite Rplus_ass with (a := (e * d)%R) (b := (e * 1)%R).
apply Rplus_le_compat; auto.
Qed.
 
Lemma Rle_Rmult_ :
 forall a b e d t : R,
 (a <= e * t)%R -> (b <= e * d)%R -> (a + b <= e * (d + t))%R.
intros.
rewrite Rmult_plus_distr_l.
rewrite Rplus_ass with (a := (e * d)%R) (b := (e * t)%R).
apply Rplus_le_compat; auto.
Qed.
 
Lemma Rmin_0 : forall a b : R, (a + b - 0)%R = (a + b)%R.
intros.
rewrite Rminus_0_r.
auto with *.
Qed.
 
Lemma Rle_trans_div :
 forall a b c d : R,
 (0 < c)%R -> (a <= b / c)%R -> (b <= d)%R -> (a <= d / c)%R.
intros.
assert (b / c <= d / c)%R.
replace (b / c)%R with (b * / c)%R.
replace (d / c)%R with (d * / c)%R.
apply Rmult_le_compat_r.
assert (0 < / c)%R.
auto with *.
apply Rlt_le; auto.
try exact H1.
auto with *.
auto with *.
apply Rle_trans with (r2 := (b / c)%R); auto.
Qed.
 
Lemma Rle_0_div_mult :
 forall a b c : R,
 (0 <= a)%R -> (0 < b)%R -> (0 <= c)%R -> (0 <= a / b * c)%R.
intros.
assert (0 <= a / b)%R.
apply Rle_0; auto.
apply Rmult_le_pos; auto.
Qed.
 
Lemma Rle_div :
 forall (a b : nat) (d : R),
 a <= b -> (0 < d)%R -> (INR a / d <= INR b / d)%R.
intros.
assert (INR a <= INR b)%R.
apply le_INR; auto with *.
replace (INR a / d)%R with (INR a * / d)%R.
replace (INR b / d)%R with (INR b * / d)%R.
apply Rmult_le_compat; auto with *.
auto with *.
auto with *.
Qed.
Lemma Rle__div_trans :
 forall a b c d : R,
 (0 <= a)%R -> (0 < d)%R -> (a <= b)%R -> (b <= c)%R -> (a / d <= c / d)%R.
intros.
assert (a <= c)%R.
apply Rle_trans with (r2 := b).
auto with *.
auto with *.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
apply Rmult_le_compat; auto with *.
Qed.



Lemma Rdiv_mult_simpl :
 forall a c d : R,
 (c / d)%R <> 0%R -> (a / d * (c / d) / (c / d))%R = (a / d)%R.
intros.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_assoc.
rewrite Rmult_comm with (r1 := (c * / d)%R).
rewrite Rinv_l.
auto with *.
auto with *.
Qed.



Lemma _1_min_mult: forall a b c : R,~b=0%R ->(Rmult (Rdiv (1-a) b) c)=(Rminus (Rdiv c  b) (Rdiv (a*c) b))%R.
intros.
rewrite Rdiv_Rmult.
rewrite Rmult_comm with (r2:=(Rinv b)).
rewrite Rmult_minus_distr_l.
rewrite Rmult_1_r.
rewrite Rmult_comm with (r2:=c).
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
ring.
Qed.

Lemma one_min_mult:forall a b : R,(Rmult (1-a) b)=(Rminus b (Rmult a b))%R.
intros.
ring.
Qed.



Lemma Rdiv_Rplus_eq :
 forall a c b : R, c <> 0%R -> ((a + b) / c)%R = (a / c + b / c)%R.
intros.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rmult_comm.
rewrite Rmult_plus_distr_l.
rewrite Rmult_comm.
auto with *.
Qed.

Lemma Rdiv_Rmult_simpl_ :
 forall a c d : R, a <> 0%R -> d <> 0%R -> (a * c / (d * a))%R = (c / d)%R.
intros.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rinv_mult_distr.
rewrite <- Rmult_assoc.
replace (a * c * / d * / a)%R with (a * / a * c * / d)%R.
rewrite Rinv_r.
rewrite Rmult_1_l.
auto with *.
auto with *.
rewrite Rmult_assoc.
rewrite Rmult_comm with (r2 := (c * / d)%R).
rewrite <- Rmult_assoc.
rewrite Rmult_comm with (r1 := (c * / d)%R).
rewrite <- Rmult_assoc.
auto with *.
auto with *.
auto with *.
Qed.
Lemma mult_Rinv_simpl :
 forall c d : R, c <> 0%R -> d <> 0%R -> (/ (c * d) * c)%R = (/ d)%R.
intros.
rewrite Rinv_mult_distr.
rewrite Rmult_comm.
rewrite <- Rmult_assoc.
rewrite Rmult_comm with (r1 := c).
rewrite Rinv_l.
auto with *.
auto with *.
auto with *.
auto with *.
Qed.

Lemma Rmult_lt : forall a b : R, (0 < b)%R -> (a < b)%R -> (a * / b < 1)%R.
intros.
rewrite Rmult_comm.
replace 1%R with (/ b * b)%R.
apply Rmult_lt_compat_l.
auto with *.
auto with *.
auto with *.
Qed.


 
Lemma Rle_plus_div :
 forall (a b c : nat) (d : R),
 a <= b + c -> (0 < d)%R -> (INR a / d <= INR (b + c) / d)%R.
intros.
apply Rle_div.
auto with *.
auto with *.
Qed.
 
Lemma Rplus_distr_div :
 forall (a b : nat) (d : R),
 (0 < d)%R -> (INR (a + b) / d)%R = (INR a / d + INR b / d)%R.
intros.
rewrite plus_INR.
replace ((INR a + INR b) / d)%R with ((INR a + INR b) * / d)%R.
replace (INR a / d)%R with (INR a * / d)%R.
replace (INR b / d)%R with (INR b * / d)%R.
apply Rmult_plus_distr_r; auto with *.
auto with *.
auto with *.
auto with *.
Qed.
 
Lemma Rminus_distr_div :
 forall (a b : nat) (c : R),
 b <= a -> (INR (a - b) / c)%R = (INR a / c - INR b / c)%R.
intros.
rewrite minus_INR.
replace ((INR a - INR b) / c)%R with ((INR a - INR b) * / c)%R.
replace (INR a / c)%R with (INR a * / c)%R.
replace (INR b / c)%R with (INR b * / c)%R.
rewrite Rmult_comm.
rewrite Rmult_comm with (r1 := INR a).
rewrite Rmult_comm with (r1 := INR b).
apply Rmult_minus_distr_l.
auto with *.
auto with *.
auto with *.
auto with *.
Qed.

Lemma S_Rmin : forall b : nat, (INR (S b) - 1)%R = INR b.
intros.
assert (S b = b + 1).
auto with *.
rewrite H.
rewrite plus_INR.
simpl in |- *.
unfold Rminus in |- *.
rewrite Rplus_assoc.
rewrite Rplus_comm with (r1 := 1%R).
rewrite Rplus_opp_l.
auto with *.
Qed.

Lemma Rle_ge_div :
 forall a b c d : R,
 (0 <= a)%R ->
 (0 < b)%R -> (0 < d)%R -> (a <= c)%R -> (b >= d)%R -> (a / b <= c / d)%R.
intros.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
apply Rmult_le_compat.
auto with *.
auto with *.
auto with *.
apply Rge_inv_le.
auto with *.
auto with *.
auto with *.
Qed.

Lemma Rlt_mult : forall a b : R, (0 < b)%R -> (a / b < 1)%R -> (a < b)%R.
intros a b.
rewrite Rdiv_Rmult.
intros.
replace a with (b * (a * / b))%R.
rewrite <- Rmult_1_r.
apply Rmult_lt_compat_l; auto with *.
rewrite Rmult_comm.
rewrite Rmult_assoc.
rewrite Rinv_l.
auto with *.
auto with *.
Qed.


Lemma Rle_min_plus : forall a c : R, (0 <= c)%R -> (a - c <= a + c)%R.
intros.
apply Rle_trans with (r2 := a).
unfold Rminus in |- *.
rewrite <- Rplus_0_r.
apply Rplus_le_compat.
auto with *.
auto with *.
rewrite <- Rplus_0_r with (r := a).
apply Rplus_le_compat.
auto with *.
auto with *.
Qed.


Lemma Rmult_eq_0 : forall a b : R, (a * b)%R = 0%R -> a = 0%R \/ b = 0%R.
intros.
apply Rmult_integral.
auto with *.
Qed.


Lemma Req_0 : forall a b : R, b <> 0%R -> (a / b)%R = 0%R -> a = 0%R.
intros.
rewrite Rdiv_Rmult in H0.
assert (a = 0%R \/ (/ b)%R = 0%R).
apply Rmult_eq_0.
auto with *.
assert ((/ b)%R <> 0%R).
apply Rinv_neq_0_compat; auto with *.
intuition.
Qed.

Lemma not_Req_0 : forall a b : R, b <> 0%R -> a <> 0%R -> (a / b)%R <> 0%R.
intros.
assert ((a / b)%R = 0%R -> a = 0%R).
intro.
apply Req_0 with (b := b); auto.
intuition.
Qed.



Lemma Rewr_Rdiv_mult :
 forall a b c x y : nat,
 INR x <> 0%R ->
 INR y <> 0%R ->
 a = b * c ->
 (INR a / INR (x * y))%R =
 (INR (b * y) / INR (x * y) * (INR (c * x) / INR (x * y)))%R.
intros.
rewrite H1.
rewrite mult_INR.
rewrite mult_INR.
rewrite mult_INR.
rewrite mult_INR.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rinv_mult_distr.
rewrite Rmult_comm with (r1 := (/ INR x)%R).
pattern x at 1 2 in |- *.
rewrite Rmult_comm with (r2 := (/ INR x)%R).
replace
 (INR b * INR y * (/ INR y * / INR x) * (INR c * INR x * (/ INR x * / INR y)))%R
 with
 (INR b * (INR y * / INR y) * / INR x * (INR c * (INR x * / INR x) * / INR y))%R.
rewrite Rinv_r.
rewrite Rinv_r.
rewrite Rmult_1_r.
rewrite Rmult_1_r.
rewrite Rmult_comm with (r1 := (/ INR y)%R).
replace (INR b * / INR x * (INR c * / INR y))%R with
 (INR b * (/ INR x * INR c) * / INR y)%R.
pattern c at 1 in |- *.
rewrite Rmult_comm with (r2 := INR c).
rewrite <- Rmult_assoc.
rewrite <- Rmult_assoc.
auto with *.
rewrite <- Rmult_assoc.
auto with *.
auto with *.
auto with *.
rewrite <- Rmult_assoc.
rewrite <- Rmult_assoc.
rewrite <- Rmult_assoc.
rewrite <- Rmult_assoc.
rewrite <- Rmult_assoc.
rewrite <- Rmult_assoc.
rewrite <- Rmult_assoc.
rewrite <- Rmult_assoc.
auto with *.
auto with *.
auto with *.
Qed.

Lemma Rle_plus_plus_div :
 forall a b b' c d : R,
 (0 <= d)%R ->
 (0 <= / c)%R -> (b <= b')%R -> (a + b / c * d <= a + b' / c * d)%R.
intros.
apply Rplus_le_compat.
auto with *.
apply Rmult_le_compat_r.
auto with *.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
apply Rmult_le_compat_r.
auto with *.
auto with *.
Qed.


Lemma Rdiv_Rmult_simpl :
 forall a b c d : R,
 0%R <> d -> 0%R <> c -> (a + b / c)%R = (a + b / (d * c) * d)%R.
intros.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rinv_mult_distr.
rewrite <- Rmult_assoc.
replace (a + b * / d * / c * d)%R with (a + b * (/ d * / c) * d)%R.
rewrite Rmult_comm with (r1 := (/ d)%R).
rewrite <- Rmult_assoc.
replace (a + b * / c * / d * d)%R with (a + b * / c * (/ d * d))%R.
rewrite Rinv_l.

rewrite Rmult_1_r.
auto with *.
auto with *.
auto with *.
rewrite <- Rmult_assoc.
auto with *.
auto with *.
auto with *.
Qed.

Lemma eq_Rmult : forall a b c d : R, a = b -> c = d -> (a * c)%R = (b * d)%R.
intros.
rewrite H.
rewrite H0.
reflexivity.
Qed.



Lemma Rle_not_Rlt : forall a : R, (0 <= a)%R -> 0%R <> a -> (0 < a)%R.
intros.
unfold Rle in H.
intuition.
Qed.


Lemma S_not_0 : forall n2 : nat, (INR (S n2) + 1)%R <> 0%R.
red in |- *; intros.
assert (S n2 + 1 <> 0).
auto with *.
unfold not in H0; apply H0.
apply INR_eq.
generalize H.
replace 0%R with (INR 0).
rewrite plus_INR.
auto with *.
auto with *.
Qed.



Lemma Rle_inv_monotony_r :
 forall x y a : R, (0 < a)%R -> (x <= y)%R -> (x / a <= y / a)%R.
intros.
unfold Rdiv in |- *.
apply Rmult_le_compat_r.
apply Rlt_le.
apply Rinv_0_lt_compat.
apply H.
apply H0.
Qed.

Lemma Rle_inv_monotony :
 forall x y a : R,
 (0 < y)%R -> (y <= x)%R -> (0 <= a)%R -> (a / x <= a / y)%R.
intros.
unfold Rdiv in |- *.
apply Rmult_le_compat_l.
apply H1.
apply Rle_Rinv.
apply H.
eapply Rlt_le_trans.
apply H.
apply H0.
apply H0.
Qed.

Lemma Rlt_minus_r : forall x y : R, (x < y)%R -> (0 < y - x)%R.
intros.
unfold Rminus in |- *.
replace 0%R with (x + - x)%R.
auto with real.
auto with real.
Qed.

Lemma Rle_Ropp1_compatibility :
 forall x y a : R, (x <= y)%R -> (a - y <= a - x)%R.
intros.
unfold Rminus in |- *.
auto with real.
Qed.

Lemma lem16 :
 forall a b c : R,
 b <> 0%R -> b <> c -> (a / b / (1 - c / b))%R = (a / (b - c))%R.
intros.
unfold Rdiv in |- *.
replace (a * / b * / (1 - c * / b))%R with (a * (/ b * / (1 - c * / b)))%R.
replace (/ b * / (1 - c * / b))%R with (/ (b * 1 - b * c * / b))%R.
replace (b * 1)%R with b.
replace (b * c * / b)%R with c.
reflexivity.
symmetry  in |- *.
apply Rinv_r_simpl_m.
apply H.
auto with real.
replace (b * c * / b)%R with (b * (c * / b))%R.
replace (b * 1 - b * (c * / b))%R with (b * (1 - c * / b))%R.
apply Rinv_mult_distr.
apply H.
unfold not in |- *.
intros.
absurd (b = c).
exact H0.
replace b with (b * 1)%R.
replace c with (b * (c * / b))%R.
apply Rmult_eq_compat_l.
replace (c * / b)%R with (c * / b + 0)%R.
replace 1%R with (c * / b + (1 - c * / b))%R.
apply Rplus_eq_compat_l.
exact H1.
auto with real.
auto with real.
replace (b * (c * / b))%R with (b * c * / b)%R.
auto with real.
auto with real.
auto with real.
unfold Rminus in |- *.
replace (- (b * (c * / b)))%R with (b * - (c * / b))%R.
auto with real.
apply Ropp_mult_distr_r_reverse.
auto with real.
auto with real.
Qed.

Lemma Rlt_monotony_contra1 :
 forall x y : R, (0 < y)%R -> (x / y < 1)%R -> (x < y)%R.
unfold Rdiv in |- *.
intros.
apply Rmult_lt_reg_l with (r := (/ y)%R).
apply Rinv_0_lt_compat.
exact H.
replace (/ y * x)%R with (x * / y)%R.
replace (/ y * y)%R with 1%R.
exact H0.
auto with real.
auto with real.
Qed.

Lemma plus_Rplus_div :
 forall (x y : nat) (z : R), (INR (x + y) / z)%R = (INR x / z + INR y / z)%R.
intros.
unfold Rdiv in |- *.
transitivity ((INR x + INR y) * / z)%R.
replace (INR (x + y) * / z)%R with (/ z * INR (x + y))%R.
replace ((INR x + INR y) * / z)%R with (/ z * (INR x + INR y))%R.
auto with real.
auto with real.
auto with real.
apply Rmult_plus_distr_r.
Qed.


Lemma Rplus_Rdiv : forall a b c : R, (a / b + c / b)%R = ((a + c) / b)%R.
intros.
unfold Rdiv in |- *.
rewrite Rmult_plus_distr_r.
auto with *.
Qed.


Lemma Rplus_le2 :
 forall a b c d : R, (a <= c)%R -> (b <= d)%R -> (a + b <= c + d)%R.
intros.
apply Rplus_le_compat.
exact H.
exact H0.
Qed.

Lemma Rle_lt_inv : forall x y : R, (0 <= x)%R -> (0 < y)%R -> (0 <= x / y)%R.
intros.
unfold Rdiv in |- *.
apply Rmult_le_pos.
exact H.
auto with real.
Qed.

Lemma Rdiv_mult_simp:forall a b c:R,   b <> 0%R->  c <> 0%R->(a/(b*c)*b)%R=(a/c)%R.
intros.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
rewrite Rinv_mult_distr.
ring.
rewrite Rinv_l.
ring.
auto.
auto.
auto.
Qed.

Lemma le_plus_0:forall a b c d e:R,(0<=a)%R->(0<=b)%R->(0<=d)%R->(0<c)%R->(0<e)%R->(0<=(a+b/c+d/e)%R)%R.
intros.
rewrite Rplus_assoc.
rewrite <-Rplus_0_r with R0.
apply Rplus_le_compat.
auto.
rewrite <-Rplus_0_r with R0.
apply Rplus_le_compat.
apply Rle_0;auto.
apply Rle_0;auto.
Qed.

Lemma plus_minus_assoc:forall a b c:R,(a+b-c=a+(b-c))%R.
intros.
ring.
Qed.


Lemma div_mult_simpl:forall a b c:R,b<>0%R->((a/b)*(b/c)=a/c)%R.
intros.
rewrite Rdiv_Rmult.
rewrite Rdiv_Rmult.
replace (a * / b * (b * / c))%R with (a * (/ b * b )* / c)%R.
rewrite Rinv_l.
rewrite Rdiv_Rmult.
ring.
auto.
ring.
Qed.

Lemma div_lt_0:forall a b:nat,a<>0->b<>0->(0 <(INR a) /(INR b))%R.
intros.
assert ((Rinv (INR b))<>0)%R.
apply Rinv_neq_0_compat ;auto.
intro.
apply H0.
auto with * . 
assert (0<INR a)%R.
apply not_0_Rlt_0;auto.
assert (0<(/ INR b))%R. 
auto with * .
rewrite Rdiv_Rmult.
apply Rmult_lt_0_compat;auto.
Qed.