*** empty log message ***

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

3 files changed, 23 insertions, 27 deletions

diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 45e03ca7a..482cfa0cc 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -1582,30 +1582,3 @@ end.
 Theorem INR_eq_INR2 : (n:nat) (INR n)==(INR2 n).
 Induction n; [Unfold INR INR2; Reflexivity | Intros; Unfold INR INR2; Fold INR INR2; Rewrite H; Case n0; [Reflexivity | Intros; Ring]].
 Save.
-
-(*****************************************************)
-(*          Some properties of Rmin and Rmax         *)
-(*****************************************************)
-Lemma Rmin_l : (x,y:R) ``(Rmin x y)<=x``.
-Intros; Unfold Rmin; Case (total_order_Rle x y); Intro H1; [Right; Reflexivity | Auto with real].
-Save.
-  
-Lemma Rmin_r : (x,y:R) ``(Rmin x y)<=y``.
-Intros; Unfold Rmin; Case (total_order_Rle x y); Intro H1; [Assumption | Auto with real].
-Save.
-
-Lemma Rmin_stable_in_posreal : (x,y:posreal) ``0<(Rmin x y)``.
-Intros; Apply Rmin_Rgt_r; Split; [Apply (cond_pos x) | Apply (cond_pos y)].
-Save.
-
-Lemma Rmax_l : (x,y:R) ``x<=(Rmax x y)``.
-Intros; Unfold Rmax; Case (total_order_Rle x y); Intro H1; [Assumption | Right; Reflexivity].
-Save.
-
-Lemma Rmax_r : (x,y:R) ``y<=(Rmax x y)``.
-Intros; Unfold Rmax; Case (total_order_Rle x y); Intro H1; [Right; Reflexivity | Auto with real].
-Save.
-
-Lemma Rmax_stable_in_negreal : (x,y:negreal) ``(Rmax x y)<0``.
-Intros; Unfold Rmax; Case (total_order_Rle x y); Intro; [Apply (cond_neg y) | Apply (cond_neg x)].
-Save.
\ No newline at end of file
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 34bb1f790..f82bd96d0 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -14,6 +14,7 @@
 (*********************************************************)
 
 Require Export R_Ifp.
+Require Export Rbase.
 Require Fourier.
 
 (*******************************)
@@ -54,6 +55,21 @@ Exact (Rmin_Rgt_l r1 r2 r).
 Exact (Rmin_Rgt_r r1 r2 r).
 Save.
 
+(*********)
+Lemma Rmin_l : (x,y:R) ``(Rmin x y)<=x``.
+Intros; Unfold Rmin; Case (total_order_Rle x y); Intro H1; [Right; Reflexivity | Auto with real].
+Save.
+ 
+(*********)
+Lemma Rmin_r : (x,y:R) ``(Rmin x y)<=y``.
+Intros; Unfold Rmin; Case (total_order_Rle x y); Intro H1; [Assumption | Auto with real].
+Save.
+
+(*********)
+Lemma Rmin_stable_in_posreal : (x,y:posreal) ``0<(Rmin x y)``.
+Intros; Apply Rmin_Rgt_r; Split; [Apply (cond_pos x) | Apply (cond_pos y)].
+Save.
+
 (*******************************)
 (*           Rmax              *)
 (*******************************)
@@ -105,6 +121,10 @@ Apply Rle_monotony_contra with z := r; Auto.
 Rewrite <- E1; Repeat Rewrite Rmult_Ol; Auto.
 Save.
 
+Lemma Rmax_stable_in_negreal : (x,y:negreal) ``(Rmax x y)<0``.
+Intros; Unfold Rmax; Case (total_order_Rle x y); Intro; [Apply (cond_neg y) | Apply (cond_neg x)].
+Save.
+
 (*******************************)
 (*           Rabsolu           *)
 (*******************************)
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 974c411dc..cf3ba98e0 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -14,6 +14,7 @@
 (*********************************************************)
 
 Require Export Rbasic_fun.
+Require Export R_sqr.
 Require Export Classical_Prop.
 Require DiscrR.
 Require Fourier.
@@ -583,6 +584,7 @@ Unfold limit1_in;Unfold limit_in;Simpl;Intros;
 Save.
 
 (*********)
+(*
 Lemma limit_inv : (f:R->R)(D:R->Prop)(l:R)(x0:R) (limit1_in f D l x0)->~(l==R0)->(limit1_in [x:R](Rinv (f x)) D (Rinv l) x0).
 Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Elim (H ``(Rabsolu l)/2``).
 Intros delta1 H2; Elim (H ``eps*((Rsqr l)/2)``).
@@ -630,3 +632,4 @@ Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption |
 Change ``0<eps*(Rsqr l)/2``; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Repeat Apply Rmult_lt_pos; [Assumption | Apply Rsqr_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0].
 Change ``0<(Rabsolu l)/2``; Unfold Rdiv; Apply Rmult_lt_pos; [Apply Rabsolu_pos_lt; Assumption | Apply Rlt_Rinv; Apply Rgt_2_0].
 Save.
+*)
\ No newline at end of file