*** empty log message ***

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

1 files changed, 20 insertions, 0 deletions

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           *)
 (*******************************)