theories/Reals

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@511 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 3746 insertions, 0 deletions

diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
new file mode 100644
index 000000000..8d5971a4e
--- /dev/null
+++ b/theories/Reals/R_Ifp.v
@@ -0,0 +1,529 @@
+
+(* $Id$ *)
+
+(*********************************************************)
+(* Complements for the reals.Integer and fractional part *)
+(*                                                       *)
+(*********************************************************)
+
+Require Export Rbase.
+Require Omega.
+
+(*********************************************************)
+(*       Fractional part                                 *)
+(*********************************************************)
+
+(**********)
+Definition Int_part:R->Z:=[r:R](`(up r)-1`).
+
+(**********)
+Definition frac_part:R->R:=[r:R](Rminus r (IZR (Int_part r))).
+
+(**********)
+Lemma tech_up:(r:R)(z:Z)(Rlt r (IZR z))->(Rle (IZR z) (Rplus r R1))->
+  z=(up r).
+Intros;Generalize (archimed r);Intro;Elim H1;Intros;Clear H1;
+ Unfold Rgt in H2;Unfold Rminus in H3;
+Generalize (Rle_compatibility r (Rplus (IZR (up r)) 
+ (Ropp r)) R1 H3);Intro;Clear H3;
+ Rewrite (Rplus_sym (IZR (up r)) (Ropp r)) in H1;
+ Rewrite <-(Rplus_assoc r (Ropp r) (IZR (up r))) in H1;
+ Rewrite (Rplus_Ropp_r r) in H1;Elim (Rplus_ne (IZR (up r)));Intros a b;
+ Rewrite b in H1;Clear a b;Apply (single_z_r_R1 r z (up r));Auto with zarith real.
+Save.
+
+(**********)
+Lemma up_tech:(r:R)(z:Z)(Rle (IZR z) r)->(Rlt r (IZR `z+1`))->
+  `z+1`=(up r).
+Intros;Generalize (Rle_compatibility R1 (IZR z) r H);Intro;Clear H;
+ Rewrite (Rplus_sym R1 (IZR z)) in H1;Rewrite (Rplus_sym R1 r) in H1;
+ Cut (R1==(IZR `1`));Auto with zarith real.
+Intro;Generalize H1;Pattern 1 R1;Rewrite H;Intro;Clear H H1;
+ Rewrite <-(plus_IZR z `1`) in H2;Apply (tech_up r `z+1`);Auto with zarith real.
+Save.
+
+(**********)
+Lemma fp_R0:(frac_part R0)==R0.
+Unfold frac_part; Unfold Int_part; Unfold up; Elim (archimed R0);
+ Intros; Unfold Rminus;
+ Elim (Rplus_ne (Ropp (IZR `(up R0)-1`))); Intros a b;
+ Rewrite b;Clear a b;Rewrite <- Z_R_minus;Cut (up R0)=`1`.
+Intro;Rewrite H1;
+ Rewrite (eq_Rminus (IZR `1`) (IZR `1`) (refl_eqT R (IZR `1`)));
+ Apply Ropp_O. 
+Elim (archimed R0);Intros;Clear H2;Unfold Rgt in H1;
+ Rewrite (minus_R0 (IZR (up R0))) in H0;
+ Generalize (lt_O_IZR (up R0) H1);Intro;Clear H1;
+ Generalize (le_IZR_R1 (up R0) H0);Intro;Clear H H0;Omega.
+Save.
+
+(**********)
+Lemma for_base_fp:(r:R)(Rgt (Rminus (IZR (up r)) r) R0)/\ 
+                       (Rle (Rminus (IZR (up r)) r) R1).
+Intro; Split;
+ Cut (Rgt (IZR (up r)) r)/\(Rle (Rminus (IZR (up r)) r) R1).
+Intro; Elim H; Intros.
+Apply (Rgt_minus (IZR (up r)) r H0).
+Apply archimed.
+Intro; Elim H; Intros.
+Exact H1.
+Apply archimed.
+Save.
+
+(**********)
+Lemma base_fp:(r:R)(Rge (frac_part r) R0)/\(Rlt (frac_part r) R1).
+Intro; Unfold frac_part; Unfold Int_part; Split.
+     (*sup a O*)
+Cut (Rge (Rminus r (IZR (up r))) (Ropp R1)).
+Rewrite <- Z_R_minus;Simpl;Intro; Unfold Rminus;
+ Rewrite Ropp_distr1;Rewrite <-Rplus_assoc;
+ Fold (Rminus r (IZR (up r)));
+ Fold (Rminus (Rminus r (IZR (up r))) (Ropp R1));
+ Apply Rge_minus;Auto with zarith real.
+Rewrite <- Ropp_distr2;Apply Rle_Ropp;Elim (for_base_fp r); Auto with zarith real.
+    (*inf a 1*) 
+Cut (Rlt (Rminus r (IZR (up r))) R0).
+Rewrite <- Z_R_minus; Simpl;Intro; Unfold Rminus;
+ Rewrite Ropp_distr1;Rewrite <-Rplus_assoc;
+ Fold (Rminus r (IZR (up r)));Rewrite Ropp_Ropp;
+ Elim (Rplus_ne R1);Intros a b;Pattern 2 R1;Rewrite <-a;Clear a b;
+ Rewrite (Rplus_sym  (Rminus r (IZR (up r))) R1);
+ Apply Rlt_compatibility;Auto with zarith real.
+Elim (for_base_fp r);Intros;Rewrite <-Ropp_O;
+ Rewrite<-Ropp_distr2;Apply Rgt_Ropp;Auto with zarith real.
+Save.
+
+(*********************************************************)
+(*       Properties                                      *)
+(*********************************************************)
+
+(**********)
+Lemma base_Int_part:(r:R)(Rle (IZR (Int_part r)) r)/\
+                    (Rgt (Rminus (IZR (Int_part r)) r) (Ropp R1)). 
+Intro;Unfold Int_part;Elim (archimed r);Intros;Unfold up.
+Split;Rewrite <- (Z_R_minus (up r) `1`);Simpl.
+Generalize (Rle_minus (Rminus (IZR (up r)) r) R1 H0);Intro;
+ Unfold Rminus in H1;
+ Rewrite (Rplus_assoc (IZR (up r)) (Ropp r) (Ropp R1)) in 
+ H1;Rewrite (Rplus_sym (Ropp r) (Ropp R1)) in H1;
+ Rewrite <-(Rplus_assoc (IZR (up r)) (Ropp R1) (Ropp r)) in
+ H1;Fold (Rminus (IZR (up r)) R1) in H1;
+ Fold (Rminus (Rminus (IZR (up r)) R1) r) in H1;
+ Apply Rminus_le;Auto with zarith real.
+Generalize (Rgt_plus_plus_r (Ropp R1) (IZR (up r)) r H);Intro;
+ Rewrite (Rplus_sym (Ropp R1) (IZR (up r))) in H1;
+ Generalize (Rgt_plus_plus_r (Ropp r) 
+   (Rplus (IZR (up r)) (Ropp R1)) (Rplus (Ropp R1) r) H1);
+ Intro;Clear H H0 H1;
+ Rewrite (Rplus_sym (Ropp r) (Rplus (IZR (up r)) (Ropp R1)))
+ in H2;Fold (Rminus (IZR (up r)) R1) in H2;
+ Fold (Rminus (Rminus (IZR (up r)) R1) r) in H2;
+ Rewrite (Rplus_sym (Ropp r) (Rplus (Ropp R1) r)) in H2;
+ Rewrite (Rplus_assoc (Ropp R1) r (Ropp r)) in H2;
+ Rewrite (Rplus_Ropp_r r) in H2;Elim (Rplus_ne (Ropp R1));Intros a b;
+ Rewrite a in H2;Clear a b;Auto with zarith real.  
+Save.
+
+(**********)
+Lemma fp_nat:(r:R)(frac_part r)==R0->(Ex [c:Z](r==(IZR c))).
+Unfold frac_part;Intros;Split with (Int_part r);Apply Rminus_eq; Auto with zarith real.
+Save.
+
+(**********)
+Lemma R0_fp_O:(r:R)~R0==(frac_part r)->~R0==r.
+Red;Intros;Rewrite <- H0 in H;Generalize fp_R0;Intro;Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rminus_Int_part1:(r1,r2:R)(Rge (frac_part r1) (frac_part r2))->
+  (Int_part (Rminus r1 r2))=(Zminus (Int_part r1) (Int_part r2)).
+Intros;Elim (base_fp r1);Elim (base_fp r2);Intros;
+ Generalize (Rle_sym2 R0 (frac_part r2) H0);Intro;Clear H0;
+ Generalize (Rle_Ropp R0 (frac_part r2) H4);Intro;Clear H4;
+ Rewrite (Ropp_O) in H0;
+ Generalize (Rle_sym2 (Ropp (frac_part r2)) R0 H0);Intro;Clear H0;
+ Generalize (Rle_sym2 R0 (frac_part r1) H2);Intro;Clear H2;
+ Generalize (Rlt_Ropp (frac_part r2) R1 H1);Intro;Clear H1;
+ Unfold Rgt in H2;
+ Generalize (sum_inequa_Rle_lt R0 (frac_part r1) R1 (Ropp R1)
+   (Ropp (frac_part r2)) R0 H0 H3 H2 H4);Intro;Elim H1;Intros;
+ Clear H1;Elim (Rplus_ne R1);Intros a b;Rewrite a in H6;Clear a b H5;
+ Generalize (Rge_minus (frac_part r1) (frac_part r2) H);Intro;Clear H;
+ Fold (Rminus (frac_part r1) (frac_part r2)) in H6;
+ Generalize (Rle_sym2 R0 (Rminus (frac_part r1) (frac_part r2)) H1);
+ Intro;Clear H1 H3 H4 H0 H2;Unfold frac_part in H6 H;
+ Unfold Rminus in H6 H;
+ Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H;
+ Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H;
+ Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
+  (Rplus (Ropp r2) (IZR (Int_part r2)))) in H;
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
+  (IZR (Int_part r2))) in H;
+ Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H;
+ Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
+  (IZR (Int_part r2))) in H;
+ Rewrite <-(Rplus_assoc r1 (Ropp r2) 
+  (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H;
+ Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H;
+ Fold (Rminus r1 r2) in H;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) 
+ in H;Generalize (Rle_compatibility 
+  (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) R0 
+  (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) H);Intro;
+ Clear H;Rewrite (Rplus_sym (Rminus r1 r2)
+  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H0;
+ Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H0;
+ Unfold Rminus in H0;Fold (Rminus r1 r2) in H0;
+ Rewrite (Rplus_assoc (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))) 
+  (Rplus (IZR (Int_part r2)) (Ropp (IZR (Int_part r1))))) in H0;
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r2))) (IZR (Int_part r2))
+  (Ropp (IZR (Int_part r1)))) in H0;Rewrite (Rplus_Ropp_l (IZR (Int_part r2))) in 
+ H0;Elim (Rplus_ne (Ropp (IZR (Int_part r1))));Intros a b;Rewrite b in H0;
+ Clear a b;
+ Elim (Rplus_ne (Rplus (IZR (Int_part r1)) (Ropp (IZR (Int_part r2)))));
+ Intros a b;Rewrite a in H0;Clear a b;Rewrite (Rplus_Ropp_r (IZR (Int_part r1))) 
+ in H0;Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H0;
+ Clear a b;Fold (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) in H0;
+ Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H6;
+ Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H6;
+ Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
+  (Rplus (Ropp r2) (IZR (Int_part r2)))) in H6;
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
+  (IZR (Int_part r2))) in H6;
+ Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H6;
+ Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
+  (IZR (Int_part r2))) in H6;
+ Rewrite <-(Rplus_assoc r1 (Ropp r2) 
+  (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H6;
+ Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H6;
+ Fold (Rminus r1 r2) in H6;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) 
+ in H6;Generalize (Rlt_compatibility 
+   (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) 
+   (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) R1 H6);
+ Intro;Clear H6;
+ Rewrite (Rplus_sym (Rminus r1 r2)
+  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H;
+ Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H;
+ Rewrite <-(Ropp_distr2 (IZR (Int_part r1)) (IZR (Int_part r2))) in H;
+ Rewrite (Rplus_Ropp_r (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H;
+ Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H;Clear a b;
+ Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
+ Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H;
+ Cut R1==(IZR `1`);Auto with zarith real.
+Intro;Rewrite H1 in H;Clear H1;
+ Rewrite <-(plus_IZR `(Int_part r1)-(Int_part r2)` `1`) in H;
+ Generalize (up_tech  (Rminus r1 r2) `(Int_part r1)-(Int_part r2)`
+  H0 H);Intros;Clear H H0;Unfold 1 Int_part;Omega.
+Save.
+
+(**********)
+Lemma Rminus_Int_part2:(r1,r2:R)(Rlt (frac_part r1) (frac_part r2))->
+  (Int_part (Rminus r1 r2))=(Zminus (Zminus (Int_part r1) (Int_part r2)) `1`).
+Intros;Elim (base_fp r1);Elim (base_fp r2);Intros;
+ Generalize (Rle_sym2 R0 (frac_part r2) H0);Intro;Clear H0;
+ Generalize (Rle_Ropp R0 (frac_part r2) H4);Intro;Clear H4;
+ Rewrite (Ropp_O) in H0;
+ Generalize (Rle_sym2 (Ropp (frac_part r2)) R0 H0);Intro;Clear H0;
+ Generalize (Rle_sym2 R0 (frac_part r1) H2);Intro;Clear H2;
+ Generalize (Rlt_Ropp (frac_part r2) R1 H1);Intro;Clear H1;
+ Unfold Rgt in H2;
+ Generalize (sum_inequa_Rle_lt R0 (frac_part r1) R1 (Ropp R1)
+   (Ropp (frac_part r2)) R0 H0 H3 H2 H4);Intro;Elim H1;Intros;
+ Clear H1;Elim (Rplus_ne (Ropp R1));Intros a b;Rewrite b in H5;
+ Clear a b H6;Generalize (Rlt_minus (frac_part r1) (frac_part r2) H);
+ Intro;Clear H;Fold (Rminus (frac_part r1) (frac_part r2)) in H5;
+ Clear H3 H4 H0 H2;Unfold frac_part in H5 H1;
+ Unfold Rminus in H5 H1;
+ Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H5;
+ Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H5;
+ Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
+  (Rplus (Ropp r2) (IZR (Int_part r2)))) in H5;
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
+  (IZR (Int_part r2))) in H5;
+ Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H5;
+ Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
+  (IZR (Int_part r2))) in H5;
+ Rewrite <-(Rplus_assoc r1 (Ropp r2) 
+  (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H5;
+ Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H5;
+ Fold (Rminus r1 r2) in H5;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) 
+ in H5;Generalize (Rlt_compatibility 
+  (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) (Ropp R1) 
+  (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) H5);
+ Intro;Clear H5;Rewrite (Rplus_sym (Rminus r1 r2)
+  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H;
+ Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H;
+ Unfold Rminus in H;Fold (Rminus r1 r2) in H;
+ Rewrite (Rplus_assoc (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))) 
+  (Rplus (IZR (Int_part r2)) (Ropp (IZR (Int_part r1))))) in H;
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r2))) (IZR (Int_part r2))
+  (Ropp (IZR (Int_part r1)))) in H;Rewrite (Rplus_Ropp_l (IZR (Int_part r2))) in 
+ H;Elim (Rplus_ne (Ropp (IZR (Int_part r1))));Intros a b;Rewrite b in H;
+ Clear a b;Rewrite (Rplus_Ropp_r (IZR (Int_part r1))) in H;
+ Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H;
+ Clear a b;Fold (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) in H;
+ Fold (Rminus (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) R1) in H;
+ Rewrite (Ropp_distr1 r2 (Ropp (IZR (Int_part r2)))) in H1;
+ Rewrite (Ropp_Ropp (IZR (Int_part r2))) in H1;
+ Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
+  (Rplus (Ropp r2) (IZR (Int_part r2)))) in H1;
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
+  (IZR (Int_part r2))) in H1;
+ Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (Ropp r2)) in H1;
+ Rewrite (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
+  (IZR (Int_part r2))) in H1;
+ Rewrite <-(Rplus_assoc r1 (Ropp r2) 
+  (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2)))) in H1;
+ Rewrite (Rplus_sym (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) in H1;
+ Fold (Rminus r1 r2) in H1;Fold (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) 
+ in H1;Generalize (Rlt_compatibility 
+   (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) 
+   (Rplus (Rminus r1 r2) (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) R0 H1);
+ Intro;Clear H1;
+ Rewrite (Rplus_sym (Rminus r1 r2)
+  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1)))) in H0;
+ Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Rminus (IZR (Int_part r2)) (IZR (Int_part r1))) (Rminus r1 r2)) in H0;
+ Rewrite <-(Ropp_distr2 (IZR (Int_part r1)) (IZR (Int_part r2))) in H0;
+ Rewrite (Rplus_Ropp_r (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H0;
+ Elim (Rplus_ne (Rminus r1 r2));Intros a b;Rewrite b in H0;Clear a b;
+ Rewrite <-(Rplus_Ropp_l R1) in H0;
+ Rewrite <-(Rplus_assoc (Rminus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Ropp R1) R1) in H0;
+ Fold (Rminus (Rminus (IZR (Int_part r1)) (IZR (Int_part r2))) R1) in H0;
+ Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
+ Rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H;
+ Cut R1==(IZR `1`);Auto with zarith real.
+Intro;Rewrite H1 in H;Rewrite H1 in H0;Clear H1;
+ Rewrite (Z_R_minus `(Int_part r1)-(Int_part r2)` `1`) in H;
+ Rewrite (Z_R_minus `(Int_part r1)-(Int_part r2)` `1`) in H0;
+ Rewrite <-(plus_IZR `(Int_part r1)-(Int_part r2)-1` `1`) in H0;
+ Generalize (Rlt_le (IZR `(Int_part r1)-(Int_part r2)-1`) (Rminus r1 r2) H);
+ Intro;Clear H;
+ Generalize (up_tech  (Rminus r1 r2) `(Int_part r1)-(Int_part r2)-1`
+  H1 H0);Intros;Clear H0 H1;Unfold 1 Int_part;Omega.
+Save.
+
+(**********)
+Lemma Rminus_fp1:(r1,r2:R)(Rge (frac_part r1) (frac_part r2))->
+  (frac_part (Rminus r1 r2))==(Rminus (frac_part r1) (frac_part r2)).
+Intros;Unfold frac_part;
+ Generalize (Rminus_Int_part1 r1 r2 H);Intro;Rewrite -> H0;
+ Rewrite <- (Z_R_minus (Int_part r1) (Int_part r2));Unfold Rminus;
+ Rewrite -> (Ropp_distr1 (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))));
+ Rewrite -> (Ropp_distr1 r2 (Ropp (IZR (Int_part r2))));
+ Rewrite -> (Ropp_Ropp (IZR (Int_part r2)));
+ Rewrite -> (Rplus_assoc r1 (Ropp r2)
+             (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))));
+ Rewrite -> (Rplus_assoc r1 (Ropp (IZR (Int_part r1)))
+             (Rplus (Ropp r2) (IZR (Int_part r2))));
+ Rewrite <- (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
+             (IZR (Int_part r2)));
+ Rewrite <- (Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
+             (IZR (Int_part r2)));
+ Rewrite -> (Rplus_sym (Ropp r2) (Ropp (IZR (Int_part r1))));Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rminus_fp2:(r1,r2:R)(Rlt (frac_part r1) (frac_part r2))->
+  (frac_part (Rminus r1 r2))==
+  (Rplus (Rminus (frac_part r1) (frac_part r2)) R1).
+Intros;Unfold frac_part;Generalize (Rminus_Int_part2 r1 r2 H);Intro;
+ Rewrite -> H0;
+ Rewrite <- (Z_R_minus (Zminus (Int_part r1) (Int_part r2)) `1`);
+ Rewrite <- (Z_R_minus (Int_part r1) (Int_part r2));Unfold Rminus;
+ Rewrite -> (Ropp_distr1 (Rplus (IZR (Int_part r1)) (Ropp (IZR (Int_part r2))))
+             (Ropp (IZR `1`)));
+ Rewrite -> (Ropp_distr1 r2 (Ropp (IZR (Int_part r2))));
+ Rewrite -> (Ropp_Ropp (IZR `1`));
+ Rewrite -> (Ropp_Ropp (IZR (Int_part r2)));
+ Rewrite -> (Ropp_distr1 (IZR (Int_part r1)));
+ Rewrite -> (Ropp_Ropp (IZR (Int_part r2)));Simpl;
+ Rewrite <- (Rplus_assoc (Rplus r1 (Ropp r2))
+             (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))) R1);
+ Rewrite -> (Rplus_assoc r1 (Ropp r2)
+             (Rplus (Ropp (IZR (Int_part r1))) (IZR (Int_part r2))));
+ Rewrite -> (Rplus_assoc r1 (Ropp (IZR (Int_part r1)))
+             (Rplus (Ropp r2) (IZR (Int_part r2)))); 
+ Rewrite <- (Rplus_assoc (Ropp r2) (Ropp (IZR (Int_part r1)))
+             (IZR (Int_part r2)));
+ Rewrite <- (Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp r2)
+             (IZR (Int_part r2)));
+ Rewrite -> (Rplus_sym (Ropp r2) (Ropp (IZR (Int_part r1))));Auto with zarith real.
+Save.
+
+(**********)
+Lemma plus_Int_part1:(r1,r2:R)(Rge (Rplus (frac_part r1) (frac_part r2)) R1)->
+  (Int_part (Rplus r1 r2))=(Zplus (Zplus (Int_part r1) (Int_part r2)) `1`).
+Intros;
+ Generalize (Rle_sym2 R1 (Rplus (frac_part r1) (frac_part r2)) H);
+ Intro;Clear H;Elim (base_fp r1);Elim (base_fp r2);Intros;Clear H H2;
+ Generalize (Rlt_compatibility (frac_part r2) (frac_part r1) R1 H3);
+ Intro;Clear H3;
+ Generalize (Rlt_compatibility R1 (frac_part r2) R1 H1);Intro;Clear H1;
+ Rewrite (Rplus_sym R1 (frac_part r2)) in H2;
+ Generalize (Rlt_trans (Rplus (frac_part r2) (frac_part r1))
+  (Rplus (frac_part r2) R1) (Rplus R1 R1) H H2);Intro;Clear H H2;
+ Rewrite (Rplus_sym (frac_part r2) (frac_part r1)) in H1;
+ Unfold frac_part in H0 H1;Unfold Rminus in H0 H1;
+ Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
+  (Rplus r2 (Ropp (IZR (Int_part r2))))) in H1;
+ Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H1;
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
+  r2) in H1;
+ Rewrite (Rplus_sym 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H1;
+ Rewrite <-(Rplus_assoc r1 r2 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H1;
+ Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
+ Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
+  (Rplus r2 (Ropp (IZR (Int_part r2))))) in H0;
+ Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H0;
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
+  r2) in H0;
+ Rewrite (Rplus_sym 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H0;
+ Rewrite <-(Rplus_assoc r1 r2 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H0;
+ Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H0;
+ Generalize (Rle_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  R1 (Rplus (Rplus r1 r2)
+           (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) H0);Intro;
+ Clear H0;
+ Generalize (Rlt_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Rplus (Rplus r1 r2)
+   (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) (Rplus R1 R1) H1);
+ Intro;Clear H1;
+ Rewrite (Rplus_sym (Rplus r1 r2) 
+  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H;
+ Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H;
+ Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H;
+ Elim (Rplus_ne (Rplus r1 r2));Intros a b;Rewrite b in H;Clear a b;
+ Rewrite (Rplus_sym (Rplus r1 r2) 
+  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H0;
+ Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H0;
+ Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H0;
+ Elim (Rplus_ne (Rplus r1 r2));Intros a b;Rewrite b in H0;Clear a b;
+ Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) R1 R1) in 
+ H0;Cut R1==(IZR `1`);Auto with zarith real.
+Intro;Rewrite H1 in H0;Rewrite H1 in H;Clear H1;
+ Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H; 
+ Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H0;
+ Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)` `1`) in H;
+ Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)` `1`) in H0;
+ Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)+1` `1`) in H0;
+ Generalize (up_tech (Rplus r1 r2) `(Int_part r1)+(Int_part r2)+1` H H0);Intro;
+ Clear H H0;Unfold 1 Int_part;Omega.
+Save.
+
+(**********)
+Lemma plus_Int_part2:(r1,r2:R)(Rlt (Rplus (frac_part r1) (frac_part r2)) R1)->
+  (Int_part (Rplus r1 r2))=(Zplus (Int_part r1) (Int_part r2)).
+Intros;Elim (base_fp r1);Elim (base_fp r2);Intros;Clear H1 H3;
+ Generalize (Rle_sym2 R0 (frac_part r2) H0);Intro;Clear H0;
+ Generalize (Rle_sym2 R0 (frac_part r1) H2);Intro;Clear H2;
+ Generalize (Rle_compatibility (frac_part r1) R0 (frac_part r2) H1);
+ Intro;Clear H1;Elim (Rplus_ne (frac_part r1));Intros a b;
+ Rewrite a in H2;Clear a b;Generalize (Rle_trans R0 (frac_part r1)
+  (Rplus (frac_part r1) (frac_part r2)) H0 H2);Intro;Clear H0 H2;
+ Unfold frac_part in H H1;Unfold Rminus in H H1;
+ Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
+  (Rplus r2 (Ropp (IZR (Int_part r2))))) in H1;
+ Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H1;
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
+  r2) in H1;
+ Rewrite (Rplus_sym 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H1;
+ Rewrite <-(Rplus_assoc r1 r2 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H1;
+ Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H1;
+ Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
+  (Rplus r2 (Ropp (IZR (Int_part r2))))) in H;
+ Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2)))) in H;
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
+  r2) in H;
+ Rewrite (Rplus_sym 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2) in H;
+ Rewrite <-(Rplus_assoc r1 r2 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2))))) in H;
+ Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2))) in H;
+ Generalize (Rle_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  R0 (Rplus (Rplus r1 r2)
+           (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) H1);Intro;
+ Clear H1;
+ Generalize (Rlt_compatibility (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Rplus (Rplus r1 r2)
+   (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) R1 H);
+ Intro;Clear H;
+ Rewrite (Rplus_sym (Rplus r1 r2) 
+  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H1;
+ Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H1;
+ Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H1;
+ Elim (Rplus_ne (Rplus r1 r2));Intros a b;Rewrite b in H1;Clear a b;
+ Rewrite (Rplus_sym (Rplus r1 r2) 
+  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))) in H0;
+ Rewrite <-(Rplus_assoc (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))
+  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) (Rplus r1 r2)) in H0;
+ Rewrite (Rplus_Ropp_r (Rplus (IZR (Int_part r1)) (IZR (Int_part r2)))) in H0;
+ Elim (Rplus_ne (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))));Intros a b;
+ Rewrite a in H0;Clear a b;Elim (Rplus_ne (Rplus r1 r2));Intros a b;
+ Rewrite b in H0;Clear a b;Cut R1==(IZR `1`);Auto with zarith real.
+Intro;Rewrite H in H1;Clear H;
+ Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H0;
+ Rewrite <-(plus_IZR (Int_part r1) (Int_part r2)) in H1;
+ Rewrite <-(plus_IZR `(Int_part r1)+(Int_part r2)` `1`) in H1;
+ Generalize (up_tech (Rplus r1 r2) `(Int_part r1)+(Int_part r2)` H0 H1);Intro;
+ Clear H0 H1;Unfold 1 Int_part;Omega.
+Save.
+
+(**********)
+Lemma plus_frac_part1:(r1,r2:R)
+  (Rge (Rplus (frac_part r1) (frac_part r2)) R1)->
+                (frac_part (Rplus r1 r2))==
+                (Rminus (Rplus (frac_part r1) (frac_part r2)) R1).
+Intros;Unfold frac_part;
+ Generalize (plus_Int_part1 r1 r2 H);Intro;Rewrite H0;
+ Rewrite (plus_IZR `(Int_part r1)+(Int_part r2)` `1`);
+ Rewrite (plus_IZR (Int_part r1) (Int_part r2));Simpl;Unfold 3 4 Rminus;
+ Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
+  (Rplus r2 (Ropp (IZR (Int_part r2)))));
+ Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2))));
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
+   r2);
+ Rewrite (Rplus_sym 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2);
+ Rewrite <-(Rplus_assoc r1 r2 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))));
+ Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2)));
+ Unfold Rminus;
+ Rewrite (Rplus_assoc (Rplus r1 r2) 
+  (Ropp (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))))
+  (Ropp R1));
+ Rewrite <-(Ropp_distr1 (Rplus (IZR (Int_part r1)) (IZR (Int_part r2))) R1);
+ Trivial with zarith real.
+Save.
+
+(**********)
+Lemma plus_frac_part2:(r1,r2:R)
+  (Rlt (Rplus (frac_part r1) (frac_part r2)) R1)->
+(frac_part (Rplus r1 r2))==(Rplus (frac_part r1) (frac_part r2)).
+Intros;Unfold frac_part;
+ Generalize (plus_Int_part2 r1 r2 H);Intro;Rewrite H0;
+ Rewrite (plus_IZR (Int_part r1) (Int_part r2));Unfold 2 3 Rminus;
+ Rewrite (Rplus_assoc r1 (Ropp (IZR (Int_part r1))) 
+  (Rplus r2 (Ropp (IZR (Int_part r2)))));
+ Rewrite (Rplus_sym r2 (Ropp (IZR (Int_part r2))));
+ Rewrite <-(Rplus_assoc (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))
+  r2);
+ Rewrite (Rplus_sym 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))) r2);
+ Rewrite <-(Rplus_assoc r1 r2 
+  (Rplus (Ropp (IZR (Int_part r1))) (Ropp (IZR (Int_part r2)))));
+ Rewrite <-(Ropp_distr1 (IZR (Int_part r1)) (IZR (Int_part r2)));Unfold Rminus;
+ Trivial with zarith real.
+Save.
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
new file mode 100644
index 000000000..579672866
--- /dev/null
+++ b/theories/Reals/Raxioms.v
@@ -0,0 +1,164 @@
+
+(* $Id$ *)
+
+(*********************************************************)
+(*           Axiomatisation of the classical reals       *)
+(*                                                       *)
+(*********************************************************)
+
+Require Export ZArith.
+Require Export TypeSyntax.
+
+Parameter R:Type.
+Parameter R0:R.
+Parameter R1:R.
+Parameter Rplus:R->R->R.
+Parameter Rmult:R->R->R.
+Parameter Ropp:R->R.
+Parameter Rinv:R->R. 
+Parameter Rlt:R->R->Prop.    
+Parameter up:R->Z.
+(*********************************************************)
+
+(**********)
+Definition Rgt:R->R->Prop:=[r1,r2:R](Rlt r2 r1).
+
+(**********)
+Definition Rle:R->R->Prop:=[r1,r2:R]((Rlt r1 r2)\/(r1==r2)).
+
+(**********)
+Definition Rge:R->R->Prop:=[r1,r2:R]((Rgt r1 r2)\/(r1==r2)).
+
+(**********)
+Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
+
+(*********************************************************)
+(*       Field axioms                                   *)
+(*********************************************************)
+(*********************************************************)
+(*       Addition                                        *)
+(*********************************************************)
+
+(**********)
+Axiom Rplus_sym:(r1,r2:R)((Rplus r1 r2)==(Rplus r2 r1)).
+
+(**********)
+Axiom Rplus_assoc:(r1,r2,r3:R)
+  ((Rplus (Rplus r1 r2) r3)==(Rplus r1 (Rplus r2 r3))).
+
+(**********)
+Axiom Rplus_Ropp_r:(r:R)((Rplus r (Ropp r))==R0).
+Hints Resolve Rplus_Ropp_r : real v62.
+
+(**********)
+Axiom Rplus_ne:(r:R)(((Rplus r R0)==r)/\((Rplus R0 r)==r)).
+Hints Resolve Rplus_ne : real v62.
+
+(***********************************************************)       
+(*        Multiplication                                   *)
+(***********************************************************)
+
+(**********)
+Axiom Rmult_sym:(r1,r2:R)((Rmult r1 r2)==(Rmult r2 r1)).
+Hints Resolve Rmult_sym : real v62. 
+
+(**********)
+Axiom Rmult_assoc:(r1,r2,r3:R)
+  ((Rmult (Rmult r1 r2) r3)==(Rmult r1 (Rmult r2 r3))).
+Hints Resolve Rmult_assoc : real v62.
+
+(**********)
+Axiom Rinv_l:(r:R)(~(r==R0))->((Rmult (Rinv r) r)==R1).
+
+(**********)
+Axiom Rmult_ne:(r:R)(((Rmult r R1)==r)/\((Rmult R1 r)==r)).
+Hints Resolve Rmult_ne : real v62.
+
+(**********)
+Axiom R1_neq_R0:(~R1==R0).
+
+(*********************************************************)
+(*       Distributivity                                  *)
+(*********************************************************)
+
+(**********)
+Axiom Rmult_Rplus_distr:(r1,r2,r3:R)
+  ((Rmult r1 (Rplus r2 r3))==(Rplus (Rmult r1 r2) (Rmult r1 r3))).
+Hints Resolve Rmult_Rplus_distr : real v62.
+
+(*********************************************************)
+(*       Order axioms                                    *)
+(*********************************************************)
+(*********************************************************)
+(*       Total Order                                     *)
+(*********************************************************)
+
+(**********)
+Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT (Rlt r1 r2) (r1==r2)) 
+                                   (Rgt r1 r2)).
+
+(*********************************************************)
+(*       Lower                                           *)
+(*********************************************************)
+
+(**********)
+Axiom Rlt_antisym:(r1,r2:R)(Rlt r1 r2) -> ~(Rlt r2 r1).
+
+(**********)
+Axiom Rlt_trans:(r1,r2,r3:R)
+  (Rlt r1 r2)->(Rlt r2 r3)->(Rlt r1 r3).
+
+(**********)
+Axiom Rlt_compatibility:(r,r1,r2:R)(Rlt r1 r2)->
+      (Rlt (Rplus r r1) (Rplus r r2)).
+
+(**********)
+Axiom Rlt_monotony:(r,r1,r2:R)(Rlt R0 r)->(Rlt r1 r2)->
+      (Rlt (Rmult r r1) (Rmult r r2)).
+
+(**********************************************************) 
+(*       Injection from N to R                            *)
+(**********************************************************)
+
+(**********)
+Fixpoint INR [n:nat]:R:=(Cases n of
+                          O      => R0
+                         |(S O)  => R1 
+                         |(S n)  => (Rplus (INR n) R1)
+                        end).  
+
+(**********************************************************) 
+(*       Injection from Z to R                            *)
+(**********************************************************)
+
+(**********)
+Definition IZR:Z->R:=[z:Z](Cases z of
+                         ZERO      => R0
+                        |(POS n) => (INR (convert n))
+                        |(NEG n) => (Ropp (INR (convert n)))
+                           end).  
+
+(**********************************************************)
+(*       R Archimedian                                    *)
+(**********************************************************)
+
+(**********)
+Axiom archimed:(r:R)(Rgt (IZR (up r)) r)/\
+                    (Rle (Rminus (IZR (up r)) r) R1).
+
+(**********************************************************)
+(*       R Complete                                        *)
+(**********************************************************)
+
+(**********)
+Definition is_upper_bound:=[E:R->Prop][m:R](x:R)(E x)->(Rle x m).
+
+(**********)
+Definition bound:=[E:R->Prop](ExT [m:R](is_upper_bound E m)).
+
+(**********)
+Definition is_lub:=[E:R->Prop][m:R]
+    (is_upper_bound E m)/\(b:R)(is_upper_bound E b)->(Rlt m b).
+
+(**********)
+Axiom complet:(E:R->Prop)((bound E)->(ExT [m:R](is_lub E m))).
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
new file mode 100644
index 000000000..bfbab59bd
--- /dev/null
+++ b/theories/Reals/Rbase.v
@@ -0,0 +1,1142 @@
+
+(* $Id$ *)
+
+(**************************************************************************)
+(*              Basic lemmas for the classical reals numbers              *)
+(**************************************************************************)
+
+Require Export Raxioms.
+Require Export ZArithRing.
+Require Classical_Prop.
+Require Omega.
+
+(**************************************************************************)
+(*       On commence par instancier la tactique Ring sur les réels        *)
+(**************************************************************************)
+
+
+Lemma RTheory : (Ring_Theory Rplus Rmult R1 R0 Ropp [x,y:R]false).
+  Split.
+  Exact Rplus_sym.
+  Symmetry; Apply Rplus_assoc.
+  Exact Rmult_sym.
+  Symmetry; Apply Rmult_assoc.
+  Intro; Apply (let (H1,H2)=(Rplus_ne n) in H2).
+  Intro; Apply (let (H1,H2)=(Rmult_ne n) in H2).
+  Exact Rplus_Ropp_r.
+  Intros.
+  Rewrite Rmult_sym.
+  Rewrite (Rmult_sym n p).
+  Rewrite (Rmult_sym m p).
+  Apply Rmult_Rplus_distr.
+  Intros; Contradiction.
+Defined.
+
+Add Abstract Ring R Rplus Rmult R1 R0 Ropp [x,y:R]false RTheory.
+
+(**************************************************************************)
+(*                            Basic Lemmas                                *)
+(**************************************************************************)
+
+(**********)
+Lemma Req_EM:(r1,r2:R)(r1==r2)\/(~r1==r2).
+Intros;Apply (classic r1==r2).
+Save.
+Hints Resolve Req_EM : real v62.
+
+(**********)
+Lemma total_order:(r1,r2:R)((Rlt r1 r2)\/(r1==r2)\/(Rgt r1 r2)).
+Intros;Elim (total_order_T r1 r2);Intro;Auto.
+Elim y;Intro;Auto.
+Save.
+
+(**********)
+Lemma not_Req:(r1,r2:R)(~(r1==r2))->((Rlt r1 r2)\/(Rgt r1 r2)).
+Intros; Case (total_order r1 r2); Intros.
+Left; Exact H0.
+Case H0; Intros.
+Absurd r1==r2; Auto with zarith real.
+Right; Exact H1.
+Save.
+
+(**********)
+Lemma imp_not_Req:(r1,r2:R)((Rlt r1 r2)\/(Rgt r1 r2))->(~(r1==r2)).
+Intros; Elim H; Intro; Clear H;Red; Intro;Rewrite H in H0.
+Generalize (Rlt_antisym r2 r2 H0); Intro; Auto with zarith real.
+Unfold Rgt in H0;Generalize (Rlt_antisym r2 r2 H0);Intro; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rlt_antirefl:(r:R)~(Rlt r r).
+  Red; Intros; Apply (Rlt_antisym r r H); Auto with zarith real.
+Save.
+
+(**********)
+Lemma total_order_Rlt:(r1,r2:R)(sumboolT (Rlt r1 r2) ~(Rlt r1 r2)).
+Intros;Elim (total_order_T r1 r2);Intros.
+Elim y;Intro.
+Left;Assumption.
+Right;Rewrite y0;Apply Rlt_antirefl.
+Right;Unfold Rgt in y;Apply Rlt_antisym;Assumption.
+Save.
+
+(**********)
+Lemma total_order_Rle:(r1,r2:R)(sumboolT (Rle r1 r2) ~(Rle r1 r2)).
+Intros;Elim (total_order_T r1 r2);Intros.
+Left;Unfold Rle;Elim y;Intro;Auto.
+Right;Red;Intro;Elim H;Intro.
+Unfold Rgt in y;Generalize (Rlt_antisym r2 r1 y);Auto.
+Generalize (imp_not_Req r1 r2 (or_intror (Rlt r1 r2) (Rgt r1 r2) y));Auto.
+Save.
+
+(**********)
+Lemma total_order_Rgt:(r1,r2:R)(sumboolT (Rgt r1 r2) ~(Rgt r1 r2)).
+Unfold Rgt;Intros;Apply total_order_Rlt.
+Save.
+
+(**********)
+Lemma total_order_Rge:(r1,r2:R)(sumboolT (Rge r1 r2) ~(Rge r1 r2)).
+Unfold Rge;Unfold Rgt;Intros;Elim (total_order_Rle r2 r1);Intro.
+Left;Unfold Rle in y;Elim y;Auto.
+Right;Unfold Rle in y;Red;Intro;Elim H;Intro.
+Elim y;Left;Assumption.
+Elim y;Right;Auto.
+Save.
+
+(*********************************************************)
+(*         Field Lemmas                                  *)
+(*********************************************************)
+(*********************************************************)
+(*       Addition                                        *)
+(*********************************************************)
+
+(**********)
+Lemma Rplus_Ropp_l:(r:R)((Rplus (Ropp r) r)==R0).
+  Intro; Ring.
+Save.
+
+(**********)
+Lemma Rplus_Ropp:(x,y:R)((Rplus x y)==R0)->(y==(Ropp x)).
+  Intros; Replace y with (Rplus (Rplus (Ropp x) x) y);
+  [ Rewrite -> Rplus_assoc; Rewrite -> H; Ring
+  | Ring ].
+Save.
+
+(* New *)
+Hint eqT_R_congr : real := Resolve (congr_eqT R).
+
+Lemma Rplus_plus_r:(r,r1,r2:R)(r1==r2)->((Rplus r r1)==(Rplus r r2)).
+  Auto with real.
+Save.
+
+(* Old *)
+Hints Resolve Rplus_plus_r : v62.
+
+(**********)
+Lemma r_Rplus_plus:(r,r1,r2:R)((Rplus r r1)==(Rplus r r2))->(r1==r2).
+  Intros;
+   Cut (Rplus (Rplus (Ropp r) r) r1)==(Rplus (Rplus (Ropp r) r) r2).
+  Ring (Rplus (Rplus (Ropp r) r) r1) (Rplus (Rplus (Ropp r) r) r2); Trivial.
+  Repeat Rewrite -> Rplus_assoc; Rewrite <- H; Reflexivity.
+Save.
+
+Hints Resolve r_Rplus_plus : real.
+
+(**********)
+Lemma Rplus_ne_i:(r,b:R)((Rplus r b)==r)->(b==R0).
+  Intros r b; Replace r with (Rplus r R0).
+  Rewrite -> Rplus_assoc; Ring (Rplus R0 b); EAuto with real.
+  Ring.
+Save.
+
+(***********************************************************)       
+(*        Multiplication                                   *)
+(***********************************************************)
+
+(**********)
+Lemma Rinv_r:(r:R)(~(r==R0))->((Rmult r (Rinv r))==R1).
+  Intros; Rewrite -> Rmult_sym; Apply (Rinv_l r H); Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rmult_Or:(r:R)((Rmult r R0)==R0).
+Intro; Ring.
+Save.
+Hints Resolve Rmult_Or : real v62.
+
+(**********)
+Lemma Rmult_Ol:(r:R)((Rmult R0 r)==R0).
+Intro; Ring.
+Save.
+Hints Resolve Rmult_Ol : real v62.
+
+(**********)
+Lemma Rmult_mult_r:(r,r1,r2:R)(r1==r2)->((Rmult r r1)==(Rmult r r2)).
+  Auto with real.
+Save.
+(* OLD *)
+Hints Resolve Rmult_mult_r : v62.
+
+(**********)
+Lemma r_Rmult_mult:(r,r1,r2:R)((Rmult r r1)==(Rmult r r2))->
+  (~(r==R0))->(r1==r2).
+  Intros;
+   Cut (Rmult (Rmult (Rinv r) r) r1)==(Rmult (Rmult (Rinv r) r) r2).
+  Rewrite -> Rinv_l with r; Ring (Rmult R1 r1) (Rmult R1 r2); Trivial.
+
+  Repeat Rewrite -> Rmult_assoc.
+  Rewrite H; Trivial.
+Save.
+
+(**********)
+Lemma without_div_Od:(r1,r2:R)(Rmult r1 r2)==R0 -> r1==R0 \/ r2==R0.
+  Intros; Cut r1==R0\/~r1==R0.
+  Intros [Hz | Hnotz].
+  Left; Auto.
+  Replace r2 with (Rmult R0 (Rinv r1)); Auto with real.
+  Apply r_Rmult_mult with r1.
+  Rewrite H; Ring.
+  Assumption.
+  Auto with real.
+Save.
+
+(**********)
+Lemma without_div_Oi1:(r1,r2:R) r1==R0 -> (Rmult r1 r2)==R0.
+  Intros; Rewrite -> H; Ring.
+Save.
+
+(**********)
+Lemma without_div_Oi2:(r1,r2:R) r2==R0 -> (Rmult r1 r2)==R0.
+  Intros; Rewrite -> H; Ring.
+Save.
+
+(**********)
+Lemma without_div_Oi:(r1,r2:R) (r1==R0)\/(r2==R0) -> (Rmult r1 r2)==R0.
+  Intros r1 r2 [H | H]; Rewrite H; Ring.
+Save.
+
+(**********) 
+Lemma without_div_O_contr:(r1,r2:R)
+   ~(Rmult r1 r2)==R0 -> ~r1==R0 /\ ~r2==R0.
+Intros; Cut (P,Q,R:Prop)(P\/Q->R)->~R->~P/\~Q.
+Intro;Generalize (H0 r1==R0 r2==R0 (Rmult r1 r2)==R0
+       (without_div_Oi r1 r2));Intro;Apply (H1 H).
+Tauto.
+Save.
+
+(***********)
+Definition Rsqr:R->R:=[r:R](Rmult r r).
+
+(***********)
+Lemma Rsqr_O:((Rsqr R0)==R0).
+  Unfold Rsqr; Ring.
+Save.
+
+(***********)
+Lemma Rsqr_r_R0:(r:R)(Rsqr r)==R0->r==R0.
+Unfold Rsqr;Intros;Elim (without_div_Od r r H);Trivial.
+Save.
+
+(*********************************************************)
+(*       Opposite                                        *)
+(*********************************************************)
+
+(**********)
+Lemma Ropp_Ropp:(r:R)((Ropp (Ropp r))==r).
+  Intro; Ring.
+Save.
+
+(**********)
+Lemma Ropp_O:((Ropp R0)==R0).
+  Ring.
+Save.
+Hints Resolve Ropp_O : real v62.
+
+(**********)
+Lemma Ropp_distr1:(r1,r2:R)
+ ((Ropp (Rplus r1 r2))==(Rplus (Ropp r1) (Ropp r2))).
+  Intros; Ring.
+Save.
+
+(**********)
+Lemma Ropp_distr2:(r1,r2:R)((Ropp (Rminus r1 r2))==(Rminus r2 r1)).
+  Intros; Ring.
+Save.
+
+(**********)
+Lemma eq_Rminus:(r1,r2:R)(r1==r2)->((Rminus r1 r2)==R0).
+  Intros; Rewrite H; Ring.
+Save.
+
+(**********)
+Lemma Rminus_eq:(r1,r2:R)(Rminus r1 r2)==R0 -> r1==r2.
+  Intros r1 r2; Unfold Rminus; Rewrite -> Rplus_sym; Intro.
+  Rewrite <- (Ropp_Ropp r2); Apply (Rplus_Ropp (Ropp r2) r1 H).
+Save.
+
+(**********)
+Lemma Rminus_eq_contra:(r1,r2:R)~r1==r2->~(Rminus r1 r2)==R0.
+Intros;Cut (P,Q:Prop)(P->Q)->(~Q->~P).
+Intro cla;Apply (cla (Rminus r1 r2)==R0  r1==r2 (Rminus_eq r1 r2));Assumption.
+Tauto.
+Save.
+
+(**********)
+Lemma eq_Ropp:(r1,r2:R)(r1==r2)->((Ropp r1)==(Ropp r2)).
+  Auto with real.
+Save.
+
+(**********)
+Lemma eq_RoppO:(r:R)(r==R0)->((Ropp r)==R0).
+  Intros; Rewrite -> H; Ring.
+Save.
+
+(**********)
+Lemma minus_R0:(r:R)(Rminus r R0)==r.
+Intro;Unfold Rminus;Rewrite (eq_RoppO R0 (refl_eqT R R0));
+ Elim(Rplus_ne r);Intros a b;Rewrite a;Clear a b;Auto with zarith real.
+Save.
+
+(**********)
+Lemma Ropp_mul1:(r1,r2:R)(Rmult (Ropp r1) r2)==(Ropp (Rmult r1 r2)).
+  Intros; Ring.
+Save.
+
+(**********)
+Lemma Ropp_mul2:(r1,r2:R)(Rmult (Ropp r1) (Ropp r2))==(Rmult r1 r2).
+  Intros; Ring.
+Save.
+
+(*********)
+Lemma Ropp_neq:(r:R)~r==R0->~(Ropp r)==R0.
+Intros;Red;Intro;Generalize (Rplus_plus_r r (Ropp r) R0 H0);Intro;
+ Rewrite (Rplus_Ropp_r r) in H1;
+ Rewrite (let (H1,H2)=(Rplus_ne r) in H1) in H1;
+ Generalize (sym_eqT R R0 r H1);Intro;Auto.
+Save.
+
+(*********)
+Lemma Rinv_Rmult:(r1,r2:R)(~r1==R0)->(~r2==R0)->
+  (Rinv (Rmult r1 r2))==(Rmult (Rinv r1) (Rinv r2)).
+Intros;Cut ~(Rmult r1 r2)==R0.
+Intro;Apply (r_Rmult_mult (Rmult r1 r2));Auto.
+Rewrite (Rinv_r (Rmult r1 r2) H1);
+ Rewrite (Rmult_sym (Rinv r1) (Rinv r2));
+ Rewrite (Rmult_assoc r1 r2  (Rmult (Rinv r2) (Rinv r1)));
+ Rewrite <-(Rmult_assoc r2 (Rinv r2) (Rinv r1));
+ Rewrite (Rinv_r r2 H0);
+ Rewrite (let (H1,H2)=(Rmult_ne (Rinv r1)) in H2);
+ Rewrite (Rinv_r r1 H);Trivial.
+Red;Intro;Generalize (without_div_Od r1 r2 H1);Intro;Elim H2;Intro;Auto.
+Save.
+
+(*********)
+Lemma Ropp_Rinv:(r:R)~r==R0->(Ropp (Rinv r))==(Rinv (Ropp r)).
+Intros;Generalize (refl_eqT R R1);Pattern 1 R1;
+ Rewrite <-(Rinv_l r H);Rewrite <-(Rinv_l (Ropp r) (Ropp_neq r H));
+ Intro;Rewrite <-(Ropp_mul2 (Rinv r) r) in H0;
+ Rewrite (Rmult_sym (Ropp (Rinv r)) (Ropp r)) in H0;
+ Rewrite (Rmult_sym (Rinv (Ropp r)) (Ropp r)) in H0;
+ Apply (r_Rmult_mult (Ropp r) (Ropp (Rinv r)) (Rinv (Ropp r))
+    H0 (Ropp_neq r H)).
+Save.
+
+(*********)
+Lemma Rinv_Rmult_simpl:(a,b,c:R)(~a==R0)->
+      (Rmult (Rmult a (Rinv b))(Rmult c (Rinv a)))==
+      (Rmult c (Rinv b)).
+Intros; Rewrite (Rmult_sym (Rmult a (Rinv b)) (Rmult c (Rinv a)));
+ Rewrite (Rmult_assoc c (Rinv a) (Rmult a (Rinv b)));
+ Rewrite <-(Rmult_assoc (Rinv a) a (Rinv b));
+ Rewrite (Rinv_l a H);Rewrite (let (H1,H2)=(Rmult_ne (Rinv b)) in H2);
+ Reflexivity.
+Save.
+
+(*********************************************************)
+(*       Order Lemma                                     *)
+(*********************************************************)
+(*********************************************************)
+(*       Lower                                       *)
+(*********************************************************)
+
+(**********)
+Lemma not_Rle:(r1,r2:R)~(Rle r1 r2)->(Rgt r1 r2).
+Intros; Unfold Rle in H; Elim (total_order r1 r2); Intro.
+Elim H;Left; Assumption.
+Elim H0; Intro;Auto with zarith real.
+Elim H;Right; Assumption.
+Save.
+
+(**********)
+Lemma Rle_not:(r1,r2:R)(Rlt r2 r1)->~(Rle r1 r2).
+Intros; Red; Intro;Unfold Rle in H0;Elim H0; Intro.
+Generalize (Rlt_antisym r1 r2 H1); Intro; Auto with zarith real.
+Elim (imp_not_Req r2 r1);Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rle_le_eq:(r1,r2:R)(Rle r1 r2)/\(Rle r2 r1)<->(r1==r2).
+Intros; Split; Intro.
+Elim H; Unfold Rle; Intros.
+Elim H0; Elim H1; Intros.
+Absurd (Rlt r2 r1).
+Red; Intro.
+Apply (Rlt_antisym r1 r2 H3 H4).
+Auto with zarith real.
+Auto with zarith real.
+Auto with zarith real.
+Auto with zarith real.
+Rewrite <- H; Split; Unfold Rle; Right; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rlt_le:(r1,r2:R)(Rlt r1 r2)->(Rle r1 r2).
+Intros; Unfold Rle; Left; Auto with zarith real.
+Save.
+
+(**********)
+Lemma eq_Rle:(r1,r2:R)(r1==r2)->(Rle r1 r2).
+Intros; Unfold Rle; Right; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rle_trans:(r1,r2,r3:R)
+  (Rle r1 r2)->(Rle r2 r3)->(Rle r1 r3).
+Intros r1 r2 r3; Unfold Rle; Intros.
+Elim H; Elim H0; Intros.
+Cut (Rlt r1 r3).
+Intro.
+Apply (Rlt_le r1 r3); Auto with zarith real.
+Apply (Rlt_trans r1 r2 r3); Auto with zarith real.
+Rewrite <- H1; Auto with zarith real.
+Rewrite -> H2; Auto with zarith real.
+Rewrite -> H2; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rle_lt_trans:(r1,r2,r3:R)
+  (Rle r1 r2)->(Rlt r2 r3)->(Rlt r1 r3).
+Intros; Unfold Rle in H; Elim H; Intro.
+Apply (Rlt_trans r1 r2 r3 H1 H0).
+Rewrite -> H1; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rlt_le_trans:(r1,r2,r3:R)
+  (Rlt r1 r2)->(Rle r2 r3)->(Rlt r1 r3).
+Intros; Unfold Rle in H0; Elim H0; Intro.
+Apply (Rlt_trans r1 r2 r3 H H1).
+Rewrite <- H1; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rlt_anti_compatibility:
+    (r,r1,r2:R)(Rlt (Rplus r r1) (Rplus r r2))->(Rlt r1 r2).
+Intros;
+ Cut (Rlt (Rplus (Rplus (Ropp r) r) r1) 
+          (Rplus (Rplus (Ropp r) r) r2)).
+Rewrite -> Rplus_Ropp_l.
+Elim (Rplus_ne r1); Elim (Rplus_ne r2); Intros; Rewrite <- H3;
+ Rewrite <- H1; Auto with zarith real.
+Rewrite -> Rplus_assoc; Rewrite -> Rplus_assoc;
+ Apply (Rlt_compatibility (Ropp r) (Rplus r r1) (Rplus r r2) H).
+Save.
+
+(**********)
+Lemma Rle_compatibility:(r,r1,r2:R)(Rle r1 r2)->
+      (Rle (Rplus r r1) (Rplus r r2)).
+Unfold Rle; Intros; Elim H; Intro.
+Left; Apply (Rlt_compatibility r r1 r2 H0).
+Right; Rewrite <- H0; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rle_anti_compatibility:
+   (r,r1,r2:R)(Rle (Rplus r r1) (Rplus r r2))->(Rle r1 r2).
+Unfold Rle; Intros; Elim H; Intro.
+Left; Apply (Rlt_anti_compatibility r r1 r2 H0).
+Right; Apply (r_Rplus_plus r r1 r2 H0).
+Save.
+
+(**********)
+Lemma Rgt_Ropp:(r1,r2:R)
+ (Rgt r1 r2)->(Rlt (Ropp r1) (Ropp r2)).
+Intros;Unfold Rgt in H;
+ Generalize (Rlt_compatibility (Ropp r2) r2 r1 H);Intro;
+ Generalize (Rlt_compatibility (Ropp r1) (Rplus (Ropp r2) r2) 
+               (Rplus (Ropp r2) r1) H0);
+ Rewrite (Rplus_Ropp_l r2);Rewrite (Rplus_sym (Ropp r2) r1);
+ Rewrite <-(Rplus_assoc (Ropp r1) r1 (Ropp r2)); 
+ Rewrite (Rplus_Ropp_l r1);Elim (Rplus_ne (Ropp r1));Intros a b;
+ Rewrite a;Clear a b;Elim (Rplus_ne (Ropp r2));Intros a b;
+ Rewrite b;Clear a b;Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rlt_Ropp:(r1,r2:R)
+ (Rlt r1 r2)->(Rgt (Ropp r1) (Ropp r2)).
+Intros; Cut (Rgt r2 r1).
+Intro; Cut (Rlt (Ropp r2) (Ropp r1)); Auto with zarith real.
+Apply (Rgt_Ropp r2 r1 H0).
+Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rlt_anti_monotony:(r,r1,r2:R)(Rlt r R0)->(Rlt r1 r2)->
+      (Rgt (Rmult r r1) (Rmult r r2)).
+Intros;Generalize (Rlt_Ropp r1 r2 H0);Intro;Unfold Rgt;
+ Rewrite <-(Ropp_mul2 r r2);Rewrite <-(Ropp_mul2 r r1);
+ Apply (Rlt_monotony (Ropp r) (Ropp r2) (Ropp r1));Auto with zarith real.
+Apply (Rlt_anti_compatibility r R0 (Ropp r));
+ Elim (Rplus_ne r);Intros a b;Rewrite a;Clear a b;
+ Rewrite (Rplus_Ropp_r r);Assumption.
+Save.
+
+(**********)
+Lemma Rlt_minus:(r1,r2:R)(Rlt r1 r2)->(Rlt (Rminus r1 r2) R0).
+Intros; Cut (Rlt (Rminus r1 r2) (Rminus r2 r2)).
+Rewrite -> (eq_Rminus r2); Auto with zarith real.
+Unfold Rminus; Rewrite -> (Rplus_sym r1 (Ropp r2));
+ Rewrite -> (Rplus_sym r2 (Ropp r2));
+ Apply (Rlt_compatibility (Ropp r2) r1 r2 H).
+Save.
+
+(**********)
+Lemma Rle_minus:(r1,r2:R)(Rle r1 r2)->(Rle (Rminus r1 r2) R0).
+Unfold Rle; Intros; Elim H; Intro.
+Left; Apply (Rlt_minus r1 r2 H0).
+Right; Apply (eq_Rminus r1 r2 H0).
+Save.
+
+(**********)
+Lemma Rminus_lt:(r1,r2:R)(Rlt (Rminus r1 r2) R0)->(Rlt r1 r2).
+Intros;Unfold Rminus in H;
+  Generalize (Rlt_compatibility r2 (Rplus r1 (Ropp r2)) R0 H);
+  Intro;Clear H;
+  Rewrite (Rplus_sym r1 (Ropp r2)) in H0;
+  Rewrite <- (Rplus_assoc r2 (Ropp r2) r1) in H0;
+  Rewrite (Rplus_Ropp_r r2) in H0;Elim (Rplus_ne r1); Elim (Rplus_ne r2); 
+  Intros;
+  Rewrite H3 in H0; Rewrite H in H0; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rminus_le:(r1,r2:R)(Rle (Rminus r1 r2) R0)->(Rle r1 r2).
+Unfold Rle;Intros;Elim H; Intro;Clear H.
+Left;Apply Rminus_lt;Auto with zarith real.
+Right;Apply Rminus_eq;Auto with zarith real.
+Save.
+
+(**********)
+Lemma sum_inequa_Rle_lt:(a,x,b,c,y,d:R)(Rle a x)->(Rlt x b)->
+           (Rlt c y)->(Rle y d)->
+        (Rlt (Rplus a c) (Rplus x y))/\(Rlt (Rplus x y) (Rplus b d)).
+Intros;Split.
+Apply (Rlt_le_trans (Rplus a c) (Rplus a y) (Rplus x y)).
+Apply (Rlt_compatibility a c y H1).
+Rewrite (Rplus_sym a y);Rewrite (Rplus_sym x y);
+ Apply (Rle_compatibility y a x H).
+Apply (Rle_lt_trans (Rplus x y) (Rplus d x) (Rplus b d)).
+Rewrite (Rplus_sym d x);Apply (Rle_compatibility x y d H2).
+Rewrite (Rplus_sym b d);Apply (Rlt_compatibility d x b H0).
+Save.
+
+(*********)
+Lemma Rplus_lt:(r1,r2,r3,r4:R)(Rlt r1 r2)->(Rlt r3 r4)->
+ (Rlt (Rplus r1 r3) (Rplus r2 r4)).
+Intros; Generalize (Rlt_compatibility r3 r1 r2 H);
+ Generalize (Rlt_compatibility r2 r3 r4 H0);Intros;
+ Rewrite (Rplus_sym r3 r2) in H2;Rewrite (Rplus_sym r3 r1) in H2;
+ Apply (Rlt_trans (Rplus r1 r3) (Rplus r2 r3) (Rplus r2 r4) H2 H1).
+Save.
+
+(*********)
+Lemma Rmult_lt:(r1,r2,r3,r4:R)(Rgt r3 R0)->(Rgt r2 R0)->
+  (Rlt r1 r2)->(Rlt r3 r4)->(Rlt (Rmult r1 r3) (Rmult r2 r4)).
+Intros;Unfold Rgt in H H0;Generalize (Rlt_monotony r3 r1 r2 H H1);Intro;
+ Generalize (Rlt_monotony r2 r3 r4 H0 H2);Intro;
+ Rewrite (Rmult_sym r3 r1) in H3;Rewrite (Rmult_sym r3 r2) in H3;
+ Apply (Rlt_trans (Rmult r1 r3) (Rmult r2 r3) (Rmult r2 r4) H3 H4). 
+Save.
+
+(**********)
+Lemma inser_trans_R:(n,m,p,q:R)(Rle n m)/\(Rlt m p)->
+      (sumboolT ((Rle n m)/\(Rlt m q)) ((Rle q m)/\(Rlt m p))).
+Intros; Cut (sumboolT (Rle q m) (Rlt m q)).
+Intro;Cut (Rle n m);[Intro;Cut (Rlt m p)|Elim H;Auto with zarith real].
+Intro;Elim X;Intro.
+Right; Auto with zarith real.
+Left; Auto with zarith real.
+Elim H;Auto with zarith real.
+Generalize (total_order_Rle q m); Intro; Elim X; Intro.
+Left;Auto with zarith real.
+Right; Generalize (not_Rle q m y); Auto with zarith real.
+Save.
+
+(**********)
+Lemma tech_Rplus:(r,s:R)(Rle R0 r)->(Rlt R0 s)->~(Rplus r s)==R0.
+Red;Intros;Cut (Rlt R0 (Rplus r s)).
+Intro;Elim (imp_not_Req R0 (Rplus r s));Auto with zarith real.
+Clear H1;Generalize (Rlt_compatibility r R0 s H0);Intro;
+ Elim (Rplus_ne r);Intros a b;Rewrite a in H1;Clear a b;
+ Apply (Rle_lt_trans R0 r (Rplus r s) H H1).
+Save.
+
+(***********)
+Lemma pos_Rsqr:(r:R)(Rle R0 (Rsqr r)).
+Intro; Cut (Rlt r R0)\/r==R0\/(Rgt r R0).
+Intro; Elim H; Intro; Unfold Rle.
+Left; Replace R0 with (Rmult r R0).
+Unfold Rsqr; Apply (Rlt_anti_monotony r r R0 H0 H0).
+Auto with zarith real.
+Elim H0; Intro.
+Right; Rewrite -> H1; Apply sym_eqT; Apply Rsqr_O.
+Left; Unfold Rgt in H1; Replace R0 with (Rmult r R0).
+Unfold Rsqr; Apply (Rlt_monotony r R0 r H1 H1).
+Auto with zarith real.
+Apply (total_order r R0).
+Save.
+
+(***********)
+Lemma pos_Rsqr1:(r:R)(~(r==R0))->(Rlt R0 (Rsqr r)).
+Intros; Cut (Rlt r R0)\/(Rgt r R0).
+Intro; Elim H0; Intro.
+Replace R0 with (Rmult r R0); Unfold Rsqr.
+Apply (Rlt_anti_monotony r r R0 H1 H1).
+Auto with zarith real.
+Unfold Rgt in H1; Replace R0 with (Rmult r R0).
+Unfold Rsqr; Apply (Rlt_monotony r R0 r H1 H1).
+Auto with zarith real.
+Apply (not_Req r R0 H).
+Save.
+
+(**********)
+Lemma Rlt_R0_R1:(Rlt R0 R1).
+Cut ~R1==R0->(Rlt R0 (Rsqr R1)).
+Intro; Replace R1 with (Rsqr R1); Cut ~R1==R0; Auto with zarith real.
+Red; Intro; Apply (R1_neq_R0 H0).
+Unfold Rsqr; Elim (Rmult_ne R1); Auto with zarith real.
+Red; Intro; Apply (R1_neq_R0 H0).
+Intro; Apply (pos_Rsqr1 R1 H).
+Save.
+
+(*********)
+Lemma Rlt_Rinv:(r:R)(Rlt R0 r)->(Rlt R0 (Rinv r)).
+Intros; Fold (Rgt (Rinv r) R0); Apply (not_Rle (Rinv r) R0);Red;
+ Intro;Unfold Rle in H0;Elim H0; Intro;Clear H0.
+Generalize (Rlt_monotony r (Rinv r) R0 H H1);Rewrite (Rinv_r r).
+Rewrite (Rmult_Or r);Intro;Generalize (Rle_not R0 R1 H0);
+ Generalize (Rlt_le R0 R1 Rlt_R0_R1);Intros;Auto.
+Apply (sym_not_eqT R R0 r);Apply (imp_not_Req R0 r);Left;Assumption.
+Generalize (Rmult_mult_r r (Rinv r) R0 H1);Rewrite (Rinv_r r).
+Rewrite (Rmult_Or r);Intro;Generalize R1_neq_R0;Auto.
+Apply (sym_not_eqT R R0 r);Apply (imp_not_Req R0 r);Left;Assumption.
+Save.
+
+(*********)
+Lemma Rlt_Rinv2:(r:R)(Rlt r R0)->(Rlt (Rinv r) R0).
+Intros;Fold (Rgt R0 (Rinv r)); Apply (not_Rle R0 (Rinv r));Red;
+ Intro;Unfold Rle in H0;Elim H0; Intro;Clear H0.
+Generalize (Rlt_monotony (Rinv r) r R0 H1 H);Rewrite (Rinv_l r).
+Rewrite (Rmult_Or (Rinv r));Intro;Generalize (Rle_not R0 R1 H0);
+ Generalize (Rlt_le R0 R1 Rlt_R0_R1);Intros;Auto.
+Apply (imp_not_Req r R0);Left;Assumption.
+Generalize (Rmult_mult_r r R0 (Rinv r) H1);Rewrite (Rinv_r r).
+Rewrite (Rmult_Or r);Intro;Generalize R1_neq_R0;Auto.
+Apply (imp_not_Req r R0);Left;Assumption.
+Save.
+
+(*********************************************************)        
+(*       Greater                                         *)
+(*********************************************************)
+
+(**********)
+Lemma Rge_ge_eq:(r1,r2:R)(Rge r1 r2)->(Rge r2 r1)->r1==r2.
+Unfold Rge; Intros; Elim H; Intro; Auto with zarith real.
+Elim H0; Intro; Auto with zarith real.
+Absurd (Rgt r1 r2); Auto with zarith real.
+Unfold Rgt; Unfold Rgt in H2; Apply Rlt_antisym; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rlt_not_ge:(r1,r2:R)~(Rlt r1 r2)->(Rge r1 r2).
+Intros; Unfold Rge; Elim (total_order r1 r2); Intro.
+ElimType False; Auto with zarith real.
+Elim H0; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rgt_not_le:(r1,r2:R)~(Rgt r1 r2)->(Rle r1 r2).
+Intros; Unfold Rgt in H; Unfold Rle; Elim (total_order r1 r2); Intro.
+Left ; Auto with zarith real.
+Elim H0; Intro; Auto with zarith real.
+Unfold Rgt in H1; ElimType False; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rgt_ge:(r1,r2:R)(Rgt r1 r2)->(Rge r1 r2).
+Intros; Unfold Rge; Left; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rlt_sym:(r1,r2:R)
+ (((Rlt r1 r2)->(Rgt r2 r1))/\((Rgt r2 r1)->(Rlt r1 r2))).
+Intros; Split; Intro; Unfold Rgt; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rle_sym1:(r1,r2:R)(Rle r1 r2)->(Rge r2 r1).
+Intros r1 r2; Unfold Rge; Unfold Rle; Intro; Elim H; Intro.
+Left; Unfold Rgt; Auto with zarith real.
+Right; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rle_sym2:(r1,r2:R)(Rge r2 r1)->(Rle r1 r2).
+Intros r1 r2; Unfold Rge; Unfold Rle; Intro; Elim H; Intro.
+Left; Unfold Rgt in H0; Auto with zarith real.
+Right; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rle_sym:(r1,r2:R)
+ (((Rle r1 r2)->(Rge r2 r1))/\((Rge r2 r1)->(Rle r1 r2))).
+Intros; Split; Intro.
+Apply Rle_sym1; Auto with zarith real.
+Apply Rle_sym2; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rge_gt_trans:(r1,r2,r3:R)
+ (Rge r1 r2)->(Rgt r2 r3)->(Rgt r1 r3).
+Intros r1 r2 r3; Unfold Rgt; Unfold Rge; Intros; Elim H; Intros.
+Unfold Rgt in H1; Apply (Rlt_trans r3 r2 r1 H0 H1).
+Rewrite -> H1; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rgt_ge_trans:(r1,r2,r3:R)
+ (Rgt r1 r2)->(Rge r2 r3)->(Rgt r1 r3).
+Intros r1 r2 r3; Unfold Rgt; Unfold Rge; Intros; Elim H0; Intros.
+Apply (Rlt_trans r3 r2 r1 H1 H).
+Rewrite <- H1; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rgt_trans:(r1,r2,r3:R)
+ (Rgt r1 r2)->(Rgt r2 r3)->(Rgt r1 r3).
+Intros; Cut (Rge r1 r2).
+Intro; Apply (Rge_gt_trans r1 r2 r3 H1 H0).
+Apply (Rgt_ge r1 r2 H).
+Save.
+
+(**********)
+Lemma Rge_trans:(r1,r2,r3:R)
+ (Rge r1 r2)->(Rge r2 r3)->(Rge r1 r3).
+Intros; Cut (Rle r2 r1).
+Cut (Rle r3 r2); Intros.
+Cut (Rle r3 r1).
+Intro; Apply (Rle_sym1 r3 r1 H3).
+Apply (Rle_trans r3 r2 r1 H1 H2).
+Apply (Rle_sym2 r3 r2 H0).
+Apply (Rle_sym2 r2 r1 H).
+Save.
+
+(**********)
+Lemma eq_Rge:(r1,r2:R)(r1==r2)->(Rge r1 r2).
+Intros; Unfold Rge; Right; Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rle_Ropp:(r1,r2:R)
+ (Rle r1 r2)->(Rge (Ropp r1) (Ropp r2)).
+Unfold Rle; Intros; Unfold Rge; Elim H; Intro.
+Left; Apply (Rlt_Ropp r1 r2 H0).
+Right; Apply (eq_Ropp r1 r2 H0).
+Save.
+
+(**********)
+Lemma Rgt_RoppO:(r:R)(Rgt r R0)->(Rlt (Ropp r) R0).
+Intros; Rewrite <- Ropp_O; Apply (Rgt_Ropp r R0); Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rlt_RoppO:(r:R)(Rlt r R0)->(Rgt (Ropp r) R0).
+Intros; Rewrite <- Ropp_O; Apply (Rlt_Ropp r R0); Auto with zarith real.
+Save.
+
+(**********)
+Lemma Rlt_r_plus_R1:(r:R)(Rle R0 r)->(Rlt R0 (Rplus r R1)).
+Unfold Rle; Intros; Elim H; Intro; Clear H.
+Apply (Rlt_anti_compatibility (Ropp r) R0 (Rplus r R1));
+ Elim (Rplus_ne (Ropp r)); Intros; Rewrite H; Clear H H1;
+ Rewrite <- (Rplus_assoc (Ropp r) r R1); Rewrite Rplus_Ropp_l;
+ Elim (Rplus_ne R1); Intros; Rewrite H1; Clear H H1;
+ Fold (Rgt r R0) in H0; Generalize (Rgt_RoppO r H0); Intro;
+ Generalize Rlt_R0_R1; Intro; Apply (Rlt_trans (Ropp r) R0 R1 H H1).
+Rewrite <- H0; Elim (Rplus_ne R1); Intros; Rewrite H1; Clear H H1;
+ Apply Rlt_R0_R1.
+Save.
+
+(**********)
+Lemma tech_Rgt_minus:(r1,r2:R)(Rlt R0 r2)->(Rgt r1 (Rminus r1 r2)).
+Intros;Fold (Rgt r2 R0) in H;Generalize (Rgt_RoppO r2 H); Intro;
+  Generalize (Rlt_compatibility r1 (Ropp r2) R0 H0); Intro;
+  Elim (Rplus_ne r1); Intros a b; Rewrite a in H1; Clear a b;
+  Unfold Rgt;Unfold Rminus;Assumption.
+Save.
+
+(***********)
+Lemma Rgt_plus_plus_r:(r,r1,r2:R)(Rgt r1 r2)->
+      (Rgt (Rplus r r1) (Rplus r r2)).
+Unfold Rgt; Intros; Apply (Rlt_compatibility r r2 r1 H).
+Save.
+
+(***********)
+Lemma Rgt_r_plus_plus:(r,r1,r2:R)(Rgt (Rplus r r1) (Rplus r r2))->
+                              (Rgt r1 r2).
+Unfold Rgt; Intros; Apply (Rlt_anti_compatibility r r2 r1 H).
+Save.
+
+(***********)
+Lemma Rge_plus_plus_r:(r,r1,r2:R)(Rge r1 r2)->
+      (Rge (Rplus r r1) (Rplus r r2)).
+Unfold Rge; Intros; Elim H; Intro.
+Left; Apply (Rgt_plus_plus_r r r1 r2 H0).
+Right; Apply (Rplus_plus_r r r1 r2 H0).
+Save.
+
+(***********)
+Lemma Rge_r_plus_plus:(r,r1,r2:R)(Rge (Rplus r r1) (Rplus r r2))->
+                              (Rge r1 r2).
+Unfold Rge; Intros; Elim H; Intro.
+Left; Apply (Rgt_r_plus_plus r r1 r2 H0).
+Right; Apply (r_Rplus_plus r r1 r2 H0).
+Save.
+
+(***********)
+Lemma Rgt_minus:(r1,r2:R)(Rgt r1 r2)->(Rgt (Rminus r1 r2) R0).
+Intros; Cut (Rgt (Rminus r1 r2) (Rminus r2 r2)).
+Rewrite -> (eq_Rminus r2 r2); Auto with zarith real.
+Unfold Rminus; Rewrite -> (Rplus_sym r1 (Ropp r2));
+ Rewrite -> (Rplus_sym r2 (Ropp r2));
+ Apply (Rgt_plus_plus_r (Ropp r2) r1 r2 H).
+Save.
+
+(**********)
+Lemma Rge_minus:(r1,r2:R)(Rge r1 r2)->(Rge (Rminus r1 r2) R0).
+Unfold Rge; Intros; Elim H; Intro.
+Left; Apply (Rgt_minus r1 r2 H0).
+Right; Apply (eq_Rminus r1 r2 H0).
+Save.
+
+(*********)
+Lemma minus_Rge:(r1,r2:R)(Rge (Rminus r1 r2) R0)->(Rge r1 r2).
+Intros;Generalize (Rge_plus_plus_r r2 (Rminus r1 r2) R0 H); Intro;
+ Rewrite (Rplus_sym r2 (Rminus r1 r2)) in H0;Unfold Rminus in H0;
+ Rewrite (Rplus_assoc r1 (Ropp r2) r2) in H0;
+ Rewrite (Rplus_Ropp_l r2) in H0;
+ Elim (Rplus_ne r1); Intros a b; Rewrite a in H0; Clear a b;
+ Elim (Rplus_ne r2); Intros a b; Rewrite a in H0; Clear a b;Exact H0.
+Save.
+
+(*********)
+Lemma Rmult_gt:(r1,r2:R)(Rgt r1 R0)->(Rgt r2 R0)->(Rgt (Rmult r1 r2) R0).
+Unfold Rgt;Intros;Generalize (Rlt_monotony r1 R0 r2 H H0);Intro;
+ Rewrite (Rmult_Or r1) in H1;Assumption.
+Save.
+
+(***********)
+Lemma Rplus_eq_R0:(a,b:R)(Rle R0 a)->(Rle R0 b)->(Rplus a b)==R0->
+                         (a==R0)/\(b==R0).
+Intros;Generalize (Rle_Ropp R0 b H0);Intro;Rewrite Ropp_O in H2;
+ Generalize (Rle_Ropp R0 a H);Intro;Rewrite Ropp_O in H3;
+ Generalize (Rplus_Ropp a b H1);Intro;Rewrite Rplus_sym in H1;
+ Generalize (Rplus_Ropp b a H1);Intro;Clear H1;Rewrite <- H4 in H3;
+ Rewrite <-H5 in H2;Clear H4 H5; Generalize (Rle_sym1 R0 a H);Clear H;
+ Intro;Generalize (Rle_sym1 R0 b H0);Clear H0;Intro;Split;Apply Rge_ge_eq;
+ Assumption.
+Save.
+
+(***********)
+Lemma Rplus_Rsr_eq_R0:(a,b:R)(Rplus (Rsqr a) (Rsqr b))==R0->
+                         (a==R0)/\(b==R0).
+Intros;Elim (Rplus_eq_R0 (Rsqr a) (Rsqr b) (pos_Rsqr a) (pos_Rsqr b) H);
+ Intros;Clear H;Split;Apply Rsqr_r_R0;Assumption.
+Save.
+
+(**********************************************************) 
+(*       Injection from N to R                            *)
+(**********************************************************)
+
+(**********)
+Lemma S_INR:(n:nat)(INR (S n))==(Rplus (INR n) R1).
+Intro; Simpl; Case n.
+Simpl; Elim (Rplus_ne R1); Auto with zarith real.
+Auto with zarith real.
+Save.
+
+(**********)
+Lemma S_O_plus_INR:(n:nat)
+    (INR (plus (S O) n))==(Rplus (INR (S O)) (INR n)).
+Intro; Replace (plus (S O) n) with (S (plus O n)).
+Replace (INR (S (plus O n))) with (Rplus (INR (plus O n)) R1).
+Replace (INR (S O)) with (Rplus (INR O) R1).
+Replace (INR (S O)) with (Rplus (INR O) R1); Simpl; Elim (Rplus_ne R1);
+ Intros; Rewrite -> H0; Auto with zarith real; Rewrite -> Rplus_sym;
+ Auto with zarith real.
+Simpl.
+Elim (Rplus_ne R1); Auto with zarith real.
+Apply sym_eqT; Apply (S_INR (plus O n)).
+Auto with zarith real.
+Save.
+
+(**********)
+Lemma plus_INR:(n,m:nat)(INR (plus n m))==(Rplus (INR n) (INR m)). 
+Induction n.
+Simpl; Intro; Elim (Rplus_ne (INR m)); Auto with zarith real.
+Intros; Rewrite -> plus_Snm_nSm;
+ Replace (INR (S n0)) with (Rplus (INR n0) R1).
+Rewrite -> Rplus_assoc; Rewrite -> (Rplus_sym R1 (INR m));
+ Replace (Rplus (INR m) R1) with (INR (S m)).
+Apply (H (S m)).
+Apply (S_INR m).
+Apply sym_eqT; Apply (S_INR n0).
+Save.
+
+(**********)
+Lemma minus_INR:(n,m:nat)(le m n)->
+   (INR (minus n m))==(Rminus (INR n) (INR m)).
+Intros;
+ Cut (Rplus (INR m) (INR (minus n m)))
+      ==(Rplus (INR m) (Rminus (INR n) (INR m))).
+Intro;
+ Apply (r_Rplus_plus (INR m) (INR (minus n m)) 
+                  (Rminus (INR n) (INR m)) H0).
+Rewrite <- plus_INR; Rewrite -> le_plus_minus_r.
+Unfold Rminus; Rewrite -> Rplus_sym; Rewrite -> Rplus_assoc;
+ Rewrite -> Rplus_Ropp_l; Elim (Rplus_ne (INR n)); Auto with zarith real.
+Auto with zarith real.
+Save.
+
+(**********)
+Lemma INR_le:(n:nat)(Rle R0 (INR n)).
+Induction n.
+Simpl; Apply (eq_Rle R0 R0 (refl_eqT R R0)).
+Intros;Rewrite (S_INR n0);Apply (Rlt_le R0 (Rplus (INR n0) R1));
+ Apply (Rlt_r_plus_R1 (INR n0) H).
+Save.
+
+(**********)
+Lemma not_INR_O:(n:nat)~(INR n)==R0->~n=O.
+Intros;Cut n=(0)->(INR n)==R0.
+Tauto.
+Intro;Rewrite H0;Auto with zarith real.
+Save.
+
+(**********)
+Lemma not_O_INR:(n:nat)~n=O->~(INR n)==R0.
+Intros;Cut (INR n)==R0->n=O.
+Tauto.
+Elim n;Intros;Auto with zarith real.
+Rewrite (S_INR n0) in H1;Generalize (Rplus_Ropp (INR n0) R1 H1);Intro;
+ Generalize (tech_Rplus (INR n0) R1 (INR_le n0) Rlt_R0_R1);Intro;
+ ElimType False;Auto with zarith real.
+Save. 
+
+(**********************************************************) 
+(*       Injection from Z to R                            *)
+(**********************************************************)
+
+(**********)
+Definition INZ:=inject_nat.
+
+(**********)
+Lemma INR_IZR_INZ:(n:nat)(INR n)==(IZR (INZ n)).
+Induction n;Auto with zarith real.
+Intros;Rewrite S_INR;Simpl;Rewrite bij1;Rewrite <-S_INR;Auto with zarith real.
+Save.
+
+(**********)
+Lemma plus_IZR:(z,t:Z)(IZR (Zplus z t))==(Rplus (IZR z) (IZR t)). 
+Destruct z;
+ [Simpl;Intro; Elim (Rplus_ne (IZR t)); Intros a b; Rewrite b; Auto with zarith real|
+ Destruct t|Destruct t].
+Simpl;Elim (Rplus_ne (INR (convert p))); Intros a b; Rewrite a; Auto with zarith real.
+Simpl;Intro;Rewrite <- (plus_INR (convert p) (convert p0));
+ Rewrite (convert_add p p0);Trivial with zarith real.
+Unfold Zplus;Intro;Simpl;
+ Generalize (refl_equal relation (compare p p0 EGAL));
+ Pattern 2 3 (compare p p0 EGAL);Case (compare p p0 EGAL);Intro.
+Rewrite (compare_convert_EGAL p p0 H);
+ Rewrite (Rplus_Ropp_r (INR (convert p0)));Auto with zarith real.
+Simpl;Rewrite (true_sub_convert p0 p (ZC2 p p0 H));
+ Rewrite (minus_INR (convert p0) (convert p) 
+  (lt_le_weak (convert p) (convert p0) 
+   (compare_convert_INFERIEUR p p0 H)));
+ Rewrite (Ropp_distr2 (INR (convert p0)) (INR (convert p)));
+ Unfold Rminus;Trivial with zarith real.
+Simpl;Rewrite (true_sub_convert p p0 H);
+ Rewrite (minus_INR (convert p) (convert p0));[Unfold Rminus;Trivial with zarith real|
+ Generalize (compare_convert_SUPERIEUR p p0 H);Intro;Unfold gt in H0;
+  Apply (lt_le_weak (convert p0) (convert p) H0)].
+Simpl;Elim (Rplus_ne (Ropp (INR (convert p)))); Intros a b; 
+ Rewrite a; Auto with zarith real.
+Intro;Rewrite (Zplus_sym (NEG p) (POS p0));
+ Rewrite (Rplus_sym (IZR (NEG p)) (IZR (POS p0)));
+ Unfold Zplus;Simpl;
+ Generalize (refl_equal relation (compare p0 p EGAL));
+ Pattern 2 3 (compare p0 p EGAL);Case (compare p0 p EGAL);Intro.
+Rewrite (compare_convert_EGAL p0 p H);
+ Rewrite (Rplus_Ropp_r (INR (convert p)));Auto with zarith real.
+Simpl;Rewrite (true_sub_convert p p0 (ZC2 p0 p H));
+ Rewrite (minus_INR (convert p) (convert p0) 
+  (lt_le_weak (convert p0) (convert p) 
+   (compare_convert_INFERIEUR p0 p H)));
+ Rewrite (Ropp_distr2 (INR (convert p)) (INR (convert p0)));
+ Unfold Rminus;Trivial with zarith real.
+Simpl;Rewrite (true_sub_convert p0 p H);
+ Rewrite (minus_INR (convert p0) (convert p));[Unfold Rminus;Trivial with zarith real|
+ Generalize (compare_convert_SUPERIEUR p0 p H);Intro;Unfold gt in H0;
+  Apply (lt_le_weak (convert p) (convert p0) H0)].
+Simpl;Intro;
+ Rewrite <-(Ropp_distr1 (INR (convert p)) (INR (convert p0)));
+ Rewrite <- (plus_INR (convert p) (convert p0));
+ Rewrite (convert_add p p0);Trivial with zarith real.
+Save.
+
+(**********)
+Lemma Ropp_Ropp_IZR:(z:Z)(IZR (`-z`))==(Ropp (IZR z)).
+Induction z; Simpl.
+Apply sym_eqT; Apply Ropp_O.
+Trivial with zarith real.
+Intro;Rewrite (Ropp_Ropp (INR (convert p)));Trivial with zarith real.
+Save.
+
+(**********)
+Lemma Z_R_minus:(z1,z2:Z)
+  (Rminus (IZR z1) (IZR z2))==(IZR (Zminus z1 z2)).
+Unfold Rminus; Unfold Zminus; Intros; Apply sym_eqT;
+ Rewrite <-(Ropp_Ropp_IZR z2);Apply plus_IZR.
+Save. 
+
+(**********)
+Lemma lt_O_IZR:(z:Z)(Rlt R0 (IZR z))->(Zlt ZERO z). 
+Induction z; Simpl; Intros.
+Generalize (Rlt_antirefl R0);Intro;ElimType False;Auto with zarith real.
+Unfold Zlt;Simpl;Trivial with zarith real.
+Absurd (Rlt R0 (Ropp (INR (convert p))));Auto with zarith real.
+Apply (Rlt_antisym (Ropp (INR (convert p))));
+ Apply (Rgt_RoppO (INR (convert p)));Unfold Rgt;
+ Cut (~(INR (convert p))==R0).
+Intro;Generalize (not_INR_O (convert p) H0);Elim (convert p).
+Intro;Absurd O=O;Auto with zarith real.
+Intros;Rewrite (S_INR n);Apply (Rlt_r_plus_R1 (INR n) (INR_le n)).
+Apply (imp_not_Req (INR (convert p)) R0);
+ Fold (Rgt (Ropp (INR (convert p))) R0) in H;
+ Generalize (Rgt_RoppO (Ropp (INR (convert p))) H);Intro;
+ Rewrite (Ropp_Ropp (INR (convert p))) in H0;Left;Assumption.
+Save.
+
+(**********)
+Lemma lt_IZR:(z1,z2:Z)(Rlt (IZR z1) (IZR z2))->(`z1<z2`).
+Intros;Fold (Rgt (IZR z2) (IZR z1)) in H;
+ Generalize (Rgt_minus (IZR z2) (IZR z1) H);Intro;Unfold Rgt in H0;
+ Rewrite (Z_R_minus z2 z1) in H0;
+ Generalize (lt_O_IZR `z2-z1` H0);Intro;Omega.
+Save.
+
+(**********)
+Lemma eq_IZR_R0:(z:Z)(IZR z)==R0->`z=0`.
+Destruct z; Auto with zarith real;
+ [ Simpl; Intros; ElimType False | Simpl; Intros; ElimType False ].
+Absurd (INR (convert p))==R0; Auto with zarith real.
+Apply (not_O_INR (convert p));Red; Intro;Clear H;Unfold convert in H0;
+ Generalize H0; Elim p;Intros.
+Simpl in H1;Absurd (S (positive_to_nat p0 (2)))=(0); Auto with zarith real.
+Simpl in H1;Cut (2)=(plus (1) (1)); Auto with zarith real.
+Intro; Rewrite H2 in H1;Rewrite (ZL2 p0 (1)) in H1;Clear H2;
+ Cut (positive_to_nat p0 (1))=(0);Auto with zarith real.
+Simpl in H1;Absurd (1)=(0); Auto with zarith real.
+Generalize (eq_Ropp (Ropp (INR (convert p))) R0 H);Intro;Clear H;
+ Rewrite (Ropp_Ropp (INR (convert p))) in H0;Rewrite Ropp_O in H0;
+ Absurd (INR (convert p))==R0; Auto with zarith real.
+Apply (not_O_INR (convert p));Red; Intro;Clear H0;
+ Unfold convert in H;Generalize H; Elim p;Intros.
+Simpl in H1;Absurd (S (positive_to_nat p0 (2)))=(0); Auto with zarith real.
+Simpl in H1;Cut (2)=(plus (1) (1)); Auto with zarith real.
+Intro; Rewrite H2 in H1;Rewrite (ZL2 p0 (1)) in H1;Clear H2;
+ Cut (positive_to_nat p0 (1))=(0);Auto with zarith real.
+Simpl in H0;Absurd (1)=(0); Auto with zarith real.
+Save.
+
+(**********)
+Lemma eq_IZR:(z1,z2:Z)(IZR z1)==(IZR z2)->z1=z2.
+Intros;Generalize (eq_Rminus (IZR z1) (IZR z2) H);
+ Rewrite (Z_R_minus z1 z2);Intro;Generalize (eq_IZR_R0 `z1-z2` H0);
+ Intro;Omega.
+Save.
+
+(**********)
+Lemma le_IZR_R1:(z:Z)(Rle (IZR z) R1)->(Zle z `1`).
+Induction z; Intros.
+Omega.
+Unfold Rle in H;Cut `(POS p) < 1`\/`(POS p) = 1`.
+Omega.
+Elim H;Intro.
+Left;Apply (Zlt_O_minus_lt `1` (POS p));Apply (lt_O_IZR `1-(POS p)`);
+ Cut (R1==(IZR `1`));Auto with zarith real. 
+Intro;Rewrite H1 in H0;Clear H1;Fold (Rgt (IZR `1`) (IZR (POS p))) in H0;
+ Generalize (Rgt_minus (IZR `1`) (IZR (POS p)) H0);Intro;
+ Unfold Rgt in H1;Rewrite (Z_R_minus `1` (POS p)) in H1;
+ Assumption.
+Right;Cut (R1==(IZR `1`));Auto with zarith real.
+Intro;Rewrite H1 in H0;Clear H1 H;Apply (eq_IZR (POS p) `1` H0).
+Unfold Rle in H;Cut `(NEG p) < 1`\/`(NEG p) = 1`.
+Omega.
+Elim H;Intro.
+Left;Apply (Zlt_O_minus_lt `1` (NEG p));Apply (lt_O_IZR `1-(NEG p)`);
+ Cut (R1==(IZR `1`));Auto with zarith real.
+Intro;Rewrite H1 in H0;Clear H1;Fold (Rgt (IZR `1`) (IZR (NEG p))) in H0;
+ Generalize (Rgt_minus (IZR `1`) (IZR (NEG p)) H0);Intro;
+ Unfold Rgt in H1;Rewrite (Z_R_minus `1` (NEG p)) in H1;
+ Assumption.
+Right;Cut (R1==(IZR `1`));Auto with zarith real.
+Intro;Rewrite H1 in H0;Clear H1 H;Apply (eq_IZR (NEG p) `1` H0).
+Save.
+
+(**********)
+Lemma single_z_r_R1:(r:R)(z,x:Z)(Rlt r (IZR z))->(Rle (IZR z) (Rplus r R1))
+  ->(Rlt r (IZR x))->(Rle (IZR x) (Rplus r R1))->z=x.
+Intros;Generalize (Rlt_Ropp r (IZR x) H1);Intro;
+ Generalize (Rle_Ropp (IZR x) (Rplus r R1) H2);Intro;Clear H1 H2;
+ Unfold Rgt in H3;
+ Generalize (Rle_sym2 (Ropp (Rplus r R1)) (Ropp (IZR x)) H4);
+ Intro;Clear H4;
+ Generalize (sum_inequa_Rle_lt (Ropp (Rplus r R1)) (Ropp (IZR x))
+   (Ropp r) r (IZR z) (Rplus r R1) H1 H3 H H0);Intro;Elim H2;Intros;
+ Clear H2 H H0 H3 H1;Rewrite (Rplus_sym (Ropp (IZR x)) (IZR z)) in 
+ H4;Rewrite (Rplus_sym (Ropp (IZR x)) (IZR z)) in H5;
+ Fold (Rminus (IZR z) (IZR x)) in H4;
+ Fold (Rminus (IZR z) (IZR x)) in H5;
+ Rewrite <-(Rplus_assoc (Ropp r) r R1) in H5;
+ Rewrite (Rplus_Ropp_l r) in H5;Rewrite (Ropp_distr1 r R1) in H4;
+ Rewrite (Rplus_sym (Ropp r) (Ropp R1)) in H4;
+ Rewrite (Rplus_assoc (Ropp R1) (Ropp r) r) in H4;
+ Rewrite (Rplus_Ropp_l r) in H4;Elim (Rplus_ne R1);Intros a b;Rewrite b in H5;
+ Clear a b;Elim (Rplus_ne (Ropp R1));Intros a b;Rewrite a in H4;
+ Clear a b;Rewrite (Z_R_minus z x) in H4;Rewrite (Z_R_minus z x) in H5;
+ Cut (R1==(IZR `1`));Auto with zarith real.
+Cut (Ropp R1)==(IZR `-1`);Auto with zarith real.
+Intros;Rewrite H0 in H5;Rewrite H in H4;Clear H H0;
+ Generalize (lt_IZR `-1` `z-x` H4);Intro;
+ Generalize (lt_IZR `z-x` `1` H5);Intro;Clear H4 H5;Omega.
+Save.
+
+(**********)
+Lemma tech_single_z_r_R1:(r:R)(z:Z)(Rlt r (IZR z))->
+ (Rle (IZR z) (Rplus r R1))->
+ (Ex [s:Z] (~s=z/\(Rlt r (IZR s))/\(Rle (IZR s) (Rplus r R1))))->False.
+Intros;Elim H1;Intros;Elim H2;Intros;Elim H4;Intros;Clear H1 H2 H4;
+ Generalize (single_z_r_R1 r z x H H0 H5 H6);Intro;Auto with zarith real.
+Save.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
new file mode 100644
index 000000000..97df55590
--- /dev/null
+++ b/theories/Reals/Rbasic_fun.v
@@ -0,0 +1,270 @@
+
+(* $Id$ *)
+
+(*********************************************************)
+(*           Complements for the real numbers            *)
+(*                                                       *)
+(*********************************************************)
+
+Require Export R_Ifp.
+
+(*******************************)
+(*           Rmin              *)
+(*******************************)
+
+(*********)
+Definition Rmin :R->R->R:=[x,y:R]
+  Cases (total_order_Rle x y) of 
+    (leftT _)  => x
+  | (rightT _) => y
+  end.
+
+(*********)
+Lemma Rmin_Rgt:(r1,r2,r:R)(Rgt (Rmin r1 r2) r)<->
+    ((Rgt r1 r)/\(Rgt r2 r)).
+Intros;Split.
+Unfold Rmin;Case (total_order_Rle r1 r2);Intros.
+Split;Auto.
+Unfold Rgt in H;Unfold Rgt;Apply (Rlt_le_trans r r1 r2 H r0).
+Split;Auto.
+Generalize (not_Rle r1 r2 n);Intro;Clear n;
+ Apply (Rgt_trans r1 r2 r H0 H).
+Intro;Elim H;Intros;Clear H;Unfold Rmin;Case (total_order_Rle r1 r2);
+ Intros;Auto.
+Save.
+
+(*******************************)
+(*           Rabsolu           *)
+(*******************************)
+
+(*********)
+Lemma case_Rabsolu:(r:R)(sumboolT (Rlt r R0) (Rge r R0)). 
+Intro;Generalize (total_order_Rle R0 r);Intro;Elim X;Intro;Clear X.
+Right;Apply (Rle_sym1 R0 r y).
+Left;Fold (Rgt R0 r);Apply (not_Rle R0 r y).
+Save.
+
+(*********)
+Definition Rabsolu:R->R:=
+      [r:R](Cases (case_Rabsolu r) of
+              (leftT  _) => (Ropp r)
+             |(rightT _) => r
+            end).
+
+(*********)
+Lemma Rabsolu_R0:(Rabsolu R0)==R0.
+Unfold Rabsolu;Case (case_Rabsolu R0);Auto;Intro.
+Generalize (Rlt_antirefl R0);Intro;ElimType False;Auto.
+Save.
+
+(*********)
+Lemma Rabsolu_no_R0:(r:R)~r==R0->~(Rabsolu r)==R0.
+Intros;Unfold Rabsolu;Case (case_Rabsolu r);Intro;Auto.
+Apply Ropp_neq;Auto.
+Save.
+
+(*********)
+Lemma Rabsolu_pos:(x:R)(Rle R0 (Rabsolu x)).
+Intros;Unfold Rabsolu;Case (case_Rabsolu x);Intro.
+Generalize (Rlt_Ropp x R0 r);Intro;Unfold Rgt in H;
+ Rewrite Ropp_O in H;Unfold Rle;Left;Assumption.
+Apply Rle_sym2;Assumption.
+Save.
+
+(*********)
+Lemma Rabsolu_pos_lt:(x:R)(~x==R0)->(Rlt R0 (Rabsolu x)).
+Intros;Generalize (Rabsolu_pos x);Intro;Unfold Rle in H0;
+ Elim H0;Intro;Auto.
+ElimType False;Clear H0;Elim H;Clear H;Generalize H1;
+ Unfold Rabsolu;Case (case_Rabsolu x);Intros;Auto.
+Clear r H1; Generalize (Rplus_plus_r x R0 (Ropp x) H0);
+ Rewrite (let (H1,H2)=(Rplus_ne x) in H1);Rewrite (Rplus_Ropp_r x);Trivial.
+Save.
+
+(*********)
+Lemma Rabsolu_minus_sym:(x,y:R)
+ (Rabsolu (Rminus x y))==(Rabsolu (Rminus y x)).
+Intros;Unfold Rabsolu;Case (case_Rabsolu (Rminus x y)); 
+ Case (case_Rabsolu (Rminus y x));Intros.
+ Generalize (Rminus_lt y x r);Generalize (Rminus_lt x y r0);Intros;
+ Generalize (Rlt_antisym x y H);Intro;ElimType False;Auto.
+Rewrite (Ropp_distr2 x y);Trivial.
+Rewrite (Ropp_distr2 y x);Trivial.
+Unfold Rge in r r0;Elim r;Elim r0;Intros;Clear r r0.
+Generalize (Rgt_RoppO (Rminus x y) H);Rewrite (Ropp_distr2 x y);
+ Intro;Unfold Rgt in H0;Generalize (Rlt_antisym R0 (Rminus y x) H0);
+ Intro;ElimType False;Auto.
+Rewrite (Rminus_eq x y H);Trivial.
+Rewrite (Rminus_eq y x H0);Trivial.
+Rewrite (Rminus_eq y x H0);Trivial.
+Save.
+
+(*********)
+Lemma Rabsolu_mult:(x,y:R)
+ (Rabsolu (Rmult x y))==(Rmult (Rabsolu x) (Rabsolu y)).
+Intros;Unfold Rabsolu;Case (case_Rabsolu (Rmult x y));
+ Case (case_Rabsolu x);Case (case_Rabsolu y);Intros;Auto.
+Generalize (Rlt_anti_monotony y x R0 r r0);Intro;
+ Rewrite (Rmult_Or y) in H;Generalize (Rlt_antisym (Rmult x y) R0 r1);
+ Intro;Unfold Rgt in H;ElimType False;Rewrite (Rmult_sym y x) in H;
+ Auto.
+Rewrite (Ropp_mul1 x y);Trivial. 
+Rewrite (Rmult_sym x (Ropp y));Rewrite (Ropp_mul1 y x);
+ Rewrite (Rmult_sym  x y);Trivial.
+Unfold Rge in r r0;Elim r;Elim r0;Clear r r0;Intros;Unfold Rgt in H H0.
+Generalize (Rlt_monotony x R0 y H H0);Intro;Rewrite (Rmult_Or x) in H1;
+ Generalize (Rlt_antisym (Rmult x y) R0 r1);Intro;ElimType False;Auto.
+Rewrite H in r1;Rewrite (Rmult_Ol y) in r1;Generalize (Rlt_antirefl R0);
+ Intro;ElimType False;Auto.
+Rewrite H0 in r1;Rewrite (Rmult_Or x) in r1;Generalize (Rlt_antirefl R0);
+ Intro;ElimType False;Auto.
+Rewrite H0 in r1;Rewrite (Rmult_Or x) in r1;Generalize (Rlt_antirefl R0);
+ Intro;ElimType False;Auto.
+Rewrite (Ropp_mul2 x y);Trivial.
+Unfold Rge in r r1;Elim r;Elim r1;Clear r r1;Intros;Unfold Rgt in H0 H.
+Generalize (Rlt_monotony y x R0 H0 r0);Intro;Rewrite (Rmult_Or y) in H1;
+ Rewrite (Rmult_sym y x) in H1; 
+ Generalize (Rlt_antisym (Rmult x y) R0 H1);Intro;ElimType False;Auto.
+Generalize (imp_not_Req x R0 (or_introl (Rlt x R0) (Rgt x R0) r0));
+ Generalize (imp_not_Req y R0 (or_intror (Rlt y R0) (Rgt y R0) H0));Intros;
+ Generalize (without_div_Od x y H);Intro;Elim H3;Intro;ElimType False;
+ Auto.  
+Rewrite H0 in H;Rewrite (Rmult_Or x) in H;Unfold Rgt in H;
+ Generalize (Rlt_antirefl R0);Intro;ElimType False;Auto.
+Rewrite H0;Rewrite (Rmult_Or x);Rewrite (Rmult_Or (Ropp x));Trivial.
+Unfold Rge in r0 r1;Elim r0;Elim r1;Clear r0 r1;Intros;Unfold Rgt in H0 H.
+Generalize (Rlt_monotony x y R0 H0 r);Intro;Rewrite (Rmult_Or x) in H1;
+ Generalize (Rlt_antisym (Rmult x y) R0 H1);Intro;ElimType False;Auto.
+Generalize (imp_not_Req y R0 (or_introl (Rlt y R0) (Rgt y R0) r));
+ Generalize (imp_not_Req R0 x (or_introl (Rlt R0 x) (Rgt R0 x) H0));Intros;
+ Generalize (without_div_Od x y H);Intro;Elim H3;Intro;ElimType False;
+ Auto.  
+Rewrite H0 in H;Rewrite (Rmult_Ol y) in H;Unfold Rgt in H;
+ Generalize (Rlt_antirefl R0);Intro;ElimType False;Auto.
+Rewrite H0;Rewrite (Rmult_Ol y);Rewrite (Rmult_Ol (Ropp y));Trivial.
+Save.
+
+(*********)
+Lemma Rabsolu_Rinv:(r:R)(~r==R0)->(Rabsolu (Rinv r))==
+                                  (Rinv (Rabsolu r)).
+Intro;Unfold Rabsolu;Case (case_Rabsolu r);
+ Case (case_Rabsolu (Rinv r));Auto;Intros.
+Apply Ropp_Rinv;Auto.
+Generalize (Rlt_Rinv2 r r1);Intro;Unfold Rge in r0;Elim r0;Intros.
+Unfold Rgt in H1;Generalize (Rlt_antisym R0 (Rinv r) H1);Intro; 
+ ElimType False;Auto.
+Generalize 
+  (imp_not_Req (Rinv r) R0 
+   (or_introl (Rlt (Rinv r) R0) (Rgt (Rinv r) R0) H0));Intro;
+ ElimType False;Auto.
+Unfold Rge in r1;Elim r1;Clear r1;Intro.
+Unfold Rgt in H0;Generalize (Rlt_antisym R0 (Rinv r)  
+     (Rlt_Rinv r H0));Intro;ElimType False;Auto.
+ElimType False;Auto.
+Save. 
+
+(*********)
+Lemma Rabsolu_triang:(a,b:R)(Rle (Rabsolu (Rplus a b)) 
+                                (Rplus (Rabsolu a) (Rabsolu b))).
+Intros a b;Unfold Rabsolu;Case (case_Rabsolu (Rplus a b));
+ Case (case_Rabsolu a);Case (case_Rabsolu b);Intros.
+Apply (eq_Rle (Ropp (Rplus a b)) (Rplus (Ropp a) (Ropp b)));
+ Rewrite (Ropp_distr1 a b);Reflexivity.
+(**)
+Rewrite (Ropp_distr1 a b);
+ Apply (Rle_compatibility (Ropp a) (Ropp b) b);
+ Unfold Rle;Unfold Rge in r;Elim r;Intro.
+Left;Unfold Rgt in H;Generalize (Rlt_compatibility (Ropp b) R0 b H);
+ Intro;Elim (Rplus_ne (Ropp b));Intros v w;Rewrite v in H0;Clear v w;
+ Rewrite (Rplus_Ropp_l b) in H0;Apply (Rlt_trans (Ropp b) R0 b H0 H).
+Right;Rewrite H;Apply Ropp_O.
+(**)
+Rewrite (Ropp_distr1 a b);
+ Rewrite (Rplus_sym (Ropp a) (Ropp b));
+ Rewrite (Rplus_sym a (Ropp b));
+ Apply (Rle_compatibility (Ropp b) (Ropp a) a);
+ Unfold Rle;Unfold Rge in r0;Elim r0;Intro.
+Left;Unfold Rgt in H;Generalize (Rlt_compatibility (Ropp a) R0 a H);
+ Intro;Elim (Rplus_ne (Ropp a));Intros v w;Rewrite v in H0;Clear v w;
+ Rewrite (Rplus_Ropp_l a) in H0;Apply (Rlt_trans (Ropp a) R0 a H0 H).
+Right;Rewrite H;Apply Ropp_O.
+(**)
+ElimType False;Generalize (Rge_plus_plus_r a b R0 r);Intro;
+ Elim (Rplus_ne a);Intros v w;Rewrite v in H;Clear v w; 
+ Generalize (Rge_trans (Rplus a b) a R0 H r0);Intro;Clear H;
+ Unfold Rge in H0;Elim H0;Intro;Clear H0.
+Unfold Rgt in H;Generalize (Rlt_antisym (Rplus a b) R0 r1);Intro;Auto.
+Absurd (Rplus a b)==R0;Auto.
+Apply (imp_not_Req (Rplus a b) R0);Left;Assumption.
+(**)
+ElimType False;Generalize (Rlt_compatibility a b R0 r);Intro;
+ Elim (Rplus_ne a);Intros v w;Rewrite v in H;Clear v w;
+ Generalize (Rlt_trans (Rplus a b) a R0 H r0);Intro;Clear H;
+ Unfold Rge in r1;Elim r1;Clear r1;Intro.
+Unfold Rgt in H;
+ Generalize (Rlt_trans (Rplus a b) R0 (Rplus a b) H0 H);Intro;
+ Apply (Rlt_antirefl (Rplus a b));Assumption.
+Rewrite H in H0;Apply (Rlt_antirefl R0);Assumption.
+(**)
+Rewrite (Rplus_sym a b);Rewrite (Rplus_sym (Ropp a) b);
+ Apply (Rle_compatibility b a (Ropp a));
+ Apply (Rminus_le a (Ropp a));Unfold Rminus;Rewrite (Ropp_Ropp a);
+ Generalize (Rlt_compatibility a a R0 r0);Clear r r1;Intro;
+ Elim (Rplus_ne a);Intros v w;Rewrite v in H;Clear v w;
+ Generalize (Rlt_trans (Rplus a a) a R0 H r0);Intro;
+ Apply (Rlt_le (Rplus a a) R0 H0).
+(**)
+Apply (Rle_compatibility a b (Ropp b));
+ Apply (Rminus_le b (Ropp b));Unfold Rminus;Rewrite (Ropp_Ropp b);
+ Generalize (Rlt_compatibility b b R0 r);Clear r0 r1;Intro;
+ Elim (Rplus_ne b);Intros v w;Rewrite v in H;Clear v w;
+ Generalize (Rlt_trans (Rplus b b) b R0 H r);Intro;
+ Apply (Rlt_le (Rplus b b) R0 H0).
+(**)
+Unfold Rle;Right;Reflexivity.
+Save.
+
+(*********)
+Lemma Rabsolu_triang_inv:(a,b:R)(Rle (Rminus (Rabsolu a) (Rabsolu b))
+                                     (Rabsolu (Rminus a b))).
+Intros;Unfold Rabsolu;Case (case_Rabsolu a);Case (case_Rabsolu b);
+ Case (case_Rabsolu (Rminus a b));Intros.
+Unfold Rle;Right;Rewrite (Ropp_distr2 a b);Unfold Rminus;
+ Rewrite Ropp_Ropp;Apply Rplus_sym.
+Unfold 1 Rminus;Rewrite Ropp_Ropp;Rewrite Rplus_sym;
+ Fold (Rminus b a);Generalize (minus_Rge a b r);Intro;
+ Generalize (Rle_sym2 b a H);Intro;Generalize (Rle_minus b a H0);
+ Intro;Generalize (Rle_sym2 R0 (Rminus a b) r);Intro;
+ Apply (Rle_trans (Rminus b a) R0 (Rminus a b) H1 H2).
+Rewrite (Ropp_distr2 a b);Unfold Rminus;
+ Rewrite (Rplus_sym b (Ropp a));Apply Rle_compatibility; 
+ Unfold Rge in r0;Elim r0;Intros.
+Unfold Rle;Left;Generalize (Rgt_RoppO b H);Intro;Unfold Rgt in H;
+ Apply (Rlt_trans (Ropp b) R0 b H0 H).
+Unfold Rle;Right;Rewrite H;Apply Ropp_O.
+Generalize (minus_Rge a b r);Intro;
+ Generalize (Rge_trans a b R0 H r0);Intro;
+ Generalize (Rlt_antisym a R0 r1);Intro; 
+ Unfold Rge in H0;Elim H0;Intro.
+Unfold Rgt in H2;ElimType False;Auto.
+Rewrite H2 in r1;Generalize (Rlt_antirefl R0);Intro;ElimType False;
+ Auto.
+Generalize (Rminus_lt a b r);Intro;Generalize (Rlt_trans a b R0 H r0);
+ Intro;Unfold Rge in r1;Elim r1;Intro.
+Generalize (Rlt_antisym a R0 H0);Intro;Unfold Rgt in H1;ElimType False;
+ Auto.
+Rewrite H1 in H0;Generalize (Rlt_antirefl R0);Intro;ElimType False;
+ Auto.
+Unfold Rminus;Apply Rle_compatibility;Rewrite Ropp_Ropp;
+ Generalize (Rlt_compatibility (Ropp b) b R0 r0);Intro; 
+ Rewrite Rplus_Ropp_l in H;
+ Rewrite (let (H1,H2)=(Rplus_ne (Ropp b)) in H1) in H;
+ Generalize (Rlt_trans b R0 (Ropp b) r0 H);Intro;
+ Apply Rlt_le;Assumption.
+Generalize (Rlt_compatibility (Ropp (Rminus a b)) (Rminus a b)  R0 r);
+Intro; Rewrite Rplus_Ropp_l in H;
+ Rewrite (let (H1,H2)=(Rplus_ne (Ropp (Rminus a b))) in H1) in H;
+ Generalize (Rlt_trans (Rminus a b) R0 (Ropp (Rminus a b)) r H);Intro;
+ Apply Rlt_le;Assumption.
+Unfold Rle;Right;Trivial.  
+Save.
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
new file mode 100644
index 000000000..d36ca5897
--- /dev/null
+++ b/theories/Reals/Rderiv.v
@@ -0,0 +1,497 @@
+
+(* $Id$ *)
+
+(*********************************************************)
+(*      Definition of the derivative,continuity          *)
+(*                                                       *)
+(*********************************************************)
+Require Export Rfunctions.
+Require Classical_Pred_Type.
+Require Omega.
+
+(*********)
+Definition D_x:(R->Prop)->R->R->Prop:=[D:R->Prop][y:R][x:R]
+       (D x)/\(~y==x).
+
+(*********)
+Definition continue_in:(R->R)->(R->Prop)->R->Prop:=
+       [f:R->R; D:R->Prop; x0:R](limit1_in f (D_x D x0) (f x0) x0).
+
+(*********)
+Definition D_in:(R->R)->(R->R)->(R->Prop)->R->Prop:=
+  [f:R->R; d:R->R; D:R->Prop; x0:R](limit1_in 
+    [x:R] (Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0))) 
+    (D_x D x0) (d x0) x0).
+
+(*********)
+Lemma cont_deriv:(f,d:R->R;D:R->Prop;x0:R)
+         (D_in f d D x0)->(continue_in f D x0).
+Unfold continue_in;Unfold D_in;Unfold limit1_in;Unfold limit_in;Simpl;
+ Intros;Cut (Rgt (Rminus eps (Rabsolu (d x0))) R0)\/
+            ~(Rgt (Rminus eps (Rabsolu (d x0))) R0).
+Intro;Elim H1;Clear H1;Intro.
+Elim (H (Rminus eps (Rabsolu (d x0))) H1);Clear H;Intros;Elim H;Clear H;
+ Intros;Split with (Rmin R1 x);Split.
+Generalize Rlt_R0_R1;Intro Hyp;Fold (Rgt R1 R0) in Hyp;
+ Elim (Rmin_Rgt R1 x R0);Intros a b;
+ Apply (b (conj (Rgt R1 R0) (Rgt x R0) (Hyp) H)).
+Intros; Elim H3;Clear H3;Intros;
+ Generalize (let (H1,H2)=(Rmin_Rgt R1 x (R_dist x1 x0)) in H1);
+ Unfold Rgt;Intro;Elim (H5 H4);Clear H5;Intros;
+ Generalize (H2 x1 (conj (D_x D x0 x1) (Rlt (R_dist x1 x0) x) H3 H6));
+ Clear H2;Intro;Unfold D_x in H3;Elim H3;Intros;
+ Generalize (sym_not_eqT R x0 x1 H8);Clear H8;Intro H8;
+ Generalize (Rminus_eq_contra x1 x0 H8);Clear H7 H8;
+ Intro;Generalize H2;Pattern 1 (d x0); 
+ Rewrite <-(let (H1,H2)=(Rmult_ne (d x0)) in H2);
+ Rewrite <-(Rinv_l (Rminus x1 x0) H7); Unfold R_dist;Unfold 1 Rminus;
+ Rewrite (Rmult_sym (Rminus (f x1) (f x0)) (Rinv (Rminus x1 x0)));
+ Rewrite (Rmult_sym (Rmult (Rinv (Rminus x1 x0)) (Rminus x1 x0)) (d x0));
+ Rewrite <-(Ropp_mul1 (d x0) (Rmult (Rinv (Rminus x1 x0)) (Rminus x1 x0)));
+ Rewrite (Rmult_sym (Ropp (d x0))
+                    (Rmult (Rinv (Rminus x1 x0)) (Rminus x1 x0)));
+ Rewrite (Rmult_assoc (Rinv (Rminus x1 x0)) (Rminus x1 x0) (Ropp (d x0)));
+ Rewrite <-(Rmult_Rplus_distr (Rinv (Rminus x1 x0)) (Rminus (f x1) (f x0))
+                   (Rmult (Rminus x1 x0) (Ropp (d x0))));
+ Rewrite (Rabsolu_mult (Rinv (Rminus x1 x0))
+                       (Rplus (Rminus (f x1) (f x0))
+                              (Rmult (Rminus x1 x0) (Ropp (d x0)))));
+ Clear H2;Intro;Generalize (Rlt_monotony (Rabsolu (Rminus x1 x0)) 
+        (Rmult (Rabsolu (Rinv (Rminus x1 x0)))
+           (Rabsolu
+             (Rplus (Rminus (f x1) (f x0))
+               (Rmult (Rminus x1 x0) (Ropp (d x0))))))
+         (Rminus eps (Rabsolu (d x0)))
+        (Rabsolu_pos_lt (Rminus x1 x0) H7) H2); 
+ Rewrite <-(Rmult_assoc (Rabsolu (Rminus x1 x0)) 
+                 (Rabsolu (Rinv (Rminus x1 x0)))
+               (Rabsolu
+           (Rplus (Rminus (f x1) (f x0))
+             (Rmult (Rminus x1 x0) (Ropp (d x0)))))); 
+ Rewrite (Rabsolu_Rinv (Rminus x1 x0) H7);
+ Rewrite (Rinv_r (Rabsolu (Rminus x1 x0)) 
+                 (Rabsolu_no_R0 (Rminus x1 x0) H7));
+ Rewrite (let (H1,H2)=(Rmult_ne (Rabsolu
+         (Rplus (Rminus (f x1) (f x0))
+           (Rmult (Rminus x1 x0) (Ropp (d x0)))))) in H2);
+ Unfold 4 Rminus;
+ Rewrite (Rmult_Rplus_distr (Rabsolu (Rminus x1 x0)) eps 
+                (Ropp (Rabsolu (d x0))));
+ Rewrite (Rmult_sym (Rabsolu (Rminus x1 x0)) (Ropp (Rabsolu (d x0))));
+ Rewrite (Ropp_mul1 (Rabsolu (d x0)) (Rabsolu (Rminus x1 x0)));
+ Rewrite <-(Rabsolu_mult (d x0) (Rminus x1 x0)); 
+ Generalize (Rabsolu_triang_inv (Rminus (f x1) (f x0))
+         (Rmult (Rminus x1 x0) (d x0)));Intro;
+ Rewrite (Rmult_sym (Rminus x1 x0) (Ropp (d x0)));
+ Rewrite (Ropp_mul1 (d x0) (Rminus x1 x0));
+ Fold (Rminus (Rminus (f x1) (f x0)) (Rmult (d x0) (Rminus x1 x0)));
+ Rewrite (Rmult_sym (Rminus x1 x0) (d x0)) in H8;
+ Clear H2;Intro;Generalize (Rle_lt_trans 
+           (Rminus (Rabsolu (Rminus (f x1) (f x0)))
+           (Rabsolu (Rmult (d x0) (Rminus x1 x0))))
+          (Rabsolu
+           (Rminus (Rminus (f x1) (f x0)) (Rmult (d x0) (Rminus x1 x0))))
+          (Rplus (Rmult (Rabsolu (Rminus x1 x0)) eps)
+           (Ropp (Rabsolu (Rmult (d x0) (Rminus x1 x0))))) H8 H2);
+ Unfold 1 Rminus;
+ Rewrite (Rplus_sym (Rabsolu (Rminus (f x1) (f x0))) 
+                    (Ropp (Rabsolu (Rmult (d x0) (Rminus x1 x0)))));
+ Rewrite (Rplus_sym (Rmult (Rabsolu (Rminus x1 x0)) eps)
+                    (Ropp (Rabsolu (Rmult (d x0) (Rminus x1 x0)))));
+ Clear H8 H2;Intro;Generalize (Rlt_anti_compatibility  
+            (Ropp (Rabsolu (Rmult (d x0) (Rminus x1 x0)))) 
+            (Rabsolu (Rminus (f x1) (f x0)))
+            (Rmult (Rabsolu (Rminus x1 x0)) eps) H2);
+ Clear H2;Intro;Unfold Rgt in H0;Unfold R_dist in H5;
+ Generalize (Rlt_monotony eps (Rabsolu (Rminus x1 x0)) R1 H0 H5);
+ Rewrite (let (H1,H2)=(Rmult_ne eps) in H1); 
+ Rewrite (Rmult_sym eps (Rabsolu (Rminus x1 x0)));
+ Intro;Apply (Rlt_trans (Rabsolu (Rminus (f x1) (f x0)))
+                        (Rmult (Rabsolu (Rminus x1 x0)) eps)
+                        eps H2 H8).
+(**)
+Elim (H eps H0);Clear H;Intros;Elim H;Clear H;Intros;
+ Split with (Rmin (Rmin (Rinv (Rplus R1 R1)) x) 
+              (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))))));
+ Split.
+Cut (Rgt (Rmin (Rinv (Rplus R1 R1)) x) R0).
+Cut (Rgt (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))))) R0).
+Intros;Elim (Rmin_Rgt (Rmin (Rinv (Rplus R1 R1)) x) 
+            (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))))) R0);
+ Intros a b;
+ Apply (b (conj (Rgt (Rmin (Rinv (Rplus R1 R1)) x) R0)
+       (Rgt (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))))) R0)
+        H4 H3)).
+Generalize (Rgt_not_le (Rminus eps (Rabsolu (d x0))) R0 H1);Intro;
+ Generalize (Rminus_le eps (Rabsolu (d x0)) H3);Intro;Generalize H0;
+ Intro;Unfold Rgt in H5;Generalize (Rlt_le_trans R0 eps (Rabsolu (d x0))
+                                          H5 H4);Intro;
+ Fold (Rgt (Rabsolu (d x0)) R0) in H6;Cut ~(Rplus R1 R1)==R0.
+Intro;Generalize (Rabsolu_pos_lt (Rplus R1 R1) H7);Intro; 
+ Fold (Rgt (Rabsolu (Rplus R1 R1)) R0) in H8;
+ Generalize (Rmult_gt (Rabsolu (Rplus R1 R1)) (Rabsolu (d x0)) H8 H6);
+ Intro;Unfold Rgt in H9; 
+  Rewrite <-(Rabsolu_mult (Rplus R1 R1) (d x0)) in H9;
+ Generalize (Rlt_Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))) H9);Intro;
+ Fold (Rgt (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0)))) R0) in H10; 
+ Apply (Rmult_gt eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0)))) H0 H10).
+Apply (imp_not_Req (Rplus R1 R1) R0).      
+Right;Unfold Rgt;Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H7);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H8;
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H7 H8).
+Elim (Rmin_Rgt (Rinv (Rplus R1 R1)) x R0);Intros a b;
+ Cut (Rlt R0 (Rplus R1 R1)).
+Intro;Generalize (Rlt_Rinv (Rplus R1 R1) H3);Intro;
+ Fold (Rgt (Rinv (Rplus R1 R1)) R0) in H4;
+ Apply (b (conj (Rgt (Rinv (Rplus R1 R1)) R0) (Rgt x R0) H4 H)).
+Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H3);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H4;
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H3 H4).
+Intros;Elim H3;Clear H3;Intros;
+ Generalize (let (H1,H2)=(Rmin_Rgt (Rmin (Rinv (Rplus R1 R1)) x)
+       (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0)))))
+       (R_dist x1 x0)) in H1);Unfold Rgt;Intro;Elim (H5 H4);Clear H5;
+ Intros;
+ Generalize (let (H1,H2)=(Rmin_Rgt (Rinv (Rplus R1 R1)) x
+          (R_dist x1 x0)) in H1);Unfold Rgt;Intro;Elim (H7 H5);Clear H7;
+ Intros;Clear H4 H5;
+ Generalize (H2 x1 (conj (D_x D x0 x1) (Rlt (R_dist x1 x0) x) H3 H8));
+ Clear H2;Intro;Unfold D_x in H3;Elim H3;Intros;
+ Generalize (sym_not_eqT R x0 x1 H5);Clear H5;Intro H5;
+ Generalize (Rminus_eq_contra x1 x0 H5);
+ Intro;Generalize H2;Pattern 1 (d x0); 
+ Rewrite <-(let (H1,H2)=(Rmult_ne (d x0)) in H2);
+ Rewrite <-(Rinv_l (Rminus x1 x0) H9); Unfold R_dist;Unfold 1 Rminus;
+ Rewrite (Rmult_sym (Rminus (f x1) (f x0)) (Rinv (Rminus x1 x0)));
+ Rewrite (Rmult_sym (Rmult (Rinv (Rminus x1 x0)) (Rminus x1 x0)) (d x0));
+ Rewrite <-(Ropp_mul1 (d x0) (Rmult (Rinv (Rminus x1 x0)) (Rminus x1 x0)));
+ Rewrite (Rmult_sym (Ropp (d x0))
+                    (Rmult (Rinv (Rminus x1 x0)) (Rminus x1 x0)));
+ Rewrite (Rmult_assoc (Rinv (Rminus x1 x0)) (Rminus x1 x0) (Ropp (d x0)));
+ Rewrite <-(Rmult_Rplus_distr (Rinv (Rminus x1 x0)) (Rminus (f x1) (f x0))
+                   (Rmult (Rminus x1 x0) (Ropp (d x0))));
+ Rewrite (Rabsolu_mult (Rinv (Rminus x1 x0))
+                       (Rplus (Rminus (f x1) (f x0))
+                              (Rmult (Rminus x1 x0) (Ropp (d x0)))));
+ Clear H2;Intro;Generalize (Rlt_monotony (Rabsolu (Rminus x1 x0)) 
+        (Rmult (Rabsolu (Rinv (Rminus x1 x0)))
+           (Rabsolu
+             (Rplus (Rminus (f x1) (f x0))
+               (Rmult (Rminus x1 x0) (Ropp (d x0)))))) eps 
+        (Rabsolu_pos_lt (Rminus x1 x0) H9) H2); 
+ Rewrite <-(Rmult_assoc (Rabsolu (Rminus x1 x0)) 
+                 (Rabsolu (Rinv (Rminus x1 x0)))
+               (Rabsolu
+           (Rplus (Rminus (f x1) (f x0))
+             (Rmult (Rminus x1 x0) (Ropp (d x0)))))); 
+ Rewrite (Rabsolu_Rinv (Rminus x1 x0) H9);
+ Rewrite (Rinv_r (Rabsolu (Rminus x1 x0)) 
+                 (Rabsolu_no_R0 (Rminus x1 x0) H9));
+ Rewrite (let (H1,H2)=(Rmult_ne (Rabsolu
+         (Rplus (Rminus (f x1) (f x0))
+           (Rmult (Rminus x1 x0) (Ropp (d x0)))))) in H2);
+ Generalize (Rabsolu_triang_inv (Rminus (f x1) (f x0))
+         (Rmult (Rminus x1 x0) (d x0)));Intro;
+ Rewrite (Rmult_sym (Rminus x1 x0) (Ropp (d x0)));
+ Rewrite (Ropp_mul1 (d x0) (Rminus x1 x0));
+ Fold (Rminus (Rminus (f x1) (f x0)) (Rmult (d x0) (Rminus x1 x0)));
+ Rewrite (Rmult_sym (Rminus x1 x0) (d x0)) in H10;
+ Clear H2;Intro;Generalize (Rle_lt_trans 
+           (Rminus (Rabsolu (Rminus (f x1) (f x0)))
+           (Rabsolu (Rmult (d x0) (Rminus x1 x0))))
+          (Rabsolu
+           (Rminus (Rminus (f x1) (f x0)) (Rmult (d x0) (Rminus x1 x0))))
+          (Rmult (Rabsolu (Rminus x1 x0)) eps) H10 H2);
+ Clear H2;Intro;
+ Generalize (Rlt_compatibility (Rabsolu (Rmult (d x0) (Rminus x1 x0)))
+   (Rminus (Rabsolu (Rminus (f x1) (f x0)))
+           (Rabsolu (Rmult (d x0) (Rminus x1 x0))))
+   (Rmult (Rabsolu (Rminus x1 x0)) eps) H2);
+ Unfold 2 Rminus;Rewrite (Rplus_sym (Rabsolu (Rminus (f x1) (f x0)))
+    (Ropp (Rabsolu (Rmult (d x0) (Rminus x1 x0)))));
+ Rewrite <-(Rplus_assoc (Rabsolu (Rmult (d x0) (Rminus x1 x0)))
+  (Ropp (Rabsolu (Rmult (d x0) (Rminus x1 x0)))) 
+  (Rabsolu (Rminus (f x1) (f x0))));
+ Rewrite (Rplus_Ropp_r (Rabsolu (Rmult (d x0) (Rminus x1 x0))));
+ Rewrite (let (H1,H2)=(Rplus_ne (Rabsolu (Rminus (f x1) (f x0)))) in H2);
+ Clear H2;Intro;Cut (Rlt (Rplus (Rabsolu (Rmult (d x0) (Rminus x1 x0)))
+           (Rmult (Rabsolu (Rminus x1 x0)) eps)) eps).
+Intro;Apply (Rlt_trans (Rabsolu (Rminus (f x1) (f x0))) 
+    (Rplus (Rabsolu (Rmult (d x0) (Rminus x1 x0)))
+            (Rmult (Rabsolu (Rminus x1 x0)) eps)) eps H2 H11). 
+Clear H2 H5 H3 H10;Cut (Rlt R0 (Rabsolu (d x0))).
+Intro;Unfold Rgt in H0;Generalize (Rlt_monotony eps (R_dist x1 x0)
+       (Rinv (Rplus R1 R1)) H0 H7);Clear H7;Intro;
+ Generalize (Rlt_monotony (Rabsolu (d x0)) (R_dist x1 x0) 
+    (Rmult eps (Rinv (Rabsolu (Rmult (Rplus R1 R1) (d x0))))) H2 H6);
+ Clear H6;Intro;Rewrite (Rmult_sym eps (R_dist x1 x0)) in H3; 
+ Unfold R_dist in H3 H5;
+ Rewrite <-(Rabsolu_mult (d x0) (Rminus x1 x0)) in H5;
+ Rewrite (Rabsolu_mult (Rplus R1 R1) (d x0)) in H5;
+ Cut ~(Rabsolu (Rplus R1 R1))==R0.
+Intro;Fold (Rgt (Rabsolu (d x0)) R0) in H2;
+ Rewrite (Rinv_Rmult (Rabsolu (Rplus R1 R1)) (Rabsolu (d x0))
+ H6 (imp_not_Req (Rabsolu (d x0)) R0 
+  (or_intror (Rlt (Rabsolu (d x0)) R0) (Rgt (Rabsolu (d x0)) R0) H2))) 
+  in H5;
+ Rewrite (Rmult_sym (Rabsolu (d x0)) (Rmult eps
+             (Rmult (Rinv (Rabsolu (Rplus R1 R1)))
+               (Rinv (Rabsolu (d x0)))))) in H5;
+ Rewrite <-(Rmult_assoc eps (Rinv (Rabsolu (Rplus R1 R1))) 
+   (Rinv (Rabsolu (d x0)))) in H5;
+ Rewrite (Rmult_assoc (Rmult eps (Rinv (Rabsolu (Rplus R1 R1))))
+    (Rinv (Rabsolu (d x0))) (Rabsolu (d x0))) in H5;
+ Rewrite (Rinv_l (Rabsolu (d x0)) (imp_not_Req (Rabsolu (d x0)) R0 
+  (or_intror (Rlt (Rabsolu (d x0)) R0) (Rgt (Rabsolu (d x0)) R0) H2))) 
+  in H5;
+ Rewrite (let (H1,H2)=(Rmult_ne (Rmult eps (Rinv (Rabsolu (Rplus R1 R1)))))
+   in H1) in H5;Cut (Rabsolu (Rplus R1 R1))==(Rplus R1 R1).
+Intro;Rewrite H7 in H5;
+ Generalize (Rplus_lt (Rabsolu (Rmult (d x0) (Rminus x1 x0)))
+        (Rmult eps (Rinv (Rplus R1 R1)))
+        (Rmult (Rabsolu (Rminus x1 x0)) eps)
+        (Rmult eps (Rinv (Rplus R1 R1))) H5 H3);Intro;
+ Rewrite eps2 in H10;Assumption.
+Unfold Rabsolu;Case (case_Rabsolu (Rplus R1 R1));Auto.
+ Intro;Cut (Rlt R0 (Rplus R1 R1)).
+Intro;Generalize (Rlt_antisym R0 (Rplus R1 R1) H7);Intro;ElimType False;
+ Auto.
+Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H7);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H10;
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H7 H10).
+Cut ~(Rplus R1 R1)==R0.
+Intro;Red;Intro;Apply (Rabsolu_no_R0 (Rplus R1 R1) H6);Auto.
+Apply (imp_not_Req (Rplus R1 R1) R0).      
+Right;Unfold Rgt;Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H6);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H7;
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H6 H7).
+Generalize (Rgt_not_le (Rminus eps (Rabsolu (d x0))) R0 H1);Intro;
+ Generalize (Rminus_le eps (Rabsolu (d x0)) H2);Intro;
+ Unfold Rgt in H0;Apply (Rlt_le_trans R0 eps (Rabsolu (d x0)) H0 H3).
+Apply classic.
+Save.
+
+(*********)
+Lemma Dconst:(D:R->Prop)(y:R)(x0:R)(D_in [x:R]y [x:R]R0 D x0).
+Unfold D_in;Intros;Unfold limit1_in;Unfold limit_in;Intros;Simpl;
+ Split with eps;Split;Auto.
+Intros;Rewrite (eq_Rminus y y (refl_eqT R y));
+ Rewrite Rmult_Ol;Unfold R_dist; 
+ Rewrite (eq_Rminus R0 R0 (refl_eqT R R0));Unfold Rabsolu;
+ Case (case_Rabsolu R0);Intro.
+Absurd (Rlt R0 R0);Auto.
+Red;Intro;Apply (Rlt_antirefl R0 H1).
+Unfold Rgt in H0;Assumption.
+Save.
+
+(*********)
+Lemma Dx:(D:R->Prop)(x0:R)(D_in [x:R]x [x:R]R1 D x0).
+Unfold D_in;Intros;Unfold limit1_in;Unfold limit_in;Intros;Simpl;
+  Split with eps;Split;Auto.
+Intros;Elim H0;Clear H0;Intros;Unfold D_x in H0;
+ Elim H0;Intros;
+ Rewrite (Rinv_r (Rminus x x0) (Rminus_eq_contra x x0 
+      (sym_not_eqT R x0 x H3)));
+ Unfold R_dist; 
+ Rewrite (eq_Rminus R1 R1 (refl_eqT R R1));Unfold Rabsolu;
+ Case (case_Rabsolu R0);Intro.
+Absurd (Rlt R0 R0);Auto.
+Red;Intro;Apply (Rlt_antirefl R0 r).
+Unfold Rgt in H;Assumption.
+Save. 
+
+(*********)
+Lemma Dadd:(D:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R)
+  (D_in f df D x0)->(D_in g dg D x0)->
+  (D_in [x:R](Rplus (f x) (g x)) [x:R](Rplus (df x) (dg x)) D x0).
+Unfold D_in;Intros;Generalize (limit_plus 
+   [x:R](Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0)))
+   [x:R](Rmult  (Rminus (g x) (g x0)) (Rinv (Rminus x x0))) 
+   (D_x D x0) (df x0) (dg x0) x0 H H0);Clear H H0;
+ Unfold limit1_in;Unfold limit_in;Simpl;Intros;
+ Elim (H eps H0);Clear H;Intros;Elim H;Clear H;Intros;
+ Split with x;Split;Auto;Intros;Generalize (H1 x1 H2);Clear H1;Intro; 
+ Rewrite (Rmult_sym (Rminus (f x1) (f x0)) (Rinv (Rminus x1 x0))) in H1;
+ Rewrite (Rmult_sym (Rminus (g x1) (g x0)) (Rinv (Rminus x1 x0))) in H1;
+ Rewrite <-(Rmult_Rplus_distr (Rinv (Rminus x1 x0)) 
+                    (Rminus (f x1) (f x0)) 
+                    (Rminus (g x1) (g x0))) in H1;
+ Rewrite (Rmult_sym (Rinv (Rminus x1 x0))
+           (Rplus (Rminus (f x1) (f x0)) (Rminus (g x1) (g x0)))) in H1;
+ Cut (Rplus (Rminus (f x1) (f x0)) (Rminus (g x1) (g x0)))==
+      (Rminus (Rplus (f x1) (g x1)) (Rplus (f x0) (g x0))).
+Intro;Rewrite H3 in H1;Assumption.
+Ring.
+Save.
+
+(*********)
+Lemma Dmult:(D:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R)
+  (D_in f df D x0)->(D_in g dg D x0)->
+  (D_in [x:R](Rmult (f x) (g x))  
+             [x:R](Rplus (Rmult (df x) (g x)) (Rmult (f x) (dg x))) D x0).
+Intros;Unfold D_in;Generalize H H0;Intros;Unfold D_in in H H0;
+ Generalize (cont_deriv f df D x0 H1);Unfold continue_in;Intro;
+ Generalize (limit_mul 
+   [x:R](Rmult (Rminus (g x) (g x0)) (Rinv (Rminus x x0)))
+   [x:R](f x) (D_x D x0) (dg x0) (f x0) x0 H0 H3);Intro;
+ Cut (limit1_in [x:R](g x0) (D_x D x0) (g x0) x0).
+Intro;Generalize (limit_mul 
+  [x:R](Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0)))
+  [_:R](g x0) (D_x D x0) (df x0) (g x0) x0 H H5);Clear H H0 H1 H2 H3 H5;
+ Intro;Generalize (limit_plus 
+  [x:R](Rmult (Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0))) (g x0))
+  [x:R](Rmult (Rmult (Rminus (g x) (g x0)) (Rinv (Rminus x x0)))
+                (f x)) (D_x D x0) (Rmult (df x0) (g x0)) 
+                               (Rmult (dg x0) (f x0)) x0 H H4);
+ Clear H4 H;Intro;Unfold limit1_in in H;Unfold limit_in in H;
+ Simpl in H;Unfold limit1_in;Unfold limit_in;Simpl;Intros;
+ Elim (H eps H0);Clear H;Intros;Elim H;Clear H;Intros;
+ Split with x;Split;Auto;Intros;Generalize (H1 x1 H2);Clear H1;Intro;
+ Rewrite (Rmult_sym (Rminus (f x1) (f x0)) (Rinv (Rminus x1 x0))) in H1;
+ Rewrite (Rmult_sym (Rminus (g x1) (g x0)) (Rinv (Rminus x1 x0))) in H1;
+ Rewrite (Rmult_assoc (Rinv (Rminus x1 x0)) (Rminus (f x1) (f x0))
+       (g x0)) in H1;
+ Rewrite (Rmult_assoc (Rinv (Rminus x1 x0)) (Rminus (g x1) (g x0))
+       (f x1)) in H1;
+ Rewrite <-(Rmult_Rplus_distr (Rinv (Rminus x1 x0))
+                (Rmult (Rminus (f x1) (f x0)) (g x0))
+                (Rmult (Rminus (g x1) (g x0)) (f x1))) in H1;
+ Rewrite (Rmult_sym (Rinv (Rminus x1 x0))
+       (Rplus (Rmult (Rminus (f x1) (f x0)) (g x0))
+               (Rmult (Rminus (g x1) (g x0)) (f x1)))) in H1;
+ Rewrite (Rmult_sym (dg x0) (f x0)) in H1;
+ Cut (Rplus (Rmult (Rminus (f x1) (f x0)) (g x0))
+               (Rmult (Rminus (g x1) (g x0)) (f x1)))==
+      (Rminus (Rmult (f x1) (g x1)) (Rmult (f x0) (g x0))).
+Intro;Rewrite H3 in H1;Assumption.
+Ring.
+Unfold limit1_in;Unfold limit_in;Simpl;Intros;
+ Split with eps;Split;Auto;Intros;Elim (R_dist_refl (g x0) (g x0));
+ Intros a b;Rewrite (b (refl_eqT R (g x0)));Unfold Rgt in H;Assumption.
+Save.
+
+(*********)
+Lemma Dmult_const:(D:R->Prop)(f,df:R->R)(x0:R)(a:R)(D_in f df D x0)->
+  (D_in [x:R](Rmult a (f x)) ([x:R](Rmult a (df x))) D x0).
+Intros;Generalize (Dmult D [_:R]R0 df [_:R]a f x0 (Dconst D a x0) H);
+ Unfold D_in;Intros;
+ Rewrite (Rmult_Ol (f x0)) in H0;
+ Rewrite (let (H1,H2)=(Rplus_ne (Rmult a (df x0))) in H2) in H0;
+ Assumption.
+Save.
+
+(*********)
+Lemma Dopp:(D:R->Prop)(f,df:R->R)(x0:R)(D_in f df D x0)->
+  (D_in [x:R](Ropp (f x)) ([x:R](Ropp (df x))) D x0).
+Intros;Generalize (Dmult_const D f df x0 (Ropp R1) H); Unfold D_in;
+ Unfold limit1_in;Unfold limit_in;Intros;
+ Generalize (H0 eps H1);Clear H0;Intro;Elim H0;Clear H0;Intros; 
+ Elim H0;Clear H0;Simpl;Intros;Split with x;Split;Auto.
+Intros;Generalize (H2 x1 H3);Clear H2;Intro;Rewrite Ropp_mul1 in H2;
+ Rewrite Ropp_mul1 in H2;Rewrite Ropp_mul1 in H2;
+ Rewrite (let (H1,H2)=(Rmult_ne (f x1)) in H2) in H2; 
+ Rewrite (let (H1,H2)=(Rmult_ne (f x0)) in H2) in H2;
+ Rewrite (let (H1,H2)=(Rmult_ne (df x0)) in H2) in H2;Assumption.
+Save.
+
+(*********)
+Lemma Dx_pow_n:(n:nat)(D:R->Prop)(x0:R)
+  (D_in [x:R](pow x n)  
+        [x:R](Rmult (INR n) (pow x (minus n (1)))) D x0).
+Induction n;Intros.
+Simpl; Rewrite Rmult_Ol; Apply Dconst.
+Intros;Cut n0=(minus (S n0) (1));
+  [ Intro a; Rewrite <- a;Clear a | Simpl; Apply minus_n_O ].
+Generalize (Dmult D [_:R]R1 
+   [x:R](Rmult (INR n0) (pow x (minus n0 (1)))) [x:R]x [x:R](pow x n0) 
+   x0 (Dx D x0) (H D x0));Unfold D_in;Unfold limit1_in;Unfold limit_in;
+ Simpl;Intros;
+ Elim (H0 eps H1);Clear H0;Intros;Elim H0;Clear H0;Intros;
+ Split with x;Split;Auto.
+Intros;Generalize (H2 x1 H3);Clear H2 H3;Intro;
+ Rewrite (let (H1,H2)=(Rmult_ne (pow x0 n0)) in H2) in H2;
+ Rewrite (tech_pow_Rmult x1 n0) in H2;
+ Rewrite (tech_pow_Rmult x0 n0) in H2;
+ Rewrite (Rmult_sym (INR n0) (pow x0 (minus n0 (1)))) in H2;
+ Rewrite <-(Rmult_assoc x0 (pow x0 (minus n0 (1))) (INR n0)) in H2;
+ Rewrite (tech_pow_Rmult x0 (minus n0 (1))) in H2;
+ Elim (classic (n0=O));Intro cond.
+Rewrite cond in H2;Rewrite cond;Simpl in H2;Simpl;
+ Cut (Rplus R1 (Rmult (Rmult x0 R1) R0))==(Rmult R1 R1);
+ [Intro A; Rewrite A in H2; Assumption|Ring].
+Cut ~(n0=O)->(S (minus n0 (1)))=n0;[Intro|Omega];
+ Rewrite (H3 cond) in H2; Rewrite (Rmult_sym (pow x0 n0) (INR n0)) in H2;
+ Rewrite (tech_pow_Rplus x0 n0 n0) in H2; Assumption.
+Save.
+
+(*********)
+Lemma Dcomp:(Df,Dg:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R)
+  (D_in f df Df x0)->(D_in g dg Dg (f x0))->
+  (D_in [x:R](g (f x)) [x:R](Rmult (df x) (dg (f x))) 
+                       (Dgf Df Dg f) x0).
+Intros Df Dg df dg f g x0 H H0;Generalize H H0;Unfold D_in;Intros;
+Generalize (limit_comp f [x:R](Rmult (Rminus (g x) (g (f x0)))
+                               (Rinv (Rminus x (f x0)))) (D_x Df x0)
+              (D_x Dg (f x0)) 
+              (f x0) (dg (f x0)) x0);Intro;
+ Generalize (cont_deriv f df Df x0 H);Intro;Unfold continue_in in H4;
+ Generalize (H3 H4 H2);Clear H3;Intro;
+ Generalize (limit_mul [x:R](Rmult (Rminus (g (f x)) (g (f x0)))
+                                   (Rinv (Rminus (f x) (f x0))))
+                       [x:R](Rmult (Rminus (f x) (f x0))
+                                   (Rinv (Rminus x x0))) 
+                       (Dgf (D_x Df x0) (D_x Dg (f x0)) f) 
+                       (dg (f x0)) (df x0) x0 H3);Intro;
+ Cut (limit1_in
+         [x:R](Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0)))
+         (Dgf (D_x Df x0) (D_x Dg (f x0)) f) (df x0) x0).
+Intro;Generalize (H5 H6);Clear H5;Intro;
+ Generalize (limit_mul 
+        [x:R](Rmult (Rminus (f x) (f x0)) (Rinv (Rminus x x0))) 
+        [x:R](dg (f x0))
+       (D_x Df x0) (df x0) (dg (f x0)) x0 H1
+    (limit_free [x:R](dg (f x0)) (D_x Df x0) x0 x0));
+ Intro;
+ Unfold limit1_in;Unfold limit_in;Simpl;Unfold limit1_in in H5 H7;
+ Unfold limit_in in H5 H7;Simpl in H5 H7;Intros;Elim (H5 eps H8);
+ Elim (H7 eps H8);Clear H5 H7;Intros;Elim H5;Elim H7;Clear H5 H7;
+ Intros;Split with (Rmin x x1);Split.
+Elim (Rmin_Rgt x x1 R0);Intros a b;
+ Apply (b (conj (Rgt x R0) (Rgt x1 R0) H9 H5));Clear a b.
+Intros;Elim H11;Clear H11;Intros;Elim (Rmin_Rgt x x1 (R_dist x2 x0));
+ Intros a b;Clear b;Unfold Rgt in a;Elim (a H12);Clear H5 a;Intros;
+ Unfold D_x Dgf in H11 H7 H10;Clear H12;
+ Elim (classic (f x2)==(f x0));Intro.
+Elim H11;Clear H11;Intros;Elim H11;Clear H11;Intros;
+ Generalize (H10 x2 (conj (Df x2)/\~x0==x2 (Rlt (R_dist x2 x0) x)
+        (conj (Df x2) ~x0==x2 H11 H14) H5));Intro;
+ Rewrite (eq_Rminus (f x2) (f x0) H12) in H16;
+ Rewrite (Rmult_Ol (Rinv (Rminus x2 x0))) in H16;
+ Rewrite (Rmult_Ol (dg (f x0))) in H16;
+ Rewrite H12;
+ Rewrite (eq_Rminus (g (f x0)) (g (f x0)) (refl_eqT R (g (f x0))));
+ Rewrite (Rmult_Ol (Rinv (Rminus x2 x0)));Assumption.
+Clear H10 H5;Elim H11;Clear H11;Intros;Elim H5;Clear H5;Intros;
+Cut (((Df x2)/\~x0==x2)/\(Dg (f x2))/\~(f x0)==(f x2))
+        /\(Rlt (R_dist x2 x0) x1);Auto;Intro;
+ Generalize (H7 x2 H14);Intro;
+ Generalize (Rminus_eq_contra (f x2) (f x0) H12);Intro;
+ Rewrite (Rmult_assoc (Rminus (g (f x2)) (g (f x0))) 
+           (Rinv (Rminus (f x2) (f x0)))
+          (Rmult (Rminus (f x2) (f x0)) (Rinv (Rminus x2 x0)))) in H15;
+ Rewrite <-(Rmult_assoc (Rinv (Rminus (f x2) (f x0))) 
+             (Rminus (f x2) (f x0)) (Rinv (Rminus x2 x0))) in H15;
+ Rewrite (Rinv_l (Rminus (f x2) (f x0)) H16) in H15;
+ Rewrite (let (H1,H2)=(Rmult_ne (Rinv (Rminus x2 x0))) in H2) in H15;
+ Rewrite (Rmult_sym (df x0) (dg (f x0)));Assumption.
+Clear H5 H3 H4 H2;Unfold limit1_in;Unfold limit_in;Simpl;
+ Unfold limit1_in in H1;Unfold limit_in in H1;Simpl in H1;Intros;
+ Elim (H1 eps H2);Clear H1;Intros;Elim H1;Clear H1;Intros;
+ Split with x;Split;Auto;Intros;Unfold D_x Dgf in H4 H3;
+ Elim H4;Clear H4;Intros;Elim H4;Clear H4;Intros;
+ Exact (H3 x1 (conj (Df x1)/\~x0==x1 (Rlt (R_dist x1 x0) x) H4 H5)).
+Save.   
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
new file mode 100644
index 000000000..c9ee14137
--- /dev/null
+++ b/theories/Reals/Reals.v
@@ -0,0 +1,11 @@
+
+(* $Id$ *)
+
+Require Export TypeSyntax.
+Require Export Raxioms.
+Require Export Rbase.
+Require Export R_Ifp.
+Require Export Rbasic_fun.
+Require Export Rlimit.
+Require Export Rfunctions.
+Require Export Rderiv.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
new file mode 100644
index 000000000..987a6ea63
--- /dev/null
+++ b/theories/Reals/Rfunctions.v
@@ -0,0 +1,79 @@
+
+(* $Id$ *)
+
+(*********************************************************)
+(*           Definition of the some functions            *)
+(*                                                       *)
+(*********************************************************)
+
+Require Export Rlimit.
+
+(*******************************)
+(*      Factorial              *)
+(*******************************)
+(*********)
+Fixpoint fact [n:nat]:nat:=
+  Cases n of
+     O     => (S O)
+    |(S n) => (mult (S n) (fact n))
+  end.
+ 
+(*******************************)
+(*          Power              *)
+(*******************************)
+(*********)
+Fixpoint pow [r:R;n:nat]:R:=
+  Cases n of
+     O     => R1
+    |(S n) => (Rmult r (pow r n))
+  end.
+
+(*********)
+Lemma tech_pow_Rmult:(x:R)(n:nat)(Rmult x (pow x n))==(pow x (S n)).
+Induction n; Simpl; Trivial.
+Save.
+
+(*********)
+Lemma tech_pow_Rplus:(x:R)(a,n:nat)
+  (Rplus (pow x a) (Rmult (INR n) (pow x a)))==
+           (Rmult (INR (S n)) (pow x a)).
+Intros; Pattern 1 (pow x a);  
+ Rewrite <-(let (H1,H2)=(Rmult_ne (pow x a)) in H1); 
+ Rewrite (Rmult_sym (INR n) (pow x a));
+ Rewrite <- (Rmult_Rplus_distr (pow x a) R1 (INR n));
+ Rewrite (Rplus_sym R1 (INR n)); Rewrite <-(S_INR n);
+ Apply Rmult_sym.
+Save.
+
+(*******************************)
+(*  Sum of n first naturals    *)
+(*******************************)
+(*********)
+Fixpoint sum_nat_aux [s,n:nat]:nat:=       
+  Cases n of                            
+    O => s                                
+   |(S n') => (sum_nat_aux (plus s n) n') 
+  end.
+
+(*********)
+Definition sum_nat:=(sum_nat_aux O).  
+
+(*******************************)
+(*             Sum             *)
+(*******************************)
+(*********)
+Fixpoint sum_aux [s:R;f:nat->R;N:nat]:R:=
+  Cases N of
+     O     => (Rplus s (f O))
+    |(S i) => (sum_aux (Rplus s (f N)) f i)
+  end.
+ 
+(*********)
+Definition sum_f:=(sum_aux R0).  
+
+(*******************************)
+(*        Infinit Sum          *)
+(*******************************)
+(*********)
+Definition infinit_sum:(nat->R)->R->Prop:=[s:nat->R;l:R]
+  (eps:R)(Ex[N:nat](n:nat)(ge n N)/\(Rlt (R_dist (sum_f s n) l) eps)).
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
new file mode 100644
index 000000000..56a7c709d
--- /dev/null
+++ b/theories/Reals/Rlimit.v
@@ -0,0 +1,1029 @@
+
+(* $Id$ *)
+
+(*********************************************************)
+(*           Definition of the limit                     *)
+(*                                                       *)
+(*********************************************************)
+
+Require Export Rbasic_fun.
+Require Export Classical_Prop.
+
+(*******************************)
+(*      Calculus               *)
+(*******************************)
+(*********)
+Lemma eps2_Rgt_R0:(eps:R)(Rgt eps R0)->
+      (Rgt (Rmult eps (Rinv (Rplus R1 R1))) R0).
+Intros;Generalize (Rlt_compatibility R1 R0 R1 Rlt_R0_R1);Intro;
+ Elim (Rplus_ne R1);Intros a b;Rewrite a in H0;Clear a b;
+ Generalize (Rlt_Rinv (Rplus R1 R1) 
+                       (Rlt_trans R0 R1 (Rplus R1 R1) Rlt_R0_R1 H0));Intro;
+ Unfold Rgt in H;
+ Generalize (Rlt_monotony (Rinv (Rplus R1 R1)) R0 eps H1 H);Intro;
+ Rewrite (Rmult_Or (Rinv (Rplus R1 R1))) in H2;
+ Rewrite (Rmult_sym (Rinv (Rplus R1 R1)) eps) in H2;
+ Unfold Rgt;Assumption.
+Save.
+
+(*********)
+Lemma eps2:(eps:R)(Rplus (Rmult eps (Rinv (Rplus R1 R1)))
+                        (Rmult eps (Rinv (Rplus R1 R1))))==eps.
+Intro;Rewrite<-(Rmult_Rplus_distr eps (Rinv (Rplus R1 R1)) (Rinv (Rplus R1 R1)));
+ Elim (Rmult_ne eps);Intros a b;Pattern 2 eps;Rewrite <- a;Clear a b;
+ Apply Rmult_mult_r;Clear eps;Cut ~(Rplus R1 R1)==R0.
+Intro;Apply (r_Rmult_mult (Rplus R1 R1) 
+         (Rplus (Rinv (Rplus R1 R1)) (Rinv (Rplus R1 R1))) R1);Auto;
+Rewrite (Rmult_Rplus_distr (Rplus R1 R1) (Rinv (Rplus R1 R1)) 
+                              (Rinv (Rplus R1 R1)));
+ Rewrite (Rinv_r (Rplus R1 R1) H);Elim (Rmult_ne (Rplus R1 R1));Intros a b;
+ Rewrite a;Clear a b;Reflexivity.
+Red;Intro;Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H0);Intro;Elim (Rplus_ne R1);
+ Intros a b;Rewrite a in H1;Clear a b;
+ Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H0 H1);Intro;
+ Elim (imp_not_Req R0 (Rplus R1 R1));Auto;Left;Assumption.
+Save.
+
+(*********)
+Lemma eps4:(eps:R)
+  (Rplus (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1) )))
+        (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1) ))))==
+                  (Rmult eps (Rinv (Rplus R1 R1))).
+Intro;Rewrite<-(Rmult_Rplus_distr eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) 
+                            (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))));
+ Apply Rmult_mult_r;Clear eps;
+ Rewrite <-(let (H1,H2)=
+     (Rmult_ne (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))) in H1);
+ Rewrite <-(Rmult_Rplus_distr (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) R1 R1);
+ Cut ~(Rplus R1 R1)==R0. 
+Intro;Apply (r_Rmult_mult (Rplus R1 R1) 
+           (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) (Rplus R1 R1)) 
+           (Rinv (Rplus R1 R1)));Auto.
+Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
+                      (Rplus R1 R1));
+ Rewrite <-(Rmult_assoc (Rplus R1 R1) (Rplus R1 R1) 
+             (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))));
+ Rewrite (Rinv_r (Rplus R1 R1) H);Rewrite (Rmult_Rplus_distr (Rplus R1 R1) R1 R1);
+ Rewrite (let (H1,H2)=(Rmult_ne (Rplus R1 R1)) in H1);
+ Apply (Rinv_r (Rplus (Rplus R1 R1) (Rplus R1 R1))).
+Apply (imp_not_Req (Rplus (Rplus R1 R1) (Rplus R1 R1)) R0);Right;Unfold Rgt;
+ Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H0);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H1;
+ Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H0 H1);Intro;
+ Clear H0 H1;
+ Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H2);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H0;
+ Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
+    H2 H0).
+Apply (imp_not_Req (Rplus R1 R1) R0);Right;Unfold Rgt;Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H0;
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H H0).
+Save.
+
+(*********)
+Lemma Rlt_eps2_eps:(eps:R)(Rgt eps R0)->
+        (Rlt (Rmult eps (Rinv (Rplus R1 R1))) eps).
+Intros;Unfold Rgt in H;Elim (Rmult_ne eps);Intros a b;Pattern 2 eps;
+ Rewrite <- a;Clear a b;
+ Apply (Rlt_monotony eps (Rinv (Rplus R1 R1)) R1 H);
+ Apply (Rlt_anti_compatibility (Rinv (Rplus R1 R1)) (Rinv (Rplus R1 R1))
+      R1);Elim (Rmult_ne (Rinv (Rplus R1 R1)));Intros a b;
+ Pattern 1 2 (Rinv (Rplus R1 R1));Rewrite <-b;Clear a b;
+ Rewrite (eps2 R1);Elim (Rplus_ne R1);Intros a b;Pattern 1 R1;
+ Rewrite <-a;Clear a b;Rewrite (Rplus_sym (Rinv (Rplus R1 R1)) R1);
+ Apply (Rlt_compatibility R1 R0 (Rinv (Rplus R1 R1)) 
+   (Rlt_Rinv (Rplus R1 R1) (Rlt_r_plus_R1 R1 (Rlt_le R0 R1 Rlt_R0_R1)))). 
+Save.
+
+(*********)
+Lemma Rlt_eps4_eps:(eps:R)(Rgt eps R0)->
+        (Rlt (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))) eps).
+Intros;Pattern 2 eps;Rewrite <-(let (H1,H2)=(Rmult_ne eps) in H1);
+ Unfold Rgt in H;Apply Rlt_monotony;Auto.
+ Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H0);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H1;
+ Generalize (Rlt_compatibility R1 R1 (Rplus R1 R1) H1);Intro;
+ Generalize (Rlt_compatibility (Rplus R1 R1) R1 (Rplus R1 R1) H1);Intro;
+ Generalize (Rlt_trans R1 (Rplus R1 R1) (Rplus R1 (Rplus R1 R1))
+    H1 H2);Intro;
+ Rewrite (Rplus_sym (Rplus R1 R1) R1) in H3;
+ Generalize (Rlt_trans R1 (Rplus R1 (Rplus R1 R1)) 
+       (Rplus (Rplus R1 R1) (Rplus R1 R1)) H4 H3);Clear H H0 H1 H2 H3 H4;
+ Intro;Rewrite <-(let (H1,H2)=(Rmult_ne 
+   (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))) in H1);Pattern 6 R1;
+ Rewrite <-(Rinv_l (Rplus (Rplus R1 R1) (Rplus R1 R1))).
+ Apply (Rlt_monotony (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
+       R1 (Rplus (Rplus R1 R1) (Rplus R1 R1)));Auto.
+Apply (Rlt_Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)));
+ Apply (Rlt_trans R0 R1 (Rplus (Rplus R1 R1) (Rplus R1 R1)) Rlt_R0_R1 H).
+Apply (imp_not_Req (Rplus (Rplus R1 R1) (Rplus R1 R1)) R0);Right;Unfold Rgt;
+ Apply (Rlt_trans R0 R1 (Rplus (Rplus R1 R1) (Rplus R1 R1)) Rlt_R0_R1 H).
+Save. 
+
+(*********)
+Lemma prop_eps:(r:R)((eps:R)(Rgt eps R0)->(Rlt r eps))->(Rle r R0).
+Intros;Elim (total_order r R0); Intro.
+Apply Rlt_le; Assumption.
+Elim H0; Intro.
+Apply eq_Rle; Assumption.
+Clear H0;Generalize (H r H1); Intro;Generalize (Rlt_antirefl r);
+ Intro;ElimType False; Auto.
+Save.
+
+(*******************************)
+(*      Metric space           *)
+(*******************************)
+
+(*********)
+Record Metric_Space:Type:= {
+   Base:Type;
+   dist:Base->Base->R;
+   dist_pos:(x,y:Base)(Rge (dist x y) R0);
+   dist_sym:(x,y:Base)(dist x y)==(dist y x);
+   dist_refl:(x,y:Base)((dist x y)==R0<->x==y);
+   dist_tri:(x,y,z:Base)(Rle (dist x y) 
+              (Rplus (dist x z) (dist z y))) }.
+
+(*******************************)
+(*     Limit in Metric space   *)
+(*******************************)
+
+(*********)
+Definition limit_in:=
+   [X:Metric_Space; X':Metric_Space; f:(Base X)->(Base X'); 
+    D:(Base X)->Prop; x0:(Base X); l:(Base X')]
+   (eps:R)(Rgt eps R0)->
+   (EXT alp:R | (Rgt alp R0)/\(x:(Base X))(D x)/\
+                (Rlt (dist X x x0) alp)->
+                (Rlt (dist X' (f x) l) eps)). 
+
+(*******************************)
+(*        Distance  in R       *)
+(*******************************)
+
+(*********)
+Definition R_dist:R->R->R:=[x,y:R](Rabsolu (Rminus x y)).
+
+(*********)
+Lemma R_dist_pos:(x,y:R)(Rge (R_dist x y) R0).
+Intros;Unfold R_dist;Unfold Rabsolu;Case (case_Rabsolu (Rminus x y));Intro l.
+Unfold Rge;Left;Apply (Rlt_RoppO (Rminus x y) l).
+Trivial.
+Save.
+
+(*********)
+Lemma R_dist_sym:(x,y:R)(R_dist x y)==(R_dist y x).
+Intros; Unfold R_dist; Unfold Rabsolu;
+ Case (case_Rabsolu (Rminus x y)); Case (case_Rabsolu (Rminus y x));
+ Intros l l0.
+Generalize (Rlt_RoppO (Rminus y x) l); Intro;
+ Rewrite (Ropp_distr2 y x) in H;
+ Generalize (Rlt_antisym (Rminus x y) R0 l0); Intro;Unfold Rgt in H;
+ ElimType False; Auto.
+Apply (Ropp_distr2 x y).
+Apply sym_eqT;Apply (Ropp_distr2 y x). 
+Generalize (minus_Rge y x l); Intro;
+ Generalize (minus_Rge x y l0); Intro;
+ Generalize (Rge_ge_eq x y H0 H); Intro;Rewrite H1;Trivial.
+Save.
+
+(*********)
+Lemma R_dist_refl:(x,y:R)((R_dist x y)==R0<->x==y).
+Intros;Unfold R_dist; Unfold Rabsolu;
+ Case (case_Rabsolu (Rminus x y));Intro;Split;Intro.
+Rewrite (Ropp_distr2 x y) in H;Apply sym_eqT;
+ Apply (Rminus_eq y x H).
+Rewrite (Ropp_distr2 x y);Generalize (sym_eqT R x y H);Intro;
+ Apply (eq_Rminus y x H0).
+Apply (Rminus_eq x y H).
+Apply (eq_Rminus x y H). 
+Save.
+
+(***********)
+Lemma R_dist_tri:(x,y,z:R)(Rle (R_dist x y) 
+                   (Rplus (R_dist x z) (R_dist z y))).
+Intros;Unfold R_dist; Unfold Rabsolu;
+ Case (case_Rabsolu (Rminus x y)); Case (case_Rabsolu (Rminus x z));
+ Case (case_Rabsolu (Rminus z y));Intros.
+Rewrite (Ropp_distr2 x y); Rewrite (Ropp_distr2 x z);
+ Rewrite (Ropp_distr2 z y);Unfold Rminus;
+ Rewrite (Rplus_sym y (Ropp z));
+ Rewrite (Rplus_sym z (Ropp x));
+ Rewrite (Rplus_assoc (Ropp x) z (Rplus (Ropp z) y));
+ Rewrite <-(Rplus_assoc z (Ropp z) y);Rewrite (Rplus_Ropp_r z);
+ Elim (Rplus_ne y);Intros a b;Rewrite b;Clear a b;
+ Rewrite (Rplus_sym y (Ropp x));
+ Apply (eq_Rle (Rplus (Ropp x) y) (Rplus (Ropp x) y) 
+        (refl_eqT R (Rplus (Ropp x) y))).
+Rewrite (Ropp_distr2 x y);Rewrite (Ropp_distr2 x z);Unfold Rminus;
+ Rewrite (Rplus_sym y (Ropp x));
+ Rewrite (Rplus_sym z (Ropp x));
+ Rewrite (Rplus_assoc (Ropp x) z (Rplus z (Ropp y)));
+ Apply (Rle_compatibility (Ropp x) y 
+        (Rplus z (Rplus z (Ropp y))));
+ Rewrite (Rplus_sym z (Rplus z (Ropp y)));
+ Apply (Rle_anti_compatibility (Ropp y) y
+        (Rplus (Rplus z (Ropp y)) z));Rewrite (Rplus_Ropp_l y);
+ Rewrite (Rplus_sym (Ropp y) (Rplus (Rplus z (Ropp y)) z));
+ Rewrite (Rplus_assoc (Rplus z (Ropp y)) z (Ropp y));
+ Fold (Rminus z y);Generalize (Rle_sym2 R0 (Rminus z y) r);Intro;
+ Generalize (Rle_compatibility (Rminus z y) R0 (Rminus z y) H);Intro;
+ Elim (Rplus_ne (Rminus z y)); Intros a b; Rewrite a in H0; Clear a b;
+ Apply (Rle_trans R0 (Rminus z y) (Rplus (Rminus z y) (Rminus z y)) 
+        H H0).
+Rewrite (Ropp_distr2 x y);Rewrite (Ropp_distr2 z y);Unfold Rminus;
+ Rewrite (Rplus_sym y (Ropp z));
+ Rewrite <- (Rplus_assoc (Rplus x (Ropp z)) (Ropp z) y);
+ Rewrite (Rplus_sym (Rplus (Rplus x (Ropp z)) (Ropp z)) y);
+ Apply (Rle_compatibility y (Ropp x)
+        (Rplus (Rplus x (Ropp z)) (Ropp z)));
+ Apply (Rle_anti_compatibility x (Ropp x)
+        (Rplus (Rplus x (Ropp z)) (Ropp z)));Rewrite (Rplus_Ropp_r x);
+ Rewrite (Rplus_sym x (Rplus (Rplus x (Ropp z)) (Ropp z)));
+ Rewrite (Rplus_assoc (Rplus x (Ropp z)) (Ropp z) x);
+ Rewrite (Rplus_sym (Ropp z) x);Fold (Rminus x z);
+ Generalize (Rle_sym2 R0 (Rminus x z) r0);Intro;
+ Generalize (Rle_compatibility (Rminus x z) R0 (Rminus x z) H);Intro;
+ Elim (Rplus_ne (Rminus x z));Intros a b;Rewrite a in H0;Clear a b;
+ Apply (Rle_trans R0 (Rminus x z) (Rplus (Rminus x z) (Rminus x z)) 
+         H H0).
+Unfold 2 3 Rminus;
+ Rewrite <-(Rplus_assoc (Rplus x (Ropp z)) z (Ropp y));
+ Rewrite (Rplus_assoc x (Ropp z) z);Rewrite (Rplus_Ropp_l z);
+ Elim (Rplus_ne x);Intros a b;Rewrite a;Clear a b; Fold (Rminus x y);
+ Apply (Rle_anti_compatibility (Rminus x y) (Ropp (Rminus x y))
+        (Rminus x y));Rewrite (Rplus_Ropp_r (Rminus x y));
+ Generalize (Rle_sym2 R0 (Rminus x z) r0);Intro;
+ Generalize (Rle_sym2 R0 (Rminus z y) r);Intro;
+ Generalize (Rle_compatibility (Rminus z y) R0 (Rminus x z) H);Intro;
+ Elim (Rplus_ne (Rminus z y));Intros a b;Rewrite a in H1;Clear a b;
+ Unfold 2 3 Rminus in H1;
+ Rewrite (Rplus_assoc z (Ropp y) (Rplus x (Ropp z))) in H1;
+ Rewrite (Rplus_sym z (Rplus (Ropp y) (Rplus x (Ropp z)))) 
+          in H1;
+ Rewrite <-(Rplus_assoc (Ropp y) x (Ropp z)) in H1;
+ Rewrite (Rplus_assoc (Rplus (Ropp y) x) (Ropp z) z) in H1;
+ Rewrite (Rplus_Ropp_l z) in H1;
+ Elim (Rplus_ne (Rplus (Ropp y) x));Intros a b;Rewrite a in H1;
+ Clear a b;Rewrite (Rplus_sym (Ropp y) x) in H1;
+ Fold (Rminus x y) in H1;
+ Generalize (Rle_trans R0 (Rminus z y) (Rminus x y) H0 H1);Intro;
+ Generalize (Rle_compatibility (Rminus x y) R0 (Rminus x y) H2);
+ Intro;Elim (Rplus_ne (Rminus x y));Intros a b;Rewrite a in H3;
+ Clear a b;
+ Apply (Rle_trans R0 (Rminus x y) (Rplus (Rminus x y) (Rminus x y)) 
+         H2 H3). 
+Generalize (Rminus_lt z y r);Intro;Generalize (Rminus_lt x z r0);
+ Intro;Generalize (Rlt_trans x z y H0 H);Intro;
+ Generalize (Rlt_minus x y H1);Intro;
+ Generalize (Rle_not R0 (Rminus x y) H2);Intro;
+ Generalize (Rle_sym2 R0 (Rminus x y) r1);Intro;
+ ElimType False;Auto.
+Rewrite (Ropp_distr2 x z);Unfold Rminus;
+ Rewrite (Rplus_sym x (Ropp y));
+ Rewrite <-(Rplus_assoc (Rplus z (Ropp x)) z (Ropp y));
+ Rewrite (Rplus_sym (Rplus (Rplus z (Ropp x)) z) (Ropp y));
+ Apply (Rle_compatibility (Ropp y) x 
+        (Rplus (Rplus z (Ropp x)) z));
+ Apply (Rle_anti_compatibility (Ropp x) x 
+        (Rplus (Rplus z (Ropp x)) z));
+ Rewrite (Rplus_Ropp_l x);
+ Rewrite (Rplus_sym (Ropp x) (Rplus (Rplus z (Ropp x)) z));
+ Rewrite (Rplus_assoc (Rplus z (Ropp x)) z (Ropp x));
+ Fold (Rminus z x);Generalize (Rminus_lt x z r0);Intro;
+ Generalize (Rlt_RoppO (Rminus x z) r0);Intro;
+ Rewrite (Ropp_distr2 x z) in H0;
+ Generalize (Rgt_ge (Rminus z x) R0 H0);Intro;
+ Generalize (Rle_sym2 R0 (Rminus z x) H1);Intro;
+ Generalize (Rle_compatibility (Rminus z x) R0 (Rminus z x) H2); 
+ Intro;Elim (Rplus_ne (Rminus z x)); Intros a b; Rewrite a in H3; 
+ Clear a b;
+ Apply (Rle_trans R0 (Rminus z x) (Rplus (Rminus z x) (Rminus z x)) 
+        H2 H3).
+Rewrite (Ropp_distr2 z y);Unfold Rminus;
+ Rewrite (Rplus_assoc x (Ropp z) (Rplus y (Ropp z)));
+ Apply (Rle_compatibility x (Ropp y) 
+        (Rplus (Ropp z) (Rplus y (Ropp z))));
+ Apply (Rle_anti_compatibility y (Ropp y) 
+        (Rplus (Ropp z) (Rplus y (Ropp z))));
+ Rewrite (Rplus_Ropp_r y);
+ Rewrite <-(Rplus_assoc y  (Ropp z) (Rplus y (Ropp z)));
+ Fold (Rminus y z);Generalize (Rlt_Ropp (Rminus z y) R0 r);Intro;
+ Rewrite Ropp_O in H;Rewrite (Ropp_distr2 z y) in H;
+ Generalize (Rgt_ge (Rminus y z) R0 H);Intro;
+ Generalize (Rle_sym2 R0 (Rminus y z) H0);Intro;
+ Generalize (Rle_compatibility (Rminus y z) R0 (Rminus y z) H1);
+ Intro;Elim (Rplus_ne (Rminus y z)); Intros a b; Rewrite a in H2;
+ Clear a b;
+ Apply (Rle_trans R0 (Rminus y z) (Rplus (Rminus y z) (Rminus y z)) 
+        H1 H2).
+Unfold 2 3 Rminus;
+ Rewrite (Rplus_assoc  x (Ropp z) (Rplus z (Ropp y)));
+ Rewrite <-(Rplus_assoc (Ropp z) z (Ropp y));
+ Rewrite (Rplus_Ropp_l z);Elim (Rplus_ne (Ropp y));Intros a b;Rewrite b;
+ Clear a b;Fold (Rminus x y);
+ Apply (eq_Rle (Rminus x y) (Rminus x y) (refl_eqT R (Rminus x y))).
+Save.
+
+(*******************************)
+(*    R is a metric space      *)
+(*******************************)
+
+(*********)
+Definition R_met:Metric_Space:=(Build_Metric_Space R R_dist 
+  R_dist_pos R_dist_sym R_dist_refl R_dist_tri).
+
+(*******************************)
+(*         Limit 1 arg         *)
+(*******************************)
+(*********)
+Definition Dgf:=[Df,Dg:R->Prop][f:R->R][x:R](Df x)/\(Dg (f x)).
+
+(*********)
+Definition limit1_in:(R->R)->(R->Prop)->R->R->Prop:=
+  [f:R->R; D:R->Prop; l:R; x0:R](limit_in R_met R_met f D x0 l).
+
+(*********)
+Lemma tech_limit:(f:R->R)(D:R->Prop)(l:R)(x0:R)(D x0)->
+   (limit1_in f D l x0)->l==(f x0).
+Unfold limit1_in;Unfold limit_in;Simpl;Intros;Apply NNPP;Red;Intro;
+ Generalize (R_dist_pos (f x0) l);Intro;Unfold Rge in H2;Elim H2;Intro;
+ Clear H2.
+Elim (H0 (R_dist (f x0) l) H3);Intros;Elim H2;Clear H2 H0;
+ Intros;Generalize (H2 x0);Clear H2;Intro;Elim (R_dist_refl x0 x0);
+ Intros a b;Clear a;Rewrite (b (refl_eqT R x0)) in H2;Clear b;
+ Unfold Rgt in H0;Generalize (H2 (conj (D x0) (Rlt R0 x) H H0));Intro;
+ Clear H2;Generalize (Rlt_antirefl (R_dist (f x0) l));Intro;Auto.
+Elim (R_dist_refl (f x0) l);Intros a b;Clear b;Generalize (a H3);Intro;
+Generalize (sym_eqT R (f x0) l H2);Intro;Auto.
+Save. 
+
+(*********)
+Lemma tech_limit_contr:(f:R->R)(D:R->Prop)(l:R)(x0:R)(D x0)->~l==(f x0)
+   ->~(limit1_in f D l x0).
+Intros;Generalize (tech_limit f D l x0);Tauto.
+Save.
+
+(*********)
+Lemma lim_x:(D:R->Prop)(x0:R)(limit1_in [x:R]x D x0 x0).
+Unfold limit1_in; Unfold limit_in; Simpl; Intros;Split with eps;
+ Split; Auto;Intros;Elim H0; Intros; Auto.
+Save.
+
+(*********)
+Lemma limit_plus:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R)
+   (limit1_in f D l x0)->(limit1_in g D l' x0)->
+   (limit1_in [x:R](Rplus (f x) (g x)) D (Rplus l l') x0).
+Unfold limit1_in;Unfold limit_in;Simpl;Intros;
+ Elim (H (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
+ Elim (H0 (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
+ Clear H H0;Intros;Elim H;Elim H0;Clear H H0;Intros;
+ Split with (Rmin x1 x);Split.
+Elim (Rmin_Rgt x1 x R0);Intros a b;
+ Apply (b (conj (Rgt x1 R0) (Rgt x R0) H H2));Clear a b.
+Intros;Elim H4;Clear H4;Intros;Elim (Rmin_Rgt x1 x (R_dist x2 x0));
+ Intros a b;Clear b;Unfold Rgt in a;Elim (a H5);Clear H5 a;Intros;
+ Generalize (H0 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H4 H5)); 
+ Generalize (H3 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H4 H6));
+ Clear H0 H3 H5 H6;Intros;
+ Generalize (Rplus_lt (R_dist (f x2) l) 
+                     (Rmult eps (Rinv (Rplus R1 R1))) 
+                     (R_dist (g x2) l')
+                     (Rmult eps (Rinv (Rplus R1 R1))) H3 H0);
+ Clear H0 H3 H4;Intro;Rewrite (eps2 eps) in H0;Unfold R_dist;
+ Unfold Rminus;Rewrite (Rplus_sym l l');Rewrite (Ropp_distr1 l' l);
+ Rewrite <-(Rplus_assoc (Rplus (f x2) (g x2)) (Ropp l') (Ropp l));
+ Rewrite (Rplus_assoc (f x2) (g x2) (Ropp l'));
+ Rewrite (Rplus_sym (Rplus (f x2) (Rplus (g x2) (Ropp l'))) 
+   (Ropp l));
+ Rewrite <-(Rplus_assoc (Ropp l) (f x2) (Rplus (g x2) (Ropp l')));
+ Rewrite (Rplus_sym (Ropp l) (f x2));
+ Fold (Rminus (f x2) l);Fold (Rminus (g x2) l');Unfold R_dist in H0;
+ Apply (Rle_lt_trans 
+  (Rabsolu (Rplus (Rminus (f x2) l) (Rminus (g x2) l')))
+  (Rplus (Rabsolu (Rminus (f x2) l)) (Rabsolu (Rminus (g x2) l')))
+  eps 
+  (Rabsolu_triang (Rminus (f x2) l) (Rminus (g x2) l')) H0).
+Save.
+
+(*********)
+Lemma limit_Ropp:(f:R->R)(D:R->Prop)(l:R)(x0:R)
+   (limit1_in f D l x0)->(limit1_in [x:R](Ropp (f x)) D (Ropp l) x0).
+Unfold limit1_in;Unfold limit_in;Simpl;Intros;Elim (H eps H0);Clear H;
+ Intros;Elim H;Clear H;Intros;Split with x;Split;Auto;Intros;
+ Generalize (H1 x1 H2);Clear H1;Intro;Unfold R_dist;Unfold Rminus;
+ Rewrite (Ropp_Ropp l);Rewrite (Rplus_sym (Ropp (f x1)) l);
+ Fold (Rminus l (f x1));Fold (R_dist l (f x1));Rewrite R_dist_sym;
+ Assumption.
+Save.
+
+(*********)
+Lemma limit_minus:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R)
+   (limit1_in f D l x0)->(limit1_in g D l' x0)->
+   (limit1_in [x:R](Rminus (f x) (g x)) D (Rminus l l') x0).
+Intros;Unfold Rminus;Generalize (limit_Ropp g D l' x0 H0);Intro;
+ Exact (limit_plus f [x:R](Ropp (g x)) D l (Ropp l') x0 H H1).
+Save.
+
+(*********)
+Lemma limit_free:(f:R->R)(D:R->Prop)(x:R)(x0:R)
+   (limit1_in [h:R](f x) D (f x) x0).
+Unfold limit1_in;Unfold limit_in;Simpl;Intros;Split with eps;Split;
+ Auto;Intros;Elim (R_dist_refl (f x) (f x));Intros a b;
+ Rewrite (b (refl_eqT R (f x)));Unfold Rgt in H;Assumption.
+Save.
+
+(*********)
+Lemma limit_mul:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R)
+   (limit1_in f D l x0)->(limit1_in g D l' x0)->
+   (limit1_in [x:R](Rmult (f x) (g x)) D (Rmult l l') x0).
+Unfold limit1_in;Unfold limit_in;Simpl;Intros;
+ Elim (Req_EM l R0);Elim (Req_EM l' R0);Intros.
+(**)
+Rewrite H2;Rewrite H3;Rewrite H2 in H0;Rewrite H3 in H;
+ Rewrite (Rmult_Or R0);Unfold R_dist;Unfold R_dist in H H0;
+ Elim (H eps H1);Clear H;Unfold 1 Rgt in H0;Elim (H0 R1 Rlt_R0_R1);
+ Clear H0;Intros;Elim H;Elim H0;Clear H H0;Intros;
+ Split with (Rmin x1 x);Split.
+Elim (Rmin_Rgt x1 x R0);Intros a b;
+ Apply (b (conj (Rgt x1 R0) (Rgt x R0) H H4));Clear a b.
+Intros;Elim H6;Clear H6;Intros;Elim (Rmin_Rgt x1 x (R_dist x2 x0));
+ Intros a b;Clear b;Unfold Rgt in a;Elim (a H7);Clear H7 a;Intros;
+ Unfold R_dist in H7 H8;
+ Generalize (H0 x2 (conj (D x2) 
+          (Rlt (Rabsolu (Rminus x2 x0)) x1) H6 H7));
+ Generalize (H5 x2 (conj (D x2) 
+          (Rlt (Rabsolu (Rminus x2 x0)) x) H6 H8));Intros;
+ Clear H0 H5 H7 H8;Rewrite (minus_R0 (g x2)) in H9;
+ Rewrite (minus_R0 (f x2)) in H10;
+ Rewrite (minus_R0 (Rmult (f x2) (g x2)));
+ Generalize Rlt_R0_R1;Intro;Fold (Rgt R1 R0) in H0;
+ Rewrite (Rabsolu_mult (f x2) (g x2));
+ Rewrite <-(let (H1,H2)=(Rmult_ne eps) in H1);
+ Generalize (Rabsolu_pos (g x2));Unfold Rle;Intro;Elim H5;Clear H5;
+ Intro.
+Apply (Rmult_lt (Rabsolu (f x2)) eps (Rabsolu (g x2)) R1 H5 H1 H10 H9).
+Rewrite <-H5;Rewrite (Rmult_Or (Rabsolu (f x2))); 
+ Rewrite (let (H1,H2)=(Rmult_ne eps) in H1);Unfold Rgt in H1;Assumption.
+(**)
+Rewrite H3;Rewrite H3 in H;Rewrite (Rmult_Ol l');
+ Elim (H0 (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));Intros;
+ Elim H4;Clear H4;Intros;
+ Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;Elim (H R1 H6);Intros;
+ Elim H7;Clear H7;Intros;
+ Cut (Rgt (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l')))) R0).
+Intro;Elim (H (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l')))) H9);
+ Intros;Elim H10;Clear H10;Intros;Split with (Rmin (Rmin x x1) x2);
+ Split.
+Elim (Rmin_Rgt (Rmin x x1) x2 R0);Intros;Elim (Rmin_Rgt x x1 R0);Intros;
+ Generalize (H15 (conj (Rgt x R0) (Rgt x1 R0) H4 H7));Clear H14 H15;
+ Intro;Clear H12;
+ Apply (H13 (conj (Rgt (Rmin x x1) R0) (Rgt x2 R0) H14 H10)).
+Intros;Elim H12;Clear H12;Intros;
+ Elim (Rmin_Rgt (Rmin x x1) x2 (R_dist x3 x0));Intros;Clear H15;
+ Unfold 1 Rgt in H14;Elim (H14 H13);Clear H14;Intros;Unfold Rgt in H15;
+ Clear H13;Elim (Rmin_Rgt x x1 (R_dist x3 x0));Intros;
+ Elim (H13 H14);Clear H14 H13 H16;Intros;Unfold Rgt in H13 H14;
+ Generalize (H5 x3 (conj (D x3) (Rlt (R_dist x3 x0) x) H12 H13));
+ Generalize (H8 x3 (conj (D x3) (Rlt (R_dist x3 x0) x1) H12 H14));
+ Generalize (H11 x3 (conj (D x3) (Rlt (R_dist x3 x0) x2) H12 H15));
+ Clear H5 H8 H11 H15 H13 H14 H12;Intros;Unfold R_dist in H5 H8 H11;
+ Unfold R_dist;Rewrite (minus_R0 (Rmult (f x3) (g x3)));
+ Rewrite (minus_R0 (f x3)) in H5;Rewrite (minus_R0 (f x3)) in H8;
+ Rewrite <-(let (H1,H2)=(Rplus_ne (Rmult (f x3) (g x3))) in H1);
+ Rewrite <-(Rplus_Ropp_l (Rmult (f x3) l'));Rewrite (Rmult_sym (f x3) l');
+ Rewrite <-(Ropp_mul1 l' (f x3));
+ Rewrite (Rmult_sym (Ropp l') (f x3));
+ Rewrite <-(Rplus_assoc (Rmult (f x3) (g x3)) 
+                     (Rmult (f x3) (Ropp l')) (Rmult l' (f x3)));
+ Rewrite <-(Rmult_Rplus_distr (f x3) (g x3) (Ropp l'));Fold (Rminus (g x3) l');
+ Generalize (Rabsolu_triang (Rmult (f x3) (Rminus (g x3) l'))
+                            (Rmult l' (f x3)));Intro;
+ Apply (Rle_lt_trans 
+   (Rabsolu (Rplus (Rmult (f x3) (Rminus (g x3) l')) (Rmult l' (f x3))))
+   (Rplus (Rabsolu (Rmult (f x3) (Rminus (g x3) l')))
+         (Rabsolu (Rmult l' (f x3)))) eps H12);Clear H12;
+ Rewrite (Rabsolu_mult (f x3) (Rminus (g x3) l'));
+ Rewrite (Rabsolu_mult l' (f x3));
+ Elim (Req_EM (f x3) R0);Intros.
+Rewrite H12;Rewrite Rabsolu_R0;
+ Rewrite (Rmult_Ol (Rabsolu (Rminus (g x3) l')));
+ Rewrite (Rmult_Or (Rabsolu l'));
+ Rewrite (let (H1,H2)=(Rplus_ne R0) in H1); 
+ Unfold Rgt in H1;Assumption.
+Generalize (Rabsolu_pos_lt (f x3) H12);Intro;
+ Fold (Rgt (Rabsolu (f x3)) R0) in H13;
+ Generalize (Rmult_lt (Rabsolu (Rminus (g x3) l')) 
+                      (Rmult eps (Rinv (Rplus R1 R1)))
+                      (Rabsolu (f x3)) R1 H13 (eps2_Rgt_R0 eps H1) 
+         H11 H8);Intro;
+ Generalize (Rlt_monotony (Rabsolu l') (Rabsolu (f x3))
+   (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))))  
+      (Rabsolu_pos_lt l' H2) H5);Clear H5 H8 H11 H12 H13;Intro;
+ Rewrite (Rmult_sym (Rabsolu (Rminus (g x3) l')) (Rabsolu (f x3))) 
+  in H14;Generalize (Rplus_lt 
+     (Rmult (Rabsolu (f x3)) (Rabsolu (Rminus (g x3) l')))
+     (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
+     (Rmult (Rabsolu l') (Rabsolu (f x3)))
+     (Rmult (Rabsolu l')
+        (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))))) H14 H5);
+ Clear H5 H14;Intro;
+ Cut eps==(Rplus (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
+             (Rmult (Rabsolu l')
+               (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l')))))).
+Intro;Rewrite <-H8 in H5;Assumption.
+Rewrite (let (H1,H2)=
+  (Rmult_ne (Rmult eps (Rinv (Rplus R1 R1)))) in H1);
+ Cut ~(Rabsolu l')==R0. 
+Intro;Rewrite (Rinv_Rmult (Rplus R1 R1) (Rabsolu l'));Auto.
+Rewrite (Rmult_sym (Rabsolu l') 
+  (Rmult eps (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l')))));
+ Rewrite (Rmult_assoc eps 
+    (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l')))
+    (Rabsolu l'));
+ Rewrite (Rmult_assoc (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l'))
+   (Rabsolu l'));
+ Rewrite (Rinv_l (Rabsolu l') H8);
+ Rewrite (let (H1,H2)=
+  (Rmult_ne (Rinv (Rplus R1 R1))) in H1);
+ Apply sym_eqT;Apply eps2.
+Apply (imp_not_Req (Rplus R1 R1) R0);Right;Unfold Rgt;Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H11);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H12;
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H11 H12).
+Generalize (Rabsolu_pos_lt l' H2);Intro;
+ Apply (imp_not_Req (Rabsolu l') R0);Auto.
+Unfold Rgt;Unfold Rgt in H1;
+ Rewrite <-(Rmult_Or (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))));
+ Rewrite (Rmult_sym eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))));
+ Apply (Rlt_monotony (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))) R0 eps);
+ Auto.
+Apply (Rlt_Rinv (Rmult (Rplus R1 R1) (Rabsolu l')));
+ Generalize (Rabsolu_pos_lt l' H2);
+ Clear H H0 H3 H4 H5 H7 H8 f g D l x0 x x1;Intro;
+ Rewrite <-(Rmult_Or (Rplus R1 R1)); 
+ Apply (Rlt_monotony (Rplus R1 R1) R0 (Rabsolu l'));Auto.
+Unfold Rgt in H6;Generalize (Rlt_compatibility R1 R0 R1 H6);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H0;
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H6 H0).
+(**)
+Rewrite H2;Rewrite H2 in H0;Rewrite (Rmult_Or l);
+ Elim (H (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));Intros;
+ Elim H4;Clear H4;Intros;
+ Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;Elim (H0 R1 H6);Intros;
+ Elim H7;Clear H7;Intros;
+ Cut (Rgt (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l)))) R0).
+Intro;Elim (H0 (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l)))) H9);
+ Intros;Elim H10;Clear H10;Intros;Split with (Rmin (Rmin x x1) x2);
+ Split.
+Elim (Rmin_Rgt (Rmin x x1) x2 R0);Intros;Elim (Rmin_Rgt x x1 R0);Intros;
+ Generalize (H15 (conj (Rgt x R0) (Rgt x1 R0) H4 H7));Clear H14 H15;
+ Intro;Clear H12;
+ Apply (H13 (conj (Rgt (Rmin x x1) R0) (Rgt x2 R0) H14 H10)).
+Intros;Elim H12;Clear H12;Intros;
+ Elim (Rmin_Rgt (Rmin x x1) x2 (R_dist x3 x0));Intros;Clear H15;
+ Unfold 1 Rgt in H14;Elim (H14 H13);Clear H14;Intros;Unfold Rgt in H15;
+ Clear H13;Elim (Rmin_Rgt x x1 (R_dist x3 x0));Intros;
+ Elim (H13 H14);Clear H14 H13 H16;Intros;Unfold Rgt in H13 H14;
+ Generalize (H5 x3 (conj (D x3) (Rlt (R_dist x3 x0) x) H12 H13));
+ Generalize (H8 x3 (conj (D x3) (Rlt (R_dist x3 x0) x1) H12 H14));
+ Generalize (H11 x3 (conj (D x3) (Rlt (R_dist x3 x0) x2) H12 H15));
+ Clear H5 H8 H11 H15 H13 H14 H12;Intros;Unfold R_dist in H5 H8 H11;
+ Unfold R_dist;Rewrite (minus_R0 (Rmult (f x3) (g x3)));
+ Rewrite (minus_R0 (g x3)) in H8;Rewrite (minus_R0 (g x3)) in H5;
+ Rewrite <-(let (H1,H2)=(Rplus_ne (Rmult (f x3) (g x3))) in H1);
+ Rewrite <-(Rplus_Ropp_l (Rmult (g x3) l));Rewrite (Rmult_sym (g x3) l);
+ Rewrite <-(Ropp_mul1 l (g x3));
+ Rewrite (Rmult_sym (Ropp l) (g x3));
+ Rewrite <-(Rplus_assoc (Rmult (f x3) (g x3)) 
+                     (Rmult (g x3) (Ropp l)) (Rmult l (g x3)));
+ Rewrite (Rmult_sym (f x3) (g x3));
+ Rewrite <-(Rmult_Rplus_distr (g x3) (f x3) (Ropp l));Fold (Rminus (f x3) l);
+ Generalize (Rabsolu_triang (Rmult (g x3) (Rminus (f x3) l))
+                            (Rmult l (g x3)));Intro;
+ Apply (Rle_lt_trans 
+   (Rabsolu (Rplus (Rmult (g x3) (Rminus (f x3) l)) (Rmult l (g x3))))
+   (Rplus (Rabsolu (Rmult (g x3) (Rminus (f x3) l)))
+         (Rabsolu (Rmult l (g x3)))) eps H12);Clear H12;
+ Rewrite (Rabsolu_mult (g x3) (Rminus (f x3) l));
+ Rewrite (Rabsolu_mult l (g x3));
+ Elim (Req_EM (g x3) R0);Intros.
+Rewrite H12;Rewrite Rabsolu_R0;
+ Rewrite (Rmult_Ol (Rabsolu (Rminus (f x3) l)));
+ Rewrite (Rmult_Or (Rabsolu l));
+ Rewrite (let (H1,H2)=(Rplus_ne R0) in H1); 
+ Unfold Rgt in H1;Assumption.
+Generalize (Rabsolu_pos_lt (g x3) H12);Intro;
+ Fold (Rgt (Rabsolu (g x3)) R0) in H13;
+ Generalize (Rmult_lt (Rabsolu (Rminus (f x3) l)) 
+                      (Rmult eps (Rinv (Rplus R1 R1)))
+                      (Rabsolu (g x3)) R1 H13 (eps2_Rgt_R0 eps H1) 
+         H11 H8);Intro;
+ Generalize (Rlt_monotony (Rabsolu l) (Rabsolu (g x3))
+   (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))))  
+      (Rabsolu_pos_lt l H3) H5);Clear H5 H8 H11 H12 H13;Intro;
+ Rewrite (Rmult_sym (Rabsolu (Rminus (f x3) l)) (Rabsolu (g x3))) 
+  in H14;Generalize (Rplus_lt 
+     (Rmult (Rabsolu (g x3)) (Rabsolu (Rminus (f x3) l)))
+     (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
+     (Rmult (Rabsolu l) (Rabsolu (g x3)))
+     (Rmult (Rabsolu l)
+        (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))))) H14 H5);
+ Clear H5 H14;Intro;
+ Cut eps==(Rplus (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
+             (Rmult (Rabsolu l)
+               (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l)))))).
+Intro;Rewrite <-H8 in H5;Assumption.
+Rewrite (let (H1,H2)=
+  (Rmult_ne (Rmult eps (Rinv (Rplus R1 R1)))) in H1);
+ Cut ~(Rabsolu l)==R0. 
+Intro;Rewrite (Rinv_Rmult (Rplus R1 R1) (Rabsolu l));Auto.
+Rewrite (Rmult_sym (Rabsolu l) 
+  (Rmult eps (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l)))));
+ Rewrite (Rmult_assoc eps 
+    (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l)))
+    (Rabsolu l));
+ Rewrite (Rmult_assoc (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l))
+   (Rabsolu l));
+ Rewrite (Rinv_l (Rabsolu l) H8);
+ Rewrite (let (H1,H2)=
+  (Rmult_ne (Rinv (Rplus R1 R1))) in H1);
+ Apply sym_eqT;Apply eps2.
+Apply (imp_not_Req (Rplus R1 R1) R0);Right;Unfold Rgt;Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H11);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H12;
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H11 H12).
+Generalize (Rabsolu_pos_lt l H3);Intro;
+ Apply (imp_not_Req (Rabsolu l) R0);Auto.
+Unfold Rgt;Unfold Rgt in H1;
+ Rewrite <-(Rmult_Or (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))));
+ Rewrite (Rmult_sym eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))));
+ Apply (Rlt_monotony (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))) R0 eps);
+ Auto.
+Apply (Rlt_Rinv (Rmult (Rplus R1 R1) (Rabsolu l)));
+ Generalize (Rabsolu_pos_lt l H3);
+ Clear H H0 H2 H4 H5 H7 H8 f g D l' x0 x x1;Intro;
+ Rewrite <-(Rmult_Or (Rplus R1 R1)); 
+ Apply (Rlt_monotony (Rplus R1 R1) R0 (Rabsolu l));Auto.
+Unfold Rgt in H6;Generalize (Rlt_compatibility R1 R0 R1 H6);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H0;
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H6 H0).
+(**)
+Cut ~(Rplus (Rplus R1 R1) (Rplus R1 R1))==R0.
+Cut ~(Rabsolu l)==R0.
+Cut ~(Rabsolu l')==R0.
+Intros tl' tl add4;
+ Elim (H (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
+ Intros;Elim H4;Clear H4;Intros;
+ Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;Elim (H0 R1 H6);Intros;
+ Elim H7;Clear H7;Intros;
+ Cut (Rgt (Rmult eps 
+ (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))) R0).
+Cut (Rgt (Rmult eps 
+ (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l')))) R0).
+Intros;Elim (H0 (Rmult eps 
+   (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))) H10);
+ Intros;Elim H11;Clear H11;Intros;
+ Elim (H (Rmult eps 
+   (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l')))) H9);
+ Intros;Elim H13;Clear H13;Intros;
+ Split with (Rmin (Rmin x x1) (Rmin x2 x3));Split.
+Elim (Rmin_Rgt (Rmin x x1) (Rmin x2 x3) R0);Intros;
+ Elim (Rmin_Rgt x x1 R0);Elim (Rmin_Rgt x2 x3 R0);Intros;
+ Apply (H16 (conj (Rgt (Rmin x x1) R0) (Rgt (Rmin x2 x3) R0) 
+  (H20 (conj (Rgt x R0) (Rgt x1 R0) H4 H7)) 
+  (H18 (conj (Rgt x2 R0) (Rgt x3 R0) H11 H13)))).
+Intros;Elim H15;Clear H15;Intros;
+ Elim (Rmin_Rgt (Rmin x x1) (Rmin x2 x3) (R_dist x4 x0));Intros;
+ Clear H18;Unfold 1 Rgt in H17;Elim (H17 H16);Clear H17 H16;Intros;
+ Elim (Rmin_Rgt x x1 (R_dist x4 x0));
+ Elim (Rmin_Rgt x2 x3 (R_dist x4 x0));Intros;
+ Unfold 1 Rgt in H17;Unfold 1 Rgt in H20;Elim (H18 H17);Elim (H20 H16);
+ Clear H16 H17 H18 H19 H20 H21;Intros;Unfold Rgt in H16 H17 H18 H19;
+ Generalize (H5 x4 (conj (D x4) (Rlt (R_dist x4 x0) x) H15 H16));
+ Generalize (H8 x4 (conj (D x4) (Rlt (R_dist x4 x0) x1) H15 H17));
+ Generalize (H12 x4 (conj (D x4) (Rlt (R_dist x4 x0) x2) H15 H18));
+ Generalize (H14 x4 (conj (D x4) (Rlt (R_dist x4 x0) x3) H15 H19));
+ Clear H H0 H5 H8 H12 H14 H16 H17 H18 H19;Intros;
+ Unfold R_dist in H H0 H5 H8;Unfold R_dist; 
+ Rewrite <-(let (H1,H2)=(Rplus_ne (Rmult (f x4) (g x4))) in H1);
+ Rewrite <-(Rplus_Ropp_l (Rmult (g x4) l));Rewrite (Rmult_sym (g x4) l);
+ Rewrite <-(Ropp_mul1 l (g x4));
+ Rewrite (Rmult_sym (Ropp l) (g x4));
+ Rewrite <-(Rplus_assoc (Rmult (f x4) (g x4)) 
+                     (Rmult (g x4) (Ropp l)) (Rmult l (g x4)));
+ Rewrite (Rmult_sym (f x4) (g x4));
+ Rewrite <-(Rmult_Rplus_distr (g x4) (f x4) (Ropp l));Fold (Rminus (f x4) l);
+ Unfold 1 Rminus;Rewrite (Rmult_sym l l');Rewrite <-(Ropp_mul1 l' l);
+ Rewrite (Rmult_sym (Ropp l') l);
+ Rewrite (Rplus_assoc (Rmult (g x4) (Rminus (f x4) l)) 
+                     (Rmult l (g x4)) (Rmult l (Ropp l')));
+ Rewrite <-(Rmult_Rplus_distr l (g x4) (Ropp l'));
+ Fold (Rminus (g x4) l');
+ Generalize (Rabsolu_triang (Rmult (g x4) (Rminus (f x4) l))
+                            (Rmult l (Rminus (g x4) l')));Intro;
+ Apply (Rle_lt_trans 
+   (Rabsolu (Rplus (Rmult (g x4) (Rminus (f x4) l)) 
+                  (Rmult l (Rminus (g x4) l'))))
+   (Rplus (Rabsolu (Rmult (g x4) (Rminus (f x4) l)))
+         (Rabsolu (Rmult l (Rminus (g x4) l')))) eps H12);Clear H12;
+ Generalize (Rlt_monotony (Rabsolu l) (Rabsolu (Rminus (g x4) l')) 
+                      (Rmult eps
+           (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))))
+                      (Rabsolu_pos_lt l H3) H0);Intro;
+ Generalize (Rlt_monotony (Rabsolu l') (Rabsolu (Rminus (f x4) l)) 
+                      (Rmult eps
+           (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l'))))
+                      (Rabsolu_pos_lt l' H2) H);Intro;
+ Elim (Req_EM (f x4) l);Intros.
+Rewrite H16;Rewrite (eq_Rminus l l (refl_eqT R l));
+ Rewrite (Rmult_Or (g x4));Rewrite Rabsolu_R0;
+ Rewrite (let (H1,H2)=(Rplus_ne (Rabsolu (Rmult l (Rminus (g x4) l')))) 
+   in H2);Rewrite (Rabsolu_mult l (Rminus (g x4) l'));
+ Apply (Rlt_trans (Rmult (Rabsolu l) (Rabsolu (Rminus (g x4) l')))
+     (Rmult (Rabsolu l)
+            (Rmult eps
+              (Rinv
+                (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))))
+     eps H12); 
+ Rewrite (Rmult_sym eps 
+   (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))));
+ Rewrite <-(Rmult_assoc (Rabsolu l) 
+  (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))) eps);
+ Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l) add4 
+    tl);
+ Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
+                     (Rinv (Rabsolu l))); 
+ Rewrite <-(Rmult_assoc (Rabsolu l) (Rinv (Rabsolu l)) 
+                      (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))));
+ Rewrite (Rinv_r (Rabsolu l) tl);
+ Rewrite (let (H1,H2)=(Rmult_ne (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))))
+  in H2);Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
+           eps);Apply (Rlt_eps4_eps eps H1).
+Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;
+ Cut (Rgt (Rabsolu (Rminus (f x4) l)) R0).
+Intro;
+ Generalize (Rmult_lt (Rabsolu (Rminus (g x4) l')) R1 
+                     (Rabsolu (Rminus (f x4) l)) 
+                     (Rmult eps (Rinv (Rplus R1 R1)))
+                      H18 H17 H5 H8);Intro;
+ Rewrite (let (H1,H2)=(Rmult_ne (Rmult eps (Rinv (Rplus R1 R1)))) in H2)
+  in H19;Generalize (Rplus_lt (Rmult (Rabsolu (Rminus (g x4) l'))
+            (Rabsolu (Rminus (f x4) l)))
+                             (Rmult eps (Rinv (Rplus R1 R1)))
+                      (Rmult (Rabsolu l') (Rabsolu (Rminus (f x4) l)))
+                      (Rmult (Rabsolu l')
+            (Rmult eps (Rinv
+                (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l')))))
+              H19 H14);Intro;
+ Generalize (Rplus_lt (Rmult (Rabsolu l) (Rabsolu (Rminus (g x4) l')))
+                     (Rmult (Rabsolu l)
+            (Rmult eps
+              (Rinv
+                (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))))
+             (Rplus
+            (Rmult (Rabsolu (Rminus (g x4) l'))
+              (Rabsolu (Rminus (f x4) l)))
+            (Rmult (Rabsolu l') (Rabsolu (Rminus (f x4) l))))
+            (Rplus (Rmult eps (Rinv (Rplus R1 R1)))
+            (Rmult (Rabsolu l')
+              (Rmult eps
+                (Rinv
+              (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l'))))))
+              H12 H20);
+ Clear H5 H8 H12 H14 H19 H20 H H0 H9 H10;Replace (Rplus
+            (Rmult (Rabsolu l)
+              (Rmult eps
+                (Rinv
+                  (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))))
+            (Rplus (Rmult eps (Rinv (Rplus R1 R1)))
+              (Rmult (Rabsolu l')
+                (Rmult eps
+                  (Rinv
+                    (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1))
+                      (Rabsolu l'))))))) with eps.
+Intro;Rewrite (Rplus_sym (Rabsolu (Rmult (g x4) (Rminus (f x4) l)))
+           (Rabsolu (Rmult l (Rminus (g x4) l'))));
+ Pattern 2 (g x4);
+ Rewrite <-(let (H1,H2)=(Rplus_ne (g x4)) in H1);
+ Rewrite <-(Rplus_Ropp_r l');Rewrite <-(Rplus_assoc (g x4) l' (Ropp l')); 
+ Rewrite (Rmult_sym (Rplus (Rplus (g x4) l') (Ropp l')) 
+                      (Rminus (f x4) l));
+ Rewrite (Rabsolu_mult (Rminus (f x4) l)
+                      (Rplus (Rplus (g x4) l') (Ropp l')));
+ Rewrite (Rmult_sym (Rabsolu (Rminus (g x4) l'))
+                      (Rabsolu (Rminus (f x4) l))) in H;
+ Rewrite (Rmult_sym (Rabsolu l') 
+                      (Rabsolu (Rminus (f x4) l))) in H;
+ Rewrite <-(Rmult_Rplus_distr (Rabsolu (Rminus (f x4) l))
+                  (Rabsolu (Rminus (g x4) l'))
+                  (Rabsolu l')) in H;
+ Rewrite <-(Rabsolu_mult l (Rminus (g x4) l')) in H;
+ Rewrite (Rplus_assoc (g x4) l' (Ropp l'));
+ Rewrite (Rplus_sym l' (Ropp l'));
+ Rewrite <-(Rplus_assoc (g x4) (Ropp l') l');
+ Fold (Rminus (g x4) l');
+ Generalize (Rabsolu_triang (Rminus (g x4) l') l');Intro;
+ Unfold Rle in H0;Elim H0;Clear H0;Intro.
+Unfold Rgt in H18.
+ Generalize (Rlt_monotony (Rabsolu (Rminus (f x4) l)) 
+        (Rabsolu (Rplus (Rminus (g x4) l') l'))
+        (Rplus (Rabsolu (Rminus (g x4) l')) (Rabsolu l')) 
+        H18 H0);Intro;
+ Generalize (Rlt_compatibility (Rabsolu (Rmult l (Rminus (g x4) l')))
+        (Rmult (Rabsolu (Rminus (f x4) l))
+           (Rabsolu (Rplus (Rminus (g x4) l') l')))
+        (Rmult (Rabsolu (Rminus (f x4) l))
+           (Rplus (Rabsolu (Rminus (g x4) l')) (Rabsolu l')))
+        H5);Clear H0 H5;Intro;
+ Apply (Rlt_trans (Rplus (Rabsolu (Rmult l (Rminus (g x4) l')))
+           (Rmult (Rabsolu (Rminus (f x4) l))
+             (Rabsolu (Rplus (Rminus (g x4) l') l'))))
+                   (Rplus (Rabsolu (Rmult l (Rminus (g x4) l')))
+           (Rmult (Rabsolu (Rminus (f x4) l))
+             (Rplus (Rabsolu (Rminus (g x4) l')) (Rabsolu l'))))
+                   eps H0 H).
+Rewrite H0;Assumption. 
+Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1))
+                            (Rabsolu l) add4 tl);
+ Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1))
+                            (Rabsolu l') add4 tl');
+ Rewrite (Rmult_sym eps (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
+              (Rinv (Rabsolu l))));
+ Rewrite (Rmult_sym eps (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
+              (Rinv (Rabsolu l'))));
+ Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) 
+                      (Rinv (Rabsolu l)));
+ Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) 
+                      (Rinv (Rabsolu l')));
+ Rewrite (Rmult_assoc (Rinv (Rabsolu l)) 
+        (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps);
+ Rewrite (Rmult_assoc (Rinv (Rabsolu l')) 
+        (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps);
+ Rewrite <-(Rmult_assoc (Rabsolu l) (Rinv (Rabsolu l))
+        (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps));
+ Rewrite <-(Rmult_assoc (Rabsolu l') (Rinv (Rabsolu l'))
+        (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps));
+ Rewrite (Rinv_r (Rabsolu l) tl);Rewrite (Rinv_r (Rabsolu l') tl');
+ Rewrite (let (H1,H2)=(Rmult_ne 
+      (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps)) in H2);
+ Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps);
+ Rewrite (Rplus_sym (Rmult eps (Rinv (Rplus R1 R1)))
+                  (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))));
+ Rewrite <- (Rplus_assoc 
+     (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))))
+     (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))))
+     (Rmult eps (Rinv (Rplus R1 R1))));
+ Rewrite eps4;Rewrite eps2;Trivial.
+Unfold Rgt;Apply (Rabsolu_pos_lt (Rminus (f x4) l));Red;Intro;Elim H16;
+ Apply (Rminus_eq (f x4) l H18).
+Apply (Rmult_gt eps 
+  (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l'))) H1);
+ Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l') 
+           add4 tl'); 
+ Apply (Rmult_gt (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) 
+  (Rinv (Rabsolu l'))).
+Unfold Rgt;Apply (Rlt_Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))).
+Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H9);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H10;
+ Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H9 H10);Intro;
+ Clear H9 H10;
+ Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H11);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H9;
+ Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
+    H11 H9).
+Unfold Rgt;Apply (Rlt_Rinv (Rabsolu l') (Rabsolu_pos_lt l' H2)).
+Apply (Rmult_gt eps 
+  (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))) H1);
+ Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l) 
+           add4 tl); 
+ Apply (Rmult_gt (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) 
+  (Rinv (Rabsolu l))).
+Unfold Rgt;Apply (Rlt_Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))).
+Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H9);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H10;
+ Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H9 H10);Intro;
+ Clear H9 H10;
+ Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H11);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H9;
+ Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
+    H11 H9).
+Unfold Rgt;Apply (Rlt_Rinv (Rabsolu l) (Rabsolu_pos_lt l H3)).
+Generalize (Rabsolu_pos_lt l' H2);Intro;
+ Apply (imp_not_Req (Rabsolu l') R0);Auto.
+Generalize (Rabsolu_pos_lt l H3);Intro;
+ Apply (imp_not_Req (Rabsolu l) R0);Auto.
+Apply (imp_not_Req (Rplus (Rplus R1 R1) (Rplus R1 R1)) R0);Right;Unfold Rgt;
+ Generalize Rlt_R0_R1;Intro;
+ Generalize (Rlt_compatibility R1 R0 R1 H4);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H5;
+ Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H4 H5);Intro;
+ Clear H4 H5;
+ Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H6);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H4;
+ Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
+    H6 H4).
+Save.
+
+(*********)
+Definition adhDa:(R->Prop)->R->Prop:=[D:R->Prop][a:R]
+  (alp:R)(Rgt alp R0)->(EXT x:R | (D x)/\(Rlt (R_dist x a) alp)).
+
+(*********)
+Lemma single_limit:(f:R->R)(D:R->Prop)(l:R)(l':R)(x0:R)
+  (adhDa D x0)->(limit1_in f D l x0)->(limit1_in f D l' x0)->l==l'.
+Unfold limit1_in; Unfold limit_in; Intros.
+Cut (eps:R)(Rgt eps R0)->(Rlt (dist R_met l l') 
+                              (Rmult (Rplus R1 R1) eps)).
+Clear H0 H1;Unfold dist; Unfold R_met; Unfold R_dist; 
+ Unfold Rabsolu;Case (case_Rabsolu (Rminus l l')); Intros.
+Cut (eps:R)(Rgt eps R0)->(Rlt (Ropp (Rminus l l')) eps).
+Intro;Generalize (prop_eps (Ropp (Rminus l l')) H1);Intro;
+ Generalize (Rlt_RoppO (Rminus l l') r); Intro;Unfold Rgt in H3;
+ Generalize (Rle_not (Ropp (Rminus l l')) R0 H3); Intro;
+ ElimType False; Auto.
+Intros;Cut (Rgt (Rmult eps (Rinv (Rplus R1 R1))) R0).
+Intro;Generalize (H0 (Rmult eps (Rinv (Rplus R1 R1))) H2);
+ Rewrite (Rmult_sym eps (Rinv (Rplus R1 R1)));
+ Rewrite <- (Rmult_assoc (Rplus R1 R1) (Rinv (Rplus R1 R1)) eps);
+ Rewrite (Rinv_r (Rplus R1 R1)).
+Elim (Rmult_ne eps);Intros a b;Rewrite b;Clear a b;Trivial.
+Apply (imp_not_Req (Rplus R1 R1) R0);Right;Generalize Rlt_R0_R1;Intro;
+ Unfold Rgt;Generalize (Rlt_compatibility R1 R0 R1 H3);Intro;
+ Elim (Rplus_ne R1);Intros a b;Rewrite a in H4;Clear a b; 
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H3 H4).
+Unfold Rgt;Unfold Rgt in H1;
+ Rewrite (Rmult_sym eps(Rinv (Rplus R1 R1)));
+ Rewrite <-(Rmult_Or (Rinv (Rplus R1 R1)));
+ Apply (Rlt_monotony (Rinv (Rplus R1 R1)) R0 eps);Auto.
+Apply (Rlt_Rinv (Rplus R1 R1));Cut (Rlt R1 (Rplus R1 R1)).
+Intro;Apply (Rlt_trans R0 R1 (Rplus R1 R1) Rlt_R0_R1 H2).
+Generalize (Rlt_compatibility R1 R0 R1 Rlt_R0_R1);Elim (Rplus_ne R1);
+ Intros a b;Rewrite a;Clear a b;Trivial.
+(**)
+Cut (eps:R)(Rgt eps R0)->(Rlt (Rminus l l') eps).
+Intro;Generalize (prop_eps (Rminus l l') H1);Intro;
+ Elim (Rle_le_eq (Rminus l l') R0);Intros a b;Clear b;
+ Apply (Rminus_eq l l');Apply a;Split.
+Assumption.
+Apply (Rle_sym2 R0 (Rminus l l') r).
+Intros;Cut (Rgt (Rmult eps (Rinv (Rplus R1 R1))) R0).
+Intro;Generalize (H0 (Rmult eps (Rinv (Rplus R1 R1))) H2);
+ Rewrite (Rmult_sym eps (Rinv (Rplus R1 R1)));
+ Rewrite <- (Rmult_assoc (Rplus R1 R1) (Rinv (Rplus R1 R1)) eps);
+ Rewrite (Rinv_r (Rplus R1 R1)).
+Elim (Rmult_ne eps);Intros a b;Rewrite b;Clear a b;Trivial.
+Apply (imp_not_Req (Rplus R1 R1) R0);Right;Generalize Rlt_R0_R1;Intro;
+ Unfold Rgt;Generalize (Rlt_compatibility R1 R0 R1 H3);Intro;
+ Elim (Rplus_ne R1);Intros a b;Rewrite a in H4;Clear a b; 
+ Apply (Rlt_trans R0 R1 (Rplus R1 R1) H3 H4).
+Unfold Rgt;Unfold Rgt in H1;
+ Rewrite (Rmult_sym eps(Rinv (Rplus R1 R1)));
+ Rewrite <-(Rmult_Or (Rinv (Rplus R1 R1)));
+ Apply (Rlt_monotony (Rinv (Rplus R1 R1)) R0 eps);Auto.
+Apply (Rlt_Rinv (Rplus R1 R1));Cut (Rlt R1 (Rplus R1 R1)).
+Intro;Apply (Rlt_trans R0 R1 (Rplus R1 R1) Rlt_R0_R1 H2).
+Generalize (Rlt_compatibility R1 R0 R1 Rlt_R0_R1);Elim (Rplus_ne R1);
+ Intros a b;Rewrite a;Clear a b;Trivial.
+(**)
+Intros;Unfold adhDa in H;Elim (H0 eps H2);Intros;Elim (H1 eps H2);
+ Intros;Clear H0 H1;Elim H3;Elim H4;Clear H3 H4;Intros;
+ Simpl;Simpl in H1 H4;Generalize (Rmin_Rgt x x1 R0);Intro;Elim H5;
+ Intros;Clear H5;
+ Elim (H (Rmin x x1) (H7 (conj (Rgt x R0) (Rgt x1 R0) H3 H0)));
+ Intros; Elim H5;Intros;Clear H5 H H6 H7;
+ Generalize (Rmin_Rgt x x1 (R_dist x2 x0));Intro;Elim H;
+ Intros;Clear H H6;Unfold Rgt in H5;Elim (H5 H9);Intros;Clear H5 H9;
+ Generalize (H1 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H8 H6));
+ Generalize (H4 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H8 H));
+ Clear H8 H H6 H1 H4 H0 H3;Intros;
+ Generalize (Rplus_lt (R_dist (f x2) l) eps (R_dist (f x2) l') eps 
+  H H0); Unfold R_dist;Intros;
+ Rewrite (Rabsolu_minus_sym (f x2) l) in H1;
+ Rewrite (Rmult_sym (Rplus R1 R1) eps);Rewrite (Rmult_Rplus_distr eps R1 R1);
+ Elim (Rmult_ne eps);Intros a b;Rewrite a;Clear a b;
+ Generalize (R_dist_tri l l' (f x2));Unfold R_dist;Intros;
+ Apply (Rle_lt_trans (Rabsolu (Rminus l l')) 
+  (Rplus (Rabsolu (Rminus l (f x2))) (Rabsolu (Rminus (f x2) l')))
+  (Rplus eps eps) H3 H1).
+Save.
+
+(*********)
+Lemma limit_comp:(f,g:R->R)(Df,Dg:R->Prop)(l,l':R)(x0:R)
+   (limit1_in f Df l x0)->(limit1_in g Dg l' l)->
+   (limit1_in [x:R](g (f x)) (Dgf Df Dg f) l' x0).
+Unfold limit1_in;Unfold limit_in;Simpl;Intros;
+ Elim (H0 eps H1);Clear H0;Intros;Elim H0;Clear H0;Intros;
+ Elim (H x H0);Clear H;Intros;Elim H;Clear H;Intros;
+ Split with x1;Split;Auto;Intros;
+ Elim H4;Clear H4;Intros;Unfold Dgf in H4;Elim H4;Clear H4;Intros;
+ Generalize (H3 x2 (conj (Df x2) (Rlt (R_dist x2 x0) x1) H4 H5));
+ Intro;Exact (H2 (f x2) (conj (Dg (f x2)) (Rlt (R_dist (f x2) l) x)
+            H6 H7)).
+Save.
diff --git a/theories/Reals/TypeSyntax.v b/theories/Reals/TypeSyntax.v
new file mode 100644
index 000000000..9b68928ba
--- /dev/null
+++ b/theories/Reals/TypeSyntax.v
@@ -0,0 +1,25 @@
+
+(* $Id$ *)
+
+(*********************************************************)
+(*        Or and Exist in Type                           *)
+(*                                                       *)
+(*********************************************************)
+
+(**********)
+Inductive sumboolT [A,B:Prop]:Type:=
+   leftT : A->(sumboolT A B)
+  |rightT: B->(sumboolT A B).
+
+(**********)
+Inductive sumorT [A:Type;B:Prop]:Type:=
+   inleftT : A->(sumorT A B)
+  |inrightT: B->(sumorT A B).
+
+(**********)
+Inductive sigT [A:Set;P:A->Prop]:Type:=
+   existT: (x:A)(P x)->(sigT A P).
+
+(**********)
+Inductive sigTT [A:Type;P:A->Prop]:Type:=
+   existTT: (x:A)(P x)->(sigTT A P).