ajouts

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

4 files changed, 78 insertions, 11 deletions

diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 579672866..7b7ec3103 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -161,4 +161,7 @@ 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))).
+Axiom complet:(E:R->Prop)(bound E)->
+              (ExT [x:R] (E x))->
+              (ExT [m:R](is_lub E m)).
+
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 97df55590..63b9a3cfb 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -34,6 +34,28 @@ Intro;Elim H;Intros;Clear H;Unfold Rmin;Case (total_order_Rle r1 r2);
 Save.
 
 (*******************************)
+(*           Rmax              *)
+(*******************************)
+
+(*********)
+Definition Rmax :R->R->R:=[x,y:R]
+  Cases (total_order_Rle x y) of 
+    (leftT _)  => y
+  | (rightT _) => x
+  end.
+
+(*********)
+Lemma Rmax_Rle:(r1,r2,r:R)(Rle r (Rmax r1 r2))<->
+    ((Rle r r1)\/(Rle r r2)).
+Intros;Split.
+Unfold Rmax;Case (total_order_Rle r1 r2);Intros;Auto.
+Intro;Unfold Rmax;Case (total_order_Rle r1 r2);Elim H;Clear H;Intros;Auto.
+Apply (Rle_trans r r1 r2);Auto.
+Generalize (not_Rle r1 r2 n);Clear n;Intro;Unfold Rgt in H0;
+ Apply (Rlt_le r r1 (Rle_lt_trans r r2 r1 H H0)).
+Save.
+
+(*******************************)
 (*           Rabsolu           *)
 (*******************************)
 
@@ -268,3 +290,25 @@ Intro; Rewrite Rplus_Ropp_l in H;
  Apply Rlt_le;Assumption.
 Unfold Rle;Right;Trivial.  
 Save.
+
+(*********)
+Lemma Rabsolu_def1:(x,a:R)(Rlt x a)->(Rlt (Ropp a) x)->(Rlt (Rabsolu x) a).
+Unfold Rabsolu;Intros;Case (case_Rabsolu x);Intro.
+Generalize (Rlt_Ropp (Ropp a) x H0);Unfold Rgt;Rewrite Ropp_Ropp;Intro;
+ Assumption.
+Assumption.
+Save.
+
+(*********)
+Lemma Rabsolu_def2:(x,a:R)(Rlt (Rabsolu x) a)->(Rlt x a)/\(Rlt (Ropp a) x).
+Unfold Rabsolu;Intro x;Case (case_Rabsolu x);Intros.
+Generalize (Rlt_RoppO x r);Unfold Rgt;Intro;
+ Generalize (Rlt_trans R0 (Ropp x) a H0 H);Intro;Split. 
+Apply (Rlt_trans x R0 a r H1).
+Generalize (Rlt_Ropp (Ropp x) a H);Rewrite (Ropp_Ropp x);Unfold Rgt;Trivial.
+Fold (Rgt a x) in H;Generalize (Rgt_ge_trans a x R0 H r);Intro;
+ Generalize (Rgt_RoppO a H0);Intro;Fold (Rgt R0 (Ropp a));
+ Generalize (Rge_gt_trans x R0 (Ropp a) r H1);Unfold Rgt;Intro;Split;
+ Assumption.
+Save.
+
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index d36ca5897..680a18ab9 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -399,6 +399,14 @@ Intros;Generalize (H2 x1 H3);Clear H2;Intro;Rewrite Ropp_mul1 in H2;
 Save.
 
 (*********)
+Lemma Dminus:(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](Rminus (f x) (g x)) [x:R](Rminus (df x) (dg x)) D x0).
+Unfold Rminus;Intros;Generalize (Dopp D g dg x0 H0);Intro;
+ Apply (Dadd D df [x:R](Ropp (dg x)) f [x:R](Ropp (g x)) x0);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).
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 987a6ea63..c0ade34e1 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -49,31 +49,43 @@ Save.
 (*  Sum of n first naturals    *)
 (*******************************)
 (*********)
-Fixpoint sum_nat_aux [s,n:nat]:nat:=       
+Fixpoint sum_nat_f_O [f:nat->nat;n:nat]:nat:=       
   Cases n of                            
-    O => s                                
-   |(S n') => (sum_nat_aux (plus s n) n') 
+    O => (f O)                               
+   |(S n') => (plus (sum_nat_f_O f n') (f (S n'))) 
   end.
 
 (*********)
-Definition sum_nat:=(sum_nat_aux O).  
+Definition sum_nat_f [s,n:nat;f:nat->nat]:nat:=      
+  (sum_nat_f_O [x:nat](f (plus x s)) (minus n s)).
+
+(*********)
+Definition sum_nat_O [n:nat]:nat:=
+  (sum_nat_f_O [x]x n).
+
+(*********)
+Definition sum_nat [s,n:nat]:nat:=
+  (sum_nat_f s n [x]x).
 
 (*******************************)
 (*             Sum             *)
 (*******************************)
 (*********)
-Fixpoint sum_aux [s:R;f:nat->R;N:nat]:R:=
+Fixpoint sum_f_R0 [f:nat->R;N:nat]:R:=
   Cases N of
-     O     => (Rplus s (f O))
-    |(S i) => (sum_aux (Rplus s (f N)) f i)
+     O     => (f O)
+    |(S i) => (Rplus (sum_f_R0 f i) (f (S i)))
   end.
- 
+
 (*********)
-Definition sum_f:=(sum_aux R0).  
+Definition sum_f [s,n:nat;f:nat->R]:R:=      
+  (sum_f_R0 [x:nat](f (plus x s)) (minus n s)).
 
 (*******************************)
 (*        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)).
+  (eps:R)(Ex[N:nat](n:nat)(ge n N)/\(Rlt (R_dist (sum_f_R0 s n) l) eps)).
+
+