mise-a-jour, ajouts de quelques truc...

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

3 files changed, 274 insertions, 50 deletions

diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index bfbab59bd..b459a3d85 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -224,6 +224,13 @@ Intro;Generalize (H0 r1==R0 r2==R0 (Rmult r1 r2)==R0
 Tauto.
 Save.
 
+(**********) 
+Lemma Rmult_Rplus_distrl:
+   (r1,r2,r3:R) ((Rmult (Rplus r1 r2) r3)==
+                (Rplus (Rmult r1 r3) (Rmult r2 r3))).
+Intros; Ring.
+Save.
+
 (***********)
 Definition Rsqr:R->R:=[r:R](Rmult r r).
 
@@ -282,6 +289,13 @@ Tauto.
 Save.
 
 (**********)
+Lemma Rminus_distr:
+  (x,y,z:R) (Rmult x (Rminus y z))==
+            (Rminus (Rmult x y) (Rmult x z)).
+Intros; Ring.
+Save.
+
+(**********)
 Lemma eq_Ropp:(r1,r2:R)(r1==r2)->((Ropp r1)==(Ropp r2)).
   Auto with real.
 Save.
@@ -316,6 +330,28 @@ Intros;Red;Intro;Generalize (Rplus_plus_r r (Ropp r) R0 H0);Intro;
 Save.
 
 (*********)
+Lemma Rinv_R1:(Rinv R1)==R1.
+Apply (r_Rmult_mult R1 (Rinv R1) R1);
+ [Rewrite (Rinv_r R1 R1_neq_R0);
+  Rewrite (let (H1,H2)=(Rmult_ne R1) in H1);Trivial|
+  Red;Intro;Apply R1_neq_R0;Assumption].
+Save.
+
+(*********)
+Lemma Rinv_neq_R0:(r:R)(~r==R0)->~(Rinv r)==R0.
+Intros;Red;Intro;Generalize (Rmult_mult_r r (Rinv r) R0 H0);
+ Clear H0;Intro;Rewrite (Rinv_r r H) in H0;Rewrite (Rmult_Or r) in H0;
+ Generalize R1_neq_R0;Intro;Auto. 
+Save.
+
+(*********)
+Lemma Rinv_Rinv:(r:R)(~r==R0)->(Rinv (Rinv r))==r.
+Intros;Apply (r_Rmult_mult (Rinv r) (Rinv (Rinv r)) r);
+ [Rewrite (Rinv_r (Rinv r) (Rinv_neq_R0 r H));
+  Rewrite (Rinv_l r H);Trivial |Apply Rinv_neq_R0;Assumption].
+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.
@@ -375,6 +411,13 @@ Elim (imp_not_Req r2 r1);Auto with zarith real.
 Save.
 
 (**********)
+Lemma Rlt_ge_not:(r1,r2:R)(Rlt r1 r2)->~(Rge r1 r2).
+Intros;Red;Intro;Unfold Rge in H0;Unfold Rgt in H0;Elim H0;Intro.
+Apply (Rlt_antisym r1 r2 H H1).
+Rewrite H1 in H;Exact (Rlt_antisym r2 r2 H H).
+Save.
+
+(**********)
 Lemma Rle_le_eq:(r1,r2:R)(Rle r1 r2)/\(Rle r2 r1)<->(r1==r2).
 Intros; Split; Intro.
 Elim H; Unfold Rle; Intros.
@@ -493,6 +536,18 @@ Apply (Rlt_anti_compatibility r R0 (Ropp r));
 Save.
 
 (**********)
+Lemma Rle_monotony: 
+  (r,r1,r2:R)
+        (Rle R0 r)
+        ->(Rle r1 r2)->(Rle (Rmult r r1) (Rmult r r2)).
+Intros r r1 r2;Unfold Rle;Intros;Elim H;Elim H0;Intros.
+Left;Apply Rlt_monotony;Assumption.
+Right;Rewrite H1;Reflexivity.
+Right;Rewrite <- H2;Rewrite Rmult_Ol;Rewrite Rmult_Ol;Reflexivity.
+Right;Rewrite H1;Reflexivity.
+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.
@@ -646,6 +701,37 @@ Rewrite (Rmult_Or r);Intro;Generalize R1_neq_R0;Auto.
 Apply (imp_not_Req r R0);Left;Assumption.
 Save.
 
+(*********)
+Lemma Rinv_lt:(r1,r2:R)(Rlt R0 (Rmult r1 r2))->(Rlt r1 r2)->
+                       (Rlt (Rinv r2) (Rinv r1)).  
+Intros;Generalize (Rlt_monotony (Rinv (Rmult r1 r2)) r1 r2 
+                  (Rlt_Rinv (Rmult r1 r2) H) H0);Intro;
+ Elim (without_div_O_contr r1 r2  
+       (sym_not_eqT R R0 (Rmult r1 r2) (imp_not_Req R0 (Rmult r1 r2) 
+       (or_introl (Rlt R0 (Rmult r1 r2)) (Rgt R0 (Rmult r1 r2)) H))));
+ Intros;Rewrite Rinv_Rmult in H1;Auto;
+ Rewrite (Rmult_assoc (Rinv r1) (Rinv r2) r2) in H1;
+ Rewrite (Rinv_l r2 H3) in H1;
+ Rewrite (let (H1,H2)=(Rmult_ne (Rinv r1)) in H1) in H1;
+ Rewrite (Rmult_sym (Rinv r1) (Rinv r2)) in H1;
+ Rewrite (Rmult_assoc (Rinv r2) (Rinv r1) r1 ) in H1;
+ Rewrite (Rinv_l r1 H2) in H1;
+ Rewrite (let (H1,H2)=(Rmult_ne (Rinv r2)) in H1) in H1;Assumption.
+Save.
+
+(**********)
+Lemma Rlt_monotony_rev:
+  (r,r1,r2:R)(Rlt R0 r)->(Rlt (Rmult r r1) (Rmult r r2))
+             ->(Rlt r1 r2).
+Intros;Cut (s:R) (Rmult (Rinv r) (Rmult r s))==s.
+Intros; Rewrite <- (H1 r1); Rewrite <- (H1 r2);Apply Rlt_monotony. 
+Apply Rlt_Rinv; Assumption.
+Assumption.
+Intro;Rewrite <- Rmult_assoc;Rewrite Rinv_l.
+Ring.
+Apply imp_not_Req; Right; Unfold Rgt; Assumption.
+Save.
+
 (*********************************************************)        
 (*       Greater                                         *)
 (*********************************************************)
@@ -815,6 +901,14 @@ Right; Apply (r_Rplus_plus r r1 r2 H0).
 Save.
 
 (***********)
+Lemma Rge_monotony:
+ (x,y,z:R) (Rge z R0) -> (Rge x y) -> (Rge (Rmult x z) (Rmult y z)).
+Intros;Apply Rle_sym1;
+ Rewrite (Rmult_sym y z); Rewrite (Rmult_sym x z);
+ Apply Rle_monotony;Apply Rle_sym2; Assumption.
+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.
@@ -823,6 +917,16 @@ Unfold Rminus; Rewrite -> (Rplus_sym r1 (Ropp r2));
  Apply (Rgt_plus_plus_r (Ropp r2) r1 r2 H).
 Save.
 
+(*********)
+Lemma minus_Rgt:(r1,r2:R)(Rgt (Rminus r1 r2) R0)->(Rgt r1 r2).
+Intros;Generalize (Rgt_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 Rge_minus:(r1,r2:R)(Rge r1 r2)->(Rge (Rminus r1 r2) R0).
 Unfold Rge; Intros; Elim H; Intro.
@@ -846,6 +950,12 @@ Unfold Rgt;Intros;Generalize (Rlt_monotony r1 R0 r2 H H0);Intro;
  Rewrite (Rmult_Or r1) in H1;Assumption.
 Save.
 
+(*********)
+Lemma Rmult_lt_pos:(x,y:R)(Rlt R0 x)->(Rlt R0 y)->(Rlt R0 (Rmult x y)).
+Generalize Rmult_gt;Unfold Rgt;Auto.
+Save.
+
+
 (***********)
 Lemma Rplus_eq_R0:(a,b:R)(Rle R0 a)->(Rle R0 b)->(Rplus a b)==R0->
                          (a==R0)/\(b==R0).
@@ -919,6 +1029,34 @@ Unfold Rminus; Rewrite -> Rplus_sym; Rewrite -> Rplus_assoc;
 Auto with zarith real.
 Save.
 
+(*********)
+Lemma mult_INR:(n,m:nat)(INR (mult n m))==(Rmult (INR n) (INR m)).
+Induction n.
+Simpl; Intro;Apply sym_eqT;Apply Rmult_Ol.
+Intros;Unfold 1 mult;Cbv Beta Iota;Fold mult;
+ Rewrite (plus_INR m (mult n0 m));Rewrite (H m);
+ Pattern 1 (INR m); 
+ Rewrite <-(let (H1,H2)=(Rmult_ne (INR m)) in H1);
+ Rewrite (Rmult_sym (INR n0) (INR m));
+ Rewrite <-(Rmult_Rplus_distr (INR m) R1 (INR n0));
+ Rewrite (Rplus_sym R1 (INR n0));Rewrite <-(S_INR n0);
+ Apply Rmult_sym. 
+Save. 
+
+
+(*********)
+Lemma INR_lt_0:(n:nat)(lt O n)->(Rlt R0 (INR n)).
+Induction n;Intros.
+Absurd (lt (0) (0));[Apply lt_n_n|Assumption].
+Elim (le_lt_or_eq (0) n0 (lt_n_Sm_le (0) n0 H0));Intro.
+Generalize (H H1);Clear H H1;Intro;Rewrite (S_INR n0);
+ Generalize (Rlt_compatibility R1 R0 (INR n0) H);Intro;
+ Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H1;
+ Rewrite (Rplus_sym (INR n0) R1);
+ Apply (Rlt_trans R0 R1 (Rplus R1 (INR n0)) (Rlt_R0_R1) H1).
+Rewrite <-H1;Simpl;Apply Rlt_R0_R1.
+Save.
+
 (**********)
 Lemma INR_le:(n:nat)(Rle R0 (INR n)).
 Induction n.
@@ -927,6 +1065,18 @@ Intros;Rewrite (S_INR n0);Apply (Rlt_le R0 (Rplus (INR n0) R1));
  Apply (Rlt_r_plus_R1 (INR n0) H).
 Save.
 
+(*********)
+Lemma INR_le_nm:(n,m:nat)(le n m)->(Rle (INR n) (INR m)).
+Intros;Elim (le_lt_or_eq n m H);Intro.
+Cut (lt (0) (minus m n)).
+Intro;Generalize (INR_lt_0 (minus m n) H1);
+ Intro;Rewrite minus_INR in H2;Auto;
+ Apply (Rlt_le (INR n) (INR m));Fold (Rgt (INR m) (INR n));
+ Apply (minus_Rgt (INR m) (INR n));Unfold Rgt;Assumption.
+Omega.
+Rewrite H0;Unfold Rle;Right;Trivial.
+Save.
+
 (**********)
 Lemma not_INR_O:(n:nat)~(INR n)==R0->~n=O.
 Intros;Cut n=(0)->(INR n)==R0.
@@ -952,6 +1102,11 @@ Save.
 Definition INZ:=inject_nat.
 
 (**********)
+Lemma IZN:(z:Z)(`0<=z`)->(Ex [n:nat] z=(INZ n)).
+Unfold INZ;Intros;Apply inject_nat_complete;Assumption.
+Save.
+
+(**********)
 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.
@@ -1077,6 +1232,14 @@ Intros;Generalize (eq_Rminus (IZR z1) (IZR z2) H);
  Intro;Omega.
 Save.
 
+(*********)
+Lemma le_O_IZR:(z:Z)(Rle R0 (IZR z))->(Zle ZERO z).
+Unfold Rle;Intros;Elim H;Clear H;Intro.
+Unfold Zle;Red;Intro;Apply (Zlt_le_weak `0` z (lt_O_IZR z H));
+ Assumption.
+Generalize (eq_IZR_R0 z (sym_eqT R R0 (IZR z) H));Intro;Omega.
+Save.
+
 (**********)
 Lemma le_IZR_R1:(z:Z)(Rle (IZR z) R1)->(Zle z `1`).
 Induction z; Intros.
@@ -1106,6 +1269,12 @@ Intro;Rewrite H1 in H0;Clear H1 H;Apply (eq_IZR (NEG p) `1` H0).
 Save.
 
 (**********)
+Lemma IZR_ge: 
+  (m,n:Z) `m>= n` ->(Rge (IZR m) (IZR n)).
+Intros;Apply Rlt_not_ge;Red;Intro;Generalize (lt_IZR m n H0);Intro; Omega.
+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;
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 63b9a3cfb..b7466eb87 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -20,17 +20,30 @@ Definition Rmin :R->R->R:=[x,y:R]
   end.
 
 (*********)
+Lemma Rmin_Rgt_l:(r1,r2,r:R)(Rgt (Rmin r1 r2) r) ->
+    ((Rgt r1 r)/\(Rgt r2 r)).
+Intros r1 r2 r;Unfold Rmin;Case (total_order_Rle r1 r2);Intros.
+Split.
+Assumption.
+Unfold Rgt;Unfold Rgt in H;Exact (Rlt_le_trans r r1 r2 H r0).
+Split.
+Generalize (not_Rle r1 r2 n);Intro;Exact (Rgt_trans r1 r2 r H0 H).
+Assumption.
+Save.
+
+(*********)
+Lemma Rmin_Rgt_r:(r1,r2,r:R)(((Rgt r1 r)/\(Rgt r2 r)) -> 
+         (Rgt (Rmin r1 r2) r)).
+Intros;Unfold Rmin;Case (total_order_Rle r1 r2);Elim H;Clear H;Intros;
+ Assumption.
+Save.
+
+(*********)
 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.
+Intros; Split.
+Exact (Rmin_Rgt_l r1 r2 r).
+Exact (Rmin_Rgt_r r1 r2 r).
 Save.
 
 (*******************************)
@@ -86,6 +99,22 @@ Apply Ropp_neq;Auto.
 Save.
 
 (*********)
+Lemma Rabsolu_left: (r:R)(Rlt r R0)->((Rabsolu r) == (Ropp r)).
+Intros;Unfold Rabsolu;Case (case_Rabsolu r);Trivial;Intro;Absurd (Rge r R0).
+Exact (Rlt_ge_not r R0 H).
+Assumption.
+Save.
+
+(*********)
+Lemma Rabsolu_right: (r:R)(Rge r R0)->((Rabsolu r) == r).
+Intros;Unfold Rabsolu;Case (case_Rabsolu r);Intro.
+Absurd (Rge r R0).
+Exact (Rlt_ge_not r R0 r0).
+Assumption.
+Trivial.
+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;
@@ -94,6 +123,17 @@ Apply Rle_sym2;Assumption.
 Save.
 
 (*********)
+Lemma Rabsolu_pos_eq:(x:R)(Rle R0 x)->(Rabsolu x)==x.
+Intros;Unfold Rabsolu;Case (case_Rabsolu x);Intro;
+ [Generalize (Rle_not R0 x r);Intro;ElimType False;Auto|Trivial].
+Save.
+
+(*********)
+Lemma Rabsolu_Rabsolu:(x:R)(Rabsolu (Rabsolu x))==(Rabsolu x).
+Intro;Apply (Rabsolu_pos_eq (Rabsolu x) (Rabsolu_pos x)).
+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.
@@ -249,46 +289,22 @@ 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.  
+Intros;
+ Apply (Rle_anti_compatibility (Rabsolu b)
+        (Rminus (Rabsolu a) (Rabsolu b)) (Rabsolu (Rminus a b)));
+ Unfold Rminus;
+ Rewrite <- (Rplus_assoc (Rabsolu b) (Rabsolu a) (Ropp (Rabsolu b)));
+ Rewrite (Rplus_sym (Rabsolu b) (Rabsolu a));
+ Rewrite (Rplus_assoc (Rabsolu a) (Rabsolu b) (Ropp (Rabsolu b)));
+ Rewrite (Rplus_Ropp_r (Rabsolu b));
+ Rewrite (proj1 ? ? (Rplus_ne (Rabsolu a)));
+ Replace (Rabsolu a) with (Rabsolu (Rplus a R0)).
+ Rewrite <- (Rplus_Ropp_r b);
+ Rewrite <- (Rplus_assoc a b (Ropp b)); 
+ Rewrite (Rplus_sym a b);
+ Rewrite (Rplus_assoc b a (Ropp b)).
+ Exact (Rabsolu_triang b (Rplus a (Ropp b))).
+ Rewrite (proj1 ? ? (Rplus_ne a));Trivial.
 Save.
 
 (*********)
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index c0ade34e1..c030cb4a0 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -17,7 +17,45 @@ Fixpoint fact [n:nat]:nat:=
      O     => (S O)
     |(S n) => (mult (S n) (fact n))
   end.
+
+(*********)
+(*Lemma mult_neq_O:(n,m:nat)~n=O->~m=O->~(mult n m)=O.
+Double Induction 1 2;Simpl;Auto.
+Save.*)
  
+(*********)
+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.
+Intros; Replace (plus (fact n0) (mult n0 (fact n0))) with 
+  (mult (fact n0) (plus n0 (1))).
+Cut ~(plus n0 (1))=O.
+Intro;Apply H;Assumption.
+Replace (plus n0 (1)) with (S n0);[Auto|Ring].
+Intros;Ring.
+Double Induction 1 2;Simpl;Auto.
+Save.
+
+(*********)
+Lemma INR_fact_neq_0:(n:nat)~(INR (fact n))==R0.
+Intro;Red;Intro;Apply (not_O_INR (fact n) (fact_neq_0 n));Assumption.
+Save.    
+
+(*********)
+Lemma simpl_fact:(n:nat)(Rmult (Rinv (INR (fact (S n)))) 
+         (Rinv (Rinv (INR (fact n)))))==
+         (Rinv (INR (S n))).
+Intro;Rewrite (Rinv_Rinv (INR (fact n)) (INR_fact_neq_0 n)); 
+ Unfold 1 fact;Cbv Beta Iota;Fold fact;
+ Rewrite (mult_INR (S n) (fact n));
+ Rewrite (Rinv_Rmult (INR (S n)) (INR (fact n))).
+Rewrite (Rmult_assoc (Rinv (INR (S n))) (Rinv (INR (fact n))) 
+  (INR (fact n)));Rewrite (Rinv_l (INR (fact n)) (INR_fact_neq_0 n));
+ Apply (let (H1,H2)=(Rmult_ne (Rinv (INR (S n)))) in H1).
+Apply not_O_INR;Auto.
+Apply INR_fact_neq_0.
+Save.
+
 (*******************************)
 (*          Power              *)
 (*******************************)
@@ -86,6 +124,7 @@ Definition sum_f [s,n:nat;f:nat->R]:R:=
 (*******************************)
 (*********)
 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_R0 s n) l) eps)).
+  (eps:R)(Rgt eps R0)->
+  (Ex[N:nat](n:nat)(ge n N)->(Rlt (R_dist (sum_f_R0 s n) l) eps)).