Ajout de Rseries et Rtrigo_fun

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

10 files changed, 681 insertions, 27 deletions

diff --git a/.depend b/.depend
index 247a565b56..a276f5d11d 100644
--- a/.depend
+++ b/.depend
@@ -1463,11 +1463,11 @@ contrib/correctness/pmonad.cmx: kernel/names.cmx contrib/correctness/past.cmi \
     contrib/correctness/putil.cmx kernel/term.cmx parsing/termast.cmx \
     lib/util.cmx contrib/correctness/pmonad.cmi 
 contrib/correctness/pred.cmo: kernel/evd.cmi library/global.cmi \
-    contrib/correctness/past.cmi lib/pp.cmi kernel/reduction.cmi \
-    kernel/term.cmi contrib/correctness/pred.cmi 
+    contrib/correctness/past.cmi contrib/correctness/pmisc.cmi lib/pp.cmi \
+    kernel/reduction.cmi kernel/term.cmi contrib/correctness/pred.cmi 
 contrib/correctness/pred.cmx: kernel/evd.cmx library/global.cmx \
-    contrib/correctness/past.cmi lib/pp.cmx kernel/reduction.cmx \
-    kernel/term.cmx contrib/correctness/pred.cmi 
+    contrib/correctness/past.cmi contrib/correctness/pmisc.cmx lib/pp.cmx \
+    kernel/reduction.cmx kernel/term.cmx contrib/correctness/pred.cmi 
 contrib/correctness/prename.cmo: toplevel/himsg.cmi kernel/names.cmi \
     contrib/correctness/pmisc.cmi lib/pp.cmi lib/util.cmi \
     contrib/correctness/prename.cmi 
@@ -1606,22 +1606,24 @@ contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \
     pretyping/typing.cmx lib/util.cmx contrib/extraction/extraction.cmi 
 contrib/extraction/mlutil.cmo: kernel/declarations.cmi library/global.cmi \
     library/lib.cmi library/libobject.cmi contrib/extraction/miniml.cmi \
-    kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \
-    library/summary.cmi kernel/term.cmi lib/util.cmi \
+    kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
+    parsing/printer.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
     toplevel/vernacinterp.cmi contrib/extraction/mlutil.cmi 
 contrib/extraction/mlutil.cmx: kernel/declarations.cmx library/global.cmx \
     library/lib.cmx library/libobject.cmx contrib/extraction/miniml.cmi \
-    kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \
-    library/summary.cmx kernel/term.cmx lib/util.cmx \
+    kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
+    parsing/printer.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx contrib/extraction/mlutil.cmi 
 contrib/extraction/ocaml.cmo: kernel/environ.cmi library/global.cmi \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
-    kernel/names.cmi lib/pp.cmi lib/pp_control.cmi kernel/term.cmi \
-    lib/util.cmi contrib/extraction/ocaml.cmi 
+    kernel/names.cmi lib/options.cmi lib/pp.cmi lib/pp_control.cmi \
+    parsing/printer.cmi kernel/term.cmi lib/util.cmi \
+    contrib/extraction/ocaml.cmi 
 contrib/extraction/ocaml.cmx: kernel/environ.cmx library/global.cmx \
     contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
-    kernel/names.cmx lib/pp.cmx lib/pp_control.cmx kernel/term.cmx \
-    lib/util.cmx contrib/extraction/ocaml.cmi 
+    kernel/names.cmx lib/options.cmx lib/pp.cmx lib/pp_control.cmx \
+    parsing/printer.cmx kernel/term.cmx lib/util.cmx \
+    contrib/extraction/ocaml.cmi 
 contrib/field/field.cmo: parsing/astterm.cmi parsing/coqast.cmi \
     library/declare.cmi kernel/evd.cmi library/global.cmi library/lib.cmi \
     library/libobject.cmi kernel/names.cmi library/nametab.cmi \
diff --git a/.depend.coq b/.depend.coq
index 47db4e775f..73cf87b8a3 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -44,14 +44,17 @@ theories/Relations/Relation_Definitions.vo: theories/Relations/Relation_Definiti
 theories/Relations/Operators_Properties.vo: theories/Relations/Operators_Properties.v theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo
 theories/Relations/Newman.vo: theories/Relations/Newman.v theories/Relations/Rstar.vo
 theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v
+theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
 theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
+theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rseries.vo
 theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo
+theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rderiv.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
 theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Reals/SplitAbsolu.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo
-theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rderiv.vo
+theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo contrib/omega/Omega.vo
+theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rlimit.vo theories/Reals/Rfunctions.vo theories/Reals/Rderiv.vo theories/Reals/Rseries.vo theories/Reals/Rtrigo_fun.vo
 theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
 theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith.vo theories/Reals/TypeSyntax.vo
-theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo
+theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo
 theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo
 theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
@@ -218,7 +221,7 @@ contrib/field/Field_Compl.vo: contrib/field/Field_Compl.v
 contrib/field/Field.vo: contrib/field/Field.v contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo contrib/field/field.cmo
 contrib/extraction/test_extraction.vo: contrib/extraction/test_extraction.v
 contrib/extraction/Extraction.vo: contrib/extraction/Extraction.v
-contrib/correctness/preuves.vo: contrib/correctness/preuves.v contrib/correctness/Correctness.vo contrib/omega/Omega.vo
+contrib/correctness/preuves.vo: contrib/correctness/preuves.v contrib/correctness/Correctness.vo contrib/omega/Omega.vo contrib/correctness/Exchange.vo contrib/correctness/ArrayPermut.vo
 contrib/correctness/Tuples.vo: contrib/correctness/Tuples.v
 contrib/correctness/Sorted.vo: contrib/correctness/Sorted.v contrib/correctness/Arrays.vo contrib/correctness/ArrayPermut.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo
 contrib/correctness/Programs_stuff.vo: contrib/correctness/Programs_stuff.v contrib/correctness/Arrays_stuff.vo
diff --git a/Makefile b/Makefile
index 735b24f885..18ebe16a6b 100644
--- a/Makefile
+++ b/Makefile
@@ -416,9 +416,10 @@ REALSVO=theories/Reals/TypeSyntax.vo \
 	theories/Reals/Raxioms.vo      theories/Reals/Rbase.vo \
 	theories/Reals/DiscrR.vo       theories/Reals/R_Ifp.vo \
 	theories/Reals/Rbasic_fun.vo   theories/Reals/SplitAbsolu.vo \
-	theories/Reals/SplitRmult.vo \
-	theories/Reals/Rfunctions.vo   theories/Reals/Rlimit.vo \
-	theories/Reals/Rderiv.vo       theories/Reals/Reals.vo 
+	theories/Reals/SplitRmult.vo   theories/Reals/Rfunctions.vo \
+	theories/Reals/Rlimit.vo       theories/Reals/Rderiv.vo \
+	theories/Reals/Rseries.vo      theories/Reals/Rtrigo_fun.vo \
+	theories/Reals/Reals.vo 
 
 THEORIESVO = $(LOGICVO) $(ARITHVO) $(BOOLVO) $(ZARITHVO) $(LISTSVO) \
              $(SETSVO) $(INTMAPVO) $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index d8c2d62f1b..1079323dc5 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -14,6 +14,7 @@
 (*********************************************************)
 
 Require Export R_Ifp.
+Require Fourier.
 
 (*******************************)
 (*           Rmin              *)
@@ -134,6 +135,11 @@ Generalize (Rlt_Ropp x R0 r);Intro;Unfold Rgt in H;
 Apply Rle_sym2;Assumption.
 Save.
 
+Lemma Rle_Rabsolu:
+ (x:R) (Rle x (Rabsolu x)).
+Intro; Unfold Rabsolu;Case (case_Rabsolu x);Intros;Fourier.
+Save.
+
 (*********)
 Lemma Rabsolu_pos_eq:(x:R)(Rle R0 x)->(Rabsolu x)==x.
 Intros;Unfold Rabsolu;Case (case_Rabsolu x);Intro;
@@ -237,6 +243,26 @@ Unfold Rgt in H0;Generalize (Rlt_antisym R0 (Rinv r)
 ElimType False;Auto.
 Save. 
 
+Lemma Rabsolu_Ropp:
+  (x:R) (Rabsolu (Ropp x))==(Rabsolu x).
+Intro;Cut (Ropp x)==(Rmult (Ropp R1) x).
+Intros; Rewrite H.
+Rewrite Rabsolu_mult.
+Cut (Rabsolu (Ropp R1))==R1.
+Intros; Rewrite H0.
+Ring.
+Unfold Rabsolu; Case (case_Rabsolu (Ropp R1)).
+Intro; Ring.
+Intro H0;Generalize (Rle_sym2 R0 (Ropp R1) H0);Intros.
+Generalize (Rle_Ropp R0 (Ropp R1) H1).
+Rewrite Ropp_Ropp; Rewrite Ropp_O.
+Intro;Generalize (Rle_not R1 R0 Rlt_R0_R1);Intro;
+ Generalize (Rle_sym2 R1 R0 H2);Intro;
+ ElimType False;Auto.  
+Ring.
+Save.
+
+
 (*********)
 Lemma Rabsolu_triang:(a,b:R)(Rle (Rabsolu (Rplus a b)) 
                                 (Rplus (Rabsolu a) (Rabsolu b))).
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index 01177db2ca..cb4f9347a3 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -17,3 +17,5 @@ Require Export Rbasic_fun.
 Require Export Rlimit.
 Require Export Rfunctions.
 Require Export Rderiv.
+Require Export Rseries.
+Require Export Rtrigo_fun.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 951c4de649..857969b74a 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -8,12 +8,14 @@
 
 (*i $Id$ i*)
 
+(*i Some properties about pow and sum have been made with John Harrison i*)
 (*********************************************************)
 (*           Definition of the some functions            *)
 (*                                                       *)
 (*********************************************************)
 
 Require Export Rlimit.
+Require Omega.
 
 (*******************************)
 (*      Factorial              *)
@@ -26,13 +28,6 @@ Fixpoint fact [n:nat]:nat:=
   end.
 
 (*********)
-(*i
-Lemma mult_neq_O:(n,m:nat)~n=O->~m=O->~(mult n m)=O.
-Double Induction 1 2;Simpl;Auto.
-Save.
-i*)
- 
-(*********)
 Lemma fact_neq_0:(n:nat)~(fact n)=O.
 Cut (n,m:nat)~n=O->~m=O->~(mult n m)=O.
 Intro;Induction n;Simpl;Auto.
@@ -92,6 +87,205 @@ Intros; Pattern 1 (pow x a);
  Apply Rmult_sym.
 Save.
 
+Lemma poly: (n:nat)(e:R)(Rlt R0 e)->
+ (Rle (Rplus R1 (Rmult (INR n) e)) (pow  (Rplus R1 e) n)).
+Intros;Elim n.
+Simpl;Cut (Rplus R1 (Rmult R0 e))==R1.
+Intro;Rewrite H0;Unfold Rle;Right; Reflexivity.
+Ring.
+Intros;Unfold pow; Fold pow;
+ Apply (Rle_trans (Rplus R1 (Rmult (INR (S n0)) e))
+    (Rmult (Rplus R1 e) (Rplus R1 (Rmult (INR n0) e))) 
+    (Rmult (Rplus R1 e) (pow (Rplus R1 e) n0))).
+Cut (Rmult (Rplus R1 e) (Rplus R1 (Rmult (INR n0) e)))== 
+  (Rplus (Rplus R1 (Rmult (INR (S n0)) e)) 
+         (Rmult (INR n0) (Rmult e e))).
+Intro;Rewrite H1;Pattern 1 (Rplus R1 (Rmult (INR (S n0)) e));
+ Rewrite <-(let (H1,H2)=
+   (Rplus_ne (Rplus R1 (Rmult (INR (S n0)) e))) in H1);
+ Apply Rle_compatibility;Elim n0;Intros.
+Simpl;Rewrite Rmult_Ol;Unfold Rle;Right;Auto.
+Unfold Rle;Left;Generalize Rmult_gt;Unfold Rgt;Intro;
+ Fold (Rsqr e);Apply (H3 (INR (S n1)) (Rsqr e) 
+        (INR_lt_0 (S n1) (lt_O_Sn n1)));Fold (Rgt e R0) in H;
+ Apply (pos_Rsqr1 e (imp_not_Req e R0 
+  (or_intror (Rlt e R0) (Rgt e R0) H))).
+Rewrite (S_INR n0);Ring.
+Unfold Rle in H0;Elim H0;Intro. 
+Unfold Rle;Left;Apply Rlt_monotony.
+Rewrite Rplus_sym;
+ Apply (Rlt_r_plus_R1 e (Rlt_le R0 e H)).
+Assumption.
+Rewrite H1;Unfold Rle;Right;Trivial.
+Save.
+
+Lemma Power_monotonic:
+ (x:R) (m,n:nat) (Rgt (Rabsolu x) R1) 
+        -> (le m n)
+           -> (Rle (Rabsolu (pow x m)) (Rabsolu (pow x n))).
+Intros x m n H;Induction n;Intros;Inversion H0.
+Unfold Rle; Right; Reflexivity.
+Unfold Rle; Right; Reflexivity.
+Apply (Rle_trans (Rabsolu (pow x m))
+                 (Rabsolu (pow x n))
+                 (Rabsolu (pow x (S n)))).
+Apply Hrecn; Assumption.
+Simpl;Rewrite Rabsolu_mult.
+Pattern 1 (Rabsolu (pow x n)).
+Rewrite <-Rmult_1r.
+Rewrite (Rmult_sym (Rabsolu x) (Rabsolu (pow x n))).
+Apply Rle_monotony.
+Apply Rabsolu_pos.
+Unfold Rgt in H.
+Apply Rlt_le; Assumption.
+Save.
+
+Lemma Power_Rabsolu: (x:R) (n:nat)
+     (pow (Rabsolu x) n)==(Rabsolu (pow x n)).
+Intro;Induction n;Simpl.
+Apply sym_eqT;Apply Rabsolu_pos_eq;Apply Rlt_le;Apply Rlt_R0_R1.
+Intros; Rewrite H;Apply sym_eqT;Apply Rabsolu_mult.
+Save.
+
+
+Lemma Pow_x_infinity:
+  (x:R) (Rgt (Rabsolu x) R1)
+        -> (b:R) (Ex [N:nat] ((n:nat) (ge n N) 
+                     -> (Rge (Rabsolu (pow x n)) b ))).
+Intros;Elim (archimed (Rmult b (Rinv (Rminus (Rabsolu x) R1))));Intros;
+  Clear H1;
+  Cut (Ex[N:nat] (Rge (INR N) (Rmult b (Rinv (Rminus (Rabsolu x) R1))))).
+Intro; Elim H1;Clear H1;Intros;Exists x0;Intros;
+ Apply (Rge_trans (Rabsolu (pow x n)) (Rabsolu (pow x x0)) b).
+Apply Rle_sym1;Apply Power_monotonic;Assumption.
+Rewrite <- Power_Rabsolu;Cut (Rabsolu x)==(Rplus R1 (Rminus (Rabsolu x) R1)).
+Intro; Rewrite H3;
+ Apply (Rge_trans (pow (Rplus R1 (Rminus (Rabsolu x) R1)) x0)
+                 (Rplus R1 (Rmult (INR x0)  
+                                  (Rminus (Rabsolu x) R1)))
+                 b).
+Apply Rle_sym1;Apply poly;Fold (Rgt (Rminus (Rabsolu x) R1) R0);
+ Apply Rgt_minus;Assumption.
+Apply (Rge_trans 
+         (Rplus R1 (Rmult (INR x0) (Rminus (Rabsolu x) R1)))
+         (Rmult (INR x0) (Rminus (Rabsolu x) R1))
+         b).
+Apply Rle_sym1; Apply Rlt_le;Rewrite (Rplus_sym R1 
+                   (Rmult (INR x0) (Rminus (Rabsolu x) R1)));
+ Pattern 1 (Rmult (INR x0) (Rminus (Rabsolu x) R1));
+ Rewrite <- (let (H1,H2) = (Rplus_ne 
+            (Rmult (INR x0) (Rminus (Rabsolu x) R1))) in
+         H1);
+ Apply Rlt_compatibility;
+ Apply Rlt_R0_R1.
+Cut b==(Rmult (Rmult b (Rinv (Rminus (Rabsolu x) R1)))
+              (Rminus (Rabsolu x) R1)).
+Intros; Rewrite H4;Apply Rge_monotony.
+Apply Rge_minus;Unfold Rge; Left; Assumption.
+Assumption.
+Rewrite Rmult_assoc;Rewrite Rinv_l.
+Ring.
+Apply imp_not_Req; Right;Apply Rgt_minus;Assumption.
+Ring.
+Cut `0<= (up (Rmult b (Rinv (Rminus (Rabsolu x) R1))))`\/
+     `(up (Rmult b (Rinv (Rminus (Rabsolu x) R1)))) <=  0`.
+Intros;Elim H1;Intro.
+Elim (IZN (up (Rmult b (Rinv (Rminus (Rabsolu x) R1)))) H2);Intros;Exists x0;
+ Apply (Rge_trans 
+   (INR x0)
+   (IZR (up (Rmult b (Rinv (Rminus (Rabsolu x) R1)))))
+   (Rmult b (Rinv (Rminus (Rabsolu x) R1)))).
+Rewrite INR_IZR_INZ;Apply IZR_ge;Omega.
+Unfold Rge; Left; Assumption.
+Exists O;Apply (Rge_trans (INR (0))
+          (IZR (up (Rmult b (Rinv (Rminus (Rabsolu x) R1)))))
+          (Rmult b (Rinv (Rminus (Rabsolu x) R1)))).
+Rewrite INR_IZR_INZ;Apply IZR_ge;Simpl;Omega.
+Unfold Rge; Left; Assumption.
+Omega.
+Save.
+
+Lemma pow_ne_zero:
+  (n:nat) ~(n=(0))-> (pow R0 n) == R0.
+Induction n.
+Simpl;Auto.
+Intros;Elim H;Reflexivity.
+Intros; Simpl;Apply Rmult_Ol.
+Save.
+
+Lemma pow_nonzero:
+  (x:R) (n:nat) ~(x==R0) -> ~((pow x n)==R0).
+Intro; Induction n; Simpl.
+Intro; Red;Intro;Apply R1_neq_R0;Assumption.
+Intros;Red; Intro;Elim (without_div_Od x (pow x n0) H1).
+Intro; Auto.
+Apply H;Assumption.
+Save.
+
+Lemma Rinv_pow:
+  (x:R) (n:nat) ~(x==R0) -> (Rinv (pow x n))==(pow (Rinv x) n).
+Intros; Elim n; Simpl.
+Apply Rinv_R1.
+Intro m;Intro;Rewrite Rinv_Rmult.
+Rewrite H0; Reflexivity;Assumption.
+Assumption.
+Apply pow_nonzero;Assumption.
+Save.
+
+Lemma pow_lt_1_zero:
+  (x:R) (Rlt (Rabsolu x) R1)
+        -> (e:R) (Rlt R0 e) 
+                 -> (Ex[N:nat] (n:nat) (ge n N)
+                         -> (Rlt (Rabsolu (pow x n)) e)).
+Intros;Elim (Req_EM x R0);Intro. 
+Exists (1);Rewrite H1;Intros n GE;Rewrite pow_ne_zero.
+Rewrite Rabsolu_R0;Assumption.
+Inversion GE;Auto.
+Cut (Rgt (Rabsolu (Rinv x)) R1).
+Intros;Elim (Pow_x_infinity (Rinv x) H2 (Rplus (Rinv e) R1));Intros N.
+Exists N;Intros;Rewrite <- (Rinv_Rinv e).
+Rewrite <- (Rinv_Rinv (Rabsolu (pow x n))).
+Apply Rinv_lt.
+Apply Rmult_lt_pos.
+Apply Rlt_Rinv.
+Assumption.
+Apply Rlt_Rinv.
+Apply Rabsolu_pos_lt.
+Apply pow_nonzero.
+Assumption.
+Rewrite <- Rabsolu_Rinv.
+Rewrite Rinv_pow.
+Apply (Rlt_le_trans (Rinv e)
+                    (Rplus (Rinv e) R1)
+                    (Rabsolu (pow (Rinv x) n))).
+Pattern 1 (Rinv e).
+Rewrite <- (let (H1,H2) = 
+                (Rplus_ne (Rinv e)) in H1).
+Apply Rlt_compatibility.
+Apply Rlt_R0_R1.
+Apply Rle_sym2.
+Apply H3.
+Assumption.
+Assumption.
+Apply pow_nonzero.
+Assumption.
+Apply Rabsolu_no_R0.
+Apply pow_nonzero.
+Assumption.
+Apply imp_not_Req.
+Right; Unfold Rgt; Assumption.
+Rewrite <- (Rinv_Rinv R1).
+Rewrite Rabsolu_Rinv.
+Unfold Rgt; Apply Rinv_lt.
+Apply Rmult_lt_pos.
+Apply Rabsolu_pos_lt.
+Assumption.
+Rewrite Rinv_R1; Apply Rlt_R0_R1.
+Rewrite Rinv_R1; Assumption.
+Assumption.
+Red;Intro; Apply R1_neq_R0;Assumption.
+Save.
+
 (*******************************)
 (*  Sum of n first naturals    *)
 (*******************************)
@@ -128,6 +322,35 @@ Fixpoint sum_f_R0 [f:nat->R;N:nat]:R:=
 Definition sum_f [s,n:nat;f:nat->R]:R:=      
   (sum_f_R0 [x:nat](f (plus x s)) (minus n s)).
 
+Lemma GP_finite:
+  (x:R) (n:nat) (Rmult (sum_f_R0 [n:nat] (pow x n) n)
+                       (Rminus x R1)) ==
+                (Rminus (pow x (plus n (1))) R1).
+Intros; Induction n; Simpl.
+Ring.
+Rewrite Rmult_Rplus_distrl;Rewrite Hrecn;Cut (plus n (1))=(S n).
+Intro H;Rewrite H;Simpl;Ring.
+Omega.
+Save.
+
+Lemma sum_f_R0_triangle:
+  (x:nat->R)(n:nat) (Rle (Rabsolu (sum_f_R0 x n))
+                         (sum_f_R0 [i:nat] (Rabsolu (x i)) n)).
+Intro; Induction n; Simpl.
+Unfold Rle; Right; Reflexivity.
+Intro m; Intro;Apply (Rle_trans
+          (Rabsolu (Rplus (sum_f_R0 x m) (x (S m))))
+          (Rplus (Rabsolu (sum_f_R0 x m))
+                 (Rabsolu (x (S m))))
+          (Rplus (sum_f_R0 [i:nat](Rabsolu (x i)) m) 
+                 (Rabsolu (x (S m))))).
+Apply Rabsolu_triang.
+Rewrite Rplus_sym;Rewrite (Rplus_sym 
+  (sum_f_R0 [i:nat](Rabsolu (x i)) m) (Rabsolu (x (S m))));
+  Apply Rle_compatibility;Assumption.
+Save.
+
+
 (*******************************)
 (*        Infinit Sum          *)
 (*******************************)
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 591bc22e42..471eb9f1ce 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -203,6 +203,10 @@ Apply (Rminus_eq x y H).
 Apply (eq_Rminus x y H). 
 Save.
 
+Lemma R_dist_eq:(x:R)(R_dist x x)==R0.
+Unfold R_dist;Intros;SplitAbsolu;Intros;Ring.
+Save.
+
 (***********)
 Lemma R_dist_tri:(x,y,z:R)(Rle (R_dist x y) 
                    (Rplus (R_dist x z) (R_dist z y))).
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
new file mode 100644
index 0000000000..2e94528d50
--- /dev/null
+++ b/theories/Reals/Rseries.v
@@ -0,0 +1,279 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Rderiv.
+Require Classical.
+Require Compare.
+
+(* classical is needed for Un_cv_crit *)
+(*********************************************************)
+(*           Definition of sequence and properties       *)
+(*                                                       *)
+(*********************************************************)
+
+Section sequence.
+
+(*********)
+Variable Un:nat->R.
+
+(*********)
+Fixpoint Rmax_N [N:nat]:R:=
+   Cases N of
+     O     => (Un O)
+    |(S n) => (Rmax (Un (S n)) (Rmax_N n))
+   end.
+
+(*********)
+Definition EUn:R->Prop:=[r:R](Ex [i:nat] (r==(Un i))).
+
+(*********)
+Definition Un_cv:R->Prop:=[l:R]
+  (eps:R)(Rgt eps R0)->(Ex[N:nat](n:nat)(ge n N)->
+             (Rlt (R_dist (Un n) l) eps)).
+
+(*********)
+Definition Cauchy_crit:Prop:=(eps:R)(Rgt eps R0)->
+       (Ex[N:nat] (n,m:nat)(ge n N)->(ge m N)->
+                  (Rlt (R_dist (Un n) (Un m)) eps)).
+
+(*********)
+Definition Un_growing:Prop:=(n:nat)(Rle (Un n) (Un (S n))).
+
+(*********)
+Lemma EUn_noempty:(ExT [r:R] (EUn r)).
+Unfold EUn;Split with (Un O);Split with O;Trivial.
+Save.
+
+(*********)
+Lemma Un_in_EUn:(n:nat)(EUn (Un n)).
+Intro;Unfold EUn;Split with n;Trivial.
+Save.
+
+(*********)
+Lemma Un_bound_imp:(x:R)((n:nat)(Rle (Un n) x))->(is_upper_bound EUn x).
+Intros;Unfold is_upper_bound;Intros;Unfold EUn in H0;Elim H0;Clear H0;
+ Intros;Generalize (H x1);Intro;Rewrite <- H0 in H1;Trivial.
+Save.
+
+(*********)
+Lemma growing_prop:(n,m:nat)Un_growing->(ge n m)->(Rge (Un n) (Un m)).
+Double Induction 1 2;Intros.
+Unfold Rge;Right;Trivial.
+ElimType False;Unfold ge in H1;Generalize (le_Sn_O n0);Intro;Auto.
+Cut (ge n0 (0)).
+Generalize H0;Intros;Unfold Un_growing in H0;
+ Apply (Rge_trans (Un (S n0)) (Un n0) (Un (0)) 
+                  (Rle_sym1 (Un n0) (Un (S n0)) (H0 n0)) (H O H2 H3)).
+Elim n0;Auto.
+Elim (lt_eq_lt_dec n1 n0);Intro y.
+Elim y;Clear y;Intro y.
+Unfold ge in H2;Generalize (le_not_lt n0 n1 (le_S_n n0 n1 H2));Intro;
+ ElimType False;Auto.
+Rewrite y;Unfold Rge;Right;Trivial.
+Unfold ge in H0;Generalize (H0 (S n0) H1 (lt_le_S n0 n1 y));Intro;
+ Unfold Un_growing in H1;
+ Apply (Rge_trans (Un (S n1)) (Un n1) (Un (S n0)) 
+                  (Rle_sym1 (Un n1) (Un (S n1)) (H1 n1)) H3).
+Save.
+
+
+(* classical is needed: not_all_not_ex *)
+(*********)
+Lemma Un_cv_crit:Un_growing->(bound EUn)->(ExT [l:R] (Un_cv l)).
+Unfold Un_growing Un_cv;Intros;
+ Generalize (complet EUn H0 EUn_noempty);Intro;
+ Elim H1;Clear H1;Intros;Split with x;Intros;
+ Unfold is_lub in H1;Unfold bound in H0;Unfold is_upper_bound in H0 H1;
+ Elim H0;Clear H0;Intros;Elim H1;Clear H1;Intros;
+ Generalize (H3 x0 H0);Intro;Cut (n:nat)(Rle (Un n) x);Intro.
+Cut (Ex [N:nat] (Rlt (Rminus x eps) (Un N))).
+Intro;Elim H6;Clear H6;Intros;Split with x1.
+Intros;Unfold R_dist;Apply (Rabsolu_def1 (Rminus (Un n) x) eps).
+Unfold Rgt in H2;
+ Apply (Rle_lt_trans (Rminus (Un n) x) R0 eps 
+                     (Rle_minus (Un n) x (H5 n)) H2).
+Fold Un_growing in H;Generalize (growing_prop n x1 H H7);Intro;
+ Generalize (Rlt_le_trans (Rminus x eps) (Un x1) (Un n) H6
+                          (Rle_sym2 (Un x1) (Un n) H8));Intro;
+ Generalize (Rlt_compatibility (Ropp x) (Rminus x eps) (Un n) H9);
+ Unfold Rminus;Rewrite <-(Rplus_assoc (Ropp x) x (Ropp eps));
+ Rewrite (Rplus_sym (Ropp x) (Un n));Fold (Rminus (Un n) x);
+ Rewrite Rplus_Ropp_l;Rewrite (let (H1,H2)=(Rplus_ne (Ropp eps)) in H2);
+ Trivial.
+Cut ~((N:nat)(Rge (Rminus x eps) (Un N))).
+Intro;Apply (not_all_not_ex nat ([N:nat](Rlt (Rminus x eps) (Un N))));
+ Red;Intro;Red in H6;Elim H6;Clear H6;Intro;
+ Apply (Rlt_not_ge (Rminus x eps) (Un N) (H7 N)).
+Red;Intro;Cut (N:nat)(Rle (Un N) (Rminus x eps)).
+Intro;Generalize (Un_bound_imp (Rminus x eps) H7);Intro;
+ Unfold is_upper_bound in H8;Generalize (H3 (Rminus x eps) H8);Intro;
+ Generalize (Rle_minus x (Rminus x eps) H9);Unfold Rminus;
+ Rewrite Ropp_distr1;Rewrite <- Rplus_assoc;Rewrite Rplus_Ropp_r;
+ Rewrite (let (H1,H2)=(Rplus_ne (Ropp (Ropp eps))) in H2);
+ Rewrite Ropp_Ropp;Intro;Unfold Rgt in H2;
+ Generalize (Rle_not eps R0 H2);Intro;Auto.
+Intro;Elim (H6 N);Intro;Unfold Rle.
+Left;Unfold Rgt in H7;Assumption.
+Right;Auto.
+Apply (H1 (Un n) (Un_in_EUn n)).
+Save.
+
+(*********)
+Lemma finite_greater:(N:nat)(ExT [M:R] (n:nat)(le n N)->(Rle (Un n) M)).
+Intro;Induction N.
+Split with (Un O);Intros;Rewrite (le_n_O_eq n H); 
+ Apply (eq_Rle (Un (n)) (Un (n)) (refl_eqT R (Un (n)))).
+Elim HrecN;Clear HrecN;Intros;Split with (Rmax (Un (S N)) x);Intros;
+ Elim (Rmax_Rle (Un (S N)) x (Un n));Intros;Clear H1;Inversion H0.
+Rewrite <-H1;Rewrite <-H1 in H2;
+ Apply (H2 (or_introl (Rle (Un n) (Un n)) (Rle (Un n) x) 
+    (eq_Rle (Un n) (Un n) (refl_eqT R (Un n))))).
+Apply (H2 (or_intror (Rle (Un n) (Un (S N))) (Rle (Un n) x) 
+    (H n H3))).
+Save.
+
+(*********)
+Lemma cauchy_bound:Cauchy_crit->(bound EUn).
+Unfold Cauchy_crit bound;Intros;Unfold is_upper_bound;
+ Unfold Rgt in H;Elim (H R1 Rlt_R0_R1);Clear H;Intros;
+ Generalize (H x);Intro;Generalize (le_dec x);Intro;
+ Elim (finite_greater x);Intros;Split with (Rmax x0 (Rplus (Un x) R1));
+ Clear H;Intros;Unfold EUn in H;Elim H;Clear H;Intros;Elim (H1 x2);
+ Clear H1;Intro y.
+Unfold ge in H0;Generalize (H0 x2 (le_n x) y);Clear H0;Intro;
+ Rewrite <- H in H0;Unfold R_dist in H0;
+ Elim (Rabsolu_def2 (Rminus (Un x) x1) R1 H0);Clear H0;Intros;
+ Elim (Rmax_Rle x0 (Rplus (Un x) R1) x1);Intros;Apply H4;Clear H3 H4;
+ Right;Clear H H0 y;Apply (Rlt_le x1 (Rplus (Un x) R1));
+ Generalize (Rlt_minus (Ropp R1) (Rminus (Un x) x1) H1);Clear H1;
+ Intro;Apply (Rminus_lt x1 (Rplus (Un x) R1));
+ Cut (Rminus (Ropp R1) (Rminus (Un x) x1))==
+  (Rminus x1 (Rplus (Un x) R1));[Intro;Rewrite H0 in H;Assumption|Ring].
+Generalize (H2 x2 y);Clear H2 H0;Intro;Rewrite<-H in H0;
+ Elim (Rmax_Rle x0 (Rplus (Un x) R1) x1);Intros;Clear H1;Apply H2;
+ Left;Assumption.
+Save.
+
+End sequence.
+
+(*****************************************************************)
+(*           Definition of Power Series and properties           *)
+(*                                                               *)
+(*****************************************************************)
+
+Section Isequence.
+
+(*********)
+Variable An:nat->R.
+
+(*********)
+Definition Pser:R->R->Prop:=[x,l:R]
+   (infinit_sum [n:nat](Rmult (An n) (pow x n)) l).
+
+End Isequence.
+
+Lemma GP_infinite:
+ (x:R) (Rlt (Rabsolu x) R1) 
+       -> (Pser ([n:nat] R1) x (Rinv(Rminus R1 x))).
+Intros;Unfold Pser; Unfold infinit_sum;Intros;Elim (Req_EM x R0).
+Intros;Exists O; Intros;Rewrite H1;Rewrite minus_R0;Rewrite Rinv_R1;
+  Cut (sum_f_R0 [n0:nat](Rmult R1 (pow R0 n0)) n)==R1.
+Intros; Rewrite H3;Rewrite R_dist_eq;Auto.
+Elim n; Simpl.
+Ring.
+Intros;Rewrite H3;Ring.
+Intro;Cut (Rlt R0
+      (Rmult eps (Rmult (Rabsolu (Rminus R1 x)) 
+                        (Rabsolu (Rinv x))))).
+Intro;Elim (pow_lt_1_zero x H
+                    (Rmult eps (Rmult (Rabsolu (Rminus R1 x))
+                                 (Rabsolu (Rinv x))))
+                    H2);Intro N; Intros;Exists N; Intros;
+  Cut (sum_f_R0 [n0:nat](Rmult R1 (pow x n0)) n)==
+    (sum_f_R0 [n0:nat](pow x n0) n).
+Intros; Rewrite H5;Apply (Rlt_monotony_rev
+         (Rabsolu (Rminus R1 x))
+         (R_dist (sum_f_R0 [n0:nat](pow x n0) n) 
+                 (Rinv (Rminus R1 x))) 
+         eps).
+Apply Rabsolu_pos_lt.
+Apply Rminus_eq_contra.
+Apply imp_not_Req.
+Right; Unfold Rgt.
+Apply (Rle_lt_trans x (Rabsolu x) R1).
+Apply Rle_Rabsolu.
+Assumption.
+Unfold R_dist; Rewrite <- Rabsolu_mult.
+Rewrite Rminus_distr.
+Cut (Rmult (Rminus R1 x) (sum_f_R0 [n0:nat](pow x n0) n))==
+    (Ropp (Rmult(sum_f_R0 [n0:nat](pow x n0) n) 
+          (Rminus x R1))).
+Intro; Rewrite H6.
+Rewrite GP_finite.
+Rewrite Rinv_r.
+Cut (Rminus (Ropp (Rminus (pow x (plus n (1))) R1)) R1)==
+    (Ropp (pow x (plus n (1)))).
+Intro; Rewrite H7.
+Rewrite Rabsolu_Ropp;Cut (plus n (S O))=(S n);Auto.
+Intro H8;Rewrite H8;Simpl;Rewrite Rabsolu_mult;
+  Apply (Rlt_le_trans (Rmult (Rabsolu x) (Rabsolu (pow x n)))
+                    (Rmult (Rabsolu x)
+                           (Rmult eps
+                              (Rmult (Rabsolu (Rminus R1 x)) 
+                                      (Rabsolu (Rinv x)))))
+                 (Rmult (Rabsolu (Rminus R1 x)) eps)).
+Apply Rlt_monotony.
+Apply Rabsolu_pos_lt.
+Assumption.
+Auto.
+Cut (Rmult (Rabsolu x)
+           (Rmult eps (Rmult (Rabsolu (Rminus R1 x)) 
+                             (Rabsolu (Rinv x)))))==
+    (Rmult (Rmult (Rabsolu x) (Rabsolu (Rinv x))) 
+           (Rmult eps (Rabsolu (Rminus R1 x)))).
+Clear H8;Intros; Rewrite H8;Rewrite <- Rabsolu_mult;Rewrite Rinv_r.  
+Rewrite Rabsolu_R1;Cut (Rmult R1 (Rmult eps (Rabsolu (Rminus R1 x))))==
+    (Rmult (Rabsolu (Rminus R1 x)) eps).
+Intros; Rewrite H9;Unfold Rle; Right; Reflexivity.
+Ring.
+Assumption.
+Ring.
+Ring.
+Ring.
+Apply Rminus_eq_contra.
+Apply imp_not_Req.
+Right; Unfold Rgt.
+Apply (Rle_lt_trans x (Rabsolu x) R1).
+Apply Rle_Rabsolu.
+Assumption.
+Ring; Ring.
+Elim n; Simpl.
+Ring.
+Intros; Rewrite H5.
+Ring.
+Apply Rmult_lt_pos.
+Auto.
+Apply Rmult_lt_pos.
+Apply Rabsolu_pos_lt.
+Apply Rminus_eq_contra.
+Apply imp_not_Req.
+Right; Unfold Rgt.
+Apply (Rle_lt_trans x (Rabsolu x) R1).
+Apply Rle_Rabsolu.
+Assumption.
+Apply Rabsolu_pos_lt.
+Apply Rinv_neq_R0.
+Assumption.
+Save.
+
+
+
+
+
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index b8eef3a253..4afaa83ac2 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -72,7 +72,7 @@ Grammar command atomic_pattern :=
   r_in_pattern [ "``" rnatural:rnumber($c) "``" ] -> [$c].   
 
 (*i* pp **)
-(* pb: on rajoute des () lorsque les constantes terminent par 1 lors de
+(* pb: on rajoute des () lorsque les constantes commencent par 1 lors de
 l'appel avec NRplus i*)
 
 
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
new file mode 100644
index 0000000000..1d59a71e39
--- /dev/null
+++ b/theories/Reals/Rtrigo_fun.v
@@ -0,0 +1,114 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Rseries.
+
+(*****************************************************************)
+(*           To define transcendental functions                  *)
+(*                                                               *)
+(*****************************************************************)
+(*****************************************************************)
+(*           For exponential function                            *)
+(*                                                               *)
+(*****************************************************************)
+
+(*********)
+Lemma Alembert_exp:(Un_cv
+   [n:nat](Rabsolu (Rmult (Rinv (INR (fact (S n)))) 
+         (Rinv (Rinv (INR (fact n)))))) R0).
+Unfold Un_cv;Intros;Elim (total_order_Rgt eps R1);Intro.
+Split with O;Intros;Rewrite (simpl_fact n);Unfold R_dist;
+ Rewrite (minus_R0 (Rabsolu (Rinv (INR (S n)))));
+ Rewrite (Rabsolu_Rabsolu (Rinv (INR (S n))));
+ Cut (Rgt (Rinv (INR (S n))) R0).
+Intro; Rewrite (Rabsolu_pos_eq (Rinv (INR (S n)))).
+Cut (Rlt (Rminus (Rinv eps) R1) R0).
+Intro;Generalize (Rlt_le_trans (Rminus (Rinv eps) R1) R0 (INR n) H2 
+   (INR_le n));Clear H2;Intro;
+ Unfold Rminus in H2;Generalize (Rlt_compatibility R1 
+       (Rplus (Rinv eps) (Ropp R1)) (INR n) H2);
+ Replace (Rplus R1 (Rplus (Rinv eps) (Ropp R1))) with (Rinv eps);
+ [Clear H2;Intro|Ring].
+Rewrite (Rplus_sym R1 (INR n)) in H2;Rewrite <-(S_INR n) in H2;
+ Generalize (Rmult_gt (Rinv (INR (S n))) eps H1 H);Intro;
+ Unfold Rgt in H3;
+ Generalize (Rlt_monotony (Rmult (Rinv (INR (S n))) eps) (Rinv eps)
+     (INR (S n)) H3 H2);Intro;
+ Rewrite (Rmult_assoc (Rinv (INR (S n))) eps (Rinv eps)) in H4;
+ Rewrite (Rinv_r eps (imp_not_Req eps R0 
+      (or_intror (Rlt eps R0) (Rgt eps R0) H))) 
+  in H4;Rewrite (let (H1,H2)=(Rmult_ne (Rinv (INR (S n)))) in H1) 
+  in H4;Rewrite (Rmult_sym (Rinv (INR (S n)))) in H4;
+ Rewrite (Rmult_assoc eps (Rinv (INR (S n))) (INR (S n))) in H4;
+ Rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) 
+      (sym_not_equal nat O (S n) (O_S n)))) in H4;
+ Rewrite (let (H1,H2)=(Rmult_ne eps) in H1) in H4;Assumption.
+Apply Rlt_minus;Unfold Rgt in a;Rewrite <- Rinv_R1;
+ Apply (Rinv_lt R1 eps);Auto;
+ Rewrite (let (H1,H2)=(Rmult_ne eps) in H2);Unfold Rgt in H;Assumption.
+Unfold Rgt in H1;Apply Rlt_le;Assumption.
+Unfold Rgt;Apply Rlt_Rinv; Apply INR_lt_0;Apply lt_O_Sn.
+(**)
+Cut `0<=(up (Rminus (Rinv eps) R1))`.
+Intro;Elim (IZN (up (Rminus (Rinv eps) R1)) H0);Intros;
+ Split with x;Intros;Rewrite (simpl_fact n);Unfold R_dist;
+ Rewrite (minus_R0 (Rabsolu (Rinv (INR (S n)))));
+ Rewrite (Rabsolu_Rabsolu (Rinv (INR (S n))));
+ Cut (Rgt (Rinv (INR (S n))) R0).
+Intro; Rewrite (Rabsolu_pos_eq (Rinv (INR (S n)))).
+Cut (Rlt (Rminus (Rinv eps) R1) (INR x)).
+Intro;Generalize (Rlt_le_trans (Rminus (Rinv eps) R1) (INR x) (INR n) 
+      H4 (INR_le_nm x n ([n,m:nat; H:(ge m n)]H x n H2)));  
+ Clear H4;Intro;Unfold Rminus in H4;Generalize (Rlt_compatibility R1 
+       (Rplus (Rinv eps) (Ropp R1)) (INR n) H4);
+ Replace (Rplus R1 (Rplus (Rinv eps) (Ropp R1))) with (Rinv eps);
+ [Clear H4;Intro|Ring].
+Rewrite (Rplus_sym R1 (INR n)) in H4;Rewrite <-(S_INR n) in H4;
+ Generalize (Rmult_gt (Rinv (INR (S n))) eps H3 H);Intro;
+ Unfold Rgt in H5;
+ Generalize (Rlt_monotony (Rmult (Rinv (INR (S n))) eps) (Rinv eps)
+     (INR (S n)) H5 H4);Intro;
+ Rewrite (Rmult_assoc (Rinv (INR (S n))) eps (Rinv eps)) in H6;
+ Rewrite (Rinv_r eps (imp_not_Req eps R0 
+      (or_intror (Rlt eps R0) (Rgt eps R0) H))) 
+  in H6;Rewrite (let (H1,H2)=(Rmult_ne (Rinv (INR (S n)))) in H1) 
+  in H6;Rewrite (Rmult_sym (Rinv (INR (S n)))) in H6;
+ Rewrite (Rmult_assoc eps (Rinv (INR (S n))) (INR (S n))) in H6;
+ Rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) 
+      (sym_not_equal nat O (S n) (O_S n)))) in H6;
+ Rewrite (let (H1,H2)=(Rmult_ne eps) in H1) in H6;Assumption.
+Cut (IZR (up (Rminus (Rinv eps) R1)))==(IZR (INZ x));
+ [Intro|Rewrite H1;Trivial].
+Elim (archimed (Rminus (Rinv eps) R1));Intros;Clear H6;
+ Unfold Rgt in H5;Rewrite H4 in H5;Rewrite INR_IZR_INZ;Assumption.
+Unfold Rgt in H1;Apply Rlt_le;Assumption.
+Unfold Rgt;Apply Rlt_Rinv; Apply INR_lt_0;Apply lt_O_Sn.
+Apply (le_O_IZR (up (Rminus (Rinv eps) R1))); 
+ Apply (Rle_trans R0 (Rminus (Rinv eps) R1) 
+  (IZR (up (Rminus (Rinv eps) R1)))).
+Generalize (Rgt_not_le eps R1 b);Clear b;Unfold Rle;Intro;Elim H0;
+ Clear H0;Intro.
+Left;Unfold Rgt in H;
+ Generalize (Rlt_monotony (Rinv eps) eps R1 (Rlt_Rinv eps H) H0);
+ Rewrite (Rinv_l eps (sym_not_eqT R R0 eps
+    (imp_not_Req R0 eps (or_introl (Rlt R0 eps) (Rgt R0 eps) H))));
+ Rewrite (let (H1,H2)=(Rmult_ne (Rinv eps)) in H1);Intro;
+ Fold (Rgt (Rminus (Rinv eps) R1) R0);Apply Rgt_minus;Unfold Rgt;
+ Assumption.
+Right;Rewrite H0;Rewrite Rinv_R1;Apply sym_eqT;Apply eq_Rminus;Auto.
+Elim (archimed (Rminus (Rinv eps) R1));Intros;Clear H1;
+ Unfold Rgt in H0;Apply Rlt_le;Assumption.
+Save.
+
+
+
+
+
+