Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.

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

3 files changed, 79 insertions, 18 deletions

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 45e91577ea..e037c77b59 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -16,14 +16,7 @@ Lemma Rlt_R0_R2 : 0 < 2.
 change 2 with (INR 2); apply lt_INR_0; apply lt_O_Sn.
 Qed.
 
-Lemma Rplus_lt_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x + y.
-intros.
-apply Rlt_trans with x.
-assumption.
-pattern x at 1 in |- *; rewrite <- Rplus_0_r.
-apply Rplus_lt_compat_l.
-assumption.
-Qed.
+Notation Rplus_lt_pos := Rplus_lt_0_compat (only parsing).
 
 Lemma IZR_eq : forall z1 z2:Z, z1 = z2 -> IZR z1 = IZR z2.
 intros; rewrite H; reflexivity.
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index 66bac9de77..1d44b3e731 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -51,11 +51,9 @@ Proof.
   apply prod_neq_R0; assumption.
 Qed.
 
-Lemma Rmin_pos : forall x y:R, 0 < x -> 0 < y -> 0 < Rmin x y.
-Proof.
-  intros; unfold Rmin in |- *.
-  case (Rle_dec x y); intro; assumption.
-Qed.
+(* begin hide *)
+Notation Rmin_pos := Rmin_pos (only parsing). (* compat *)
+(* end hide *)
 
 Lemma maj_term1 :
   forall (x h eps l1 alp_f2:R) (eps_f2 alp_f1d:posreal)
@@ -386,10 +384,9 @@ Proof.
   apply Rplus_lt_compat_l; assumption.
 Qed.
 
-Lemma Rmin_2 : forall a b c:R, a < b -> a < c -> a < Rmin b c.
-Proof.
-  intros; unfold Rmin in |- *; case (Rle_dec b c); intro; assumption.
-Qed.
+(* begin hide *)
+Notation Rmin_2 := Rmin_glb_lt (only parsing).
+(* end hide *)
 
 Lemma quadruple : forall x:R, 4 * x = x + x + x + x.
 Proof.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 5c3a929afa..08e6323ea5 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -16,7 +16,7 @@
 Require Import Rbase.
 Require Import R_Ifp.
 Require Import Fourier.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Implicit Type r : R.
 
@@ -32,6 +32,13 @@ Definition Rmin (x y:R) : R :=
   end.
 
 (*********)
+Lemma Rmin_case : forall r1 r2 (P:R -> Type), P r1 -> P r2 -> P (Rmin r1 r2).
+Proof.
+  intros r1 r2 P H1 H2; unfold Rmin in |- *; case (Rle_dec r1 r2);
+    auto with arith.
+Qed.
+
+(*********)
 Lemma Rmin_Rgt_l : forall r1 r2 r, Rmin r1 r2 > r -> r1 > r /\ r2 > r.
 Proof.
   intros r1 r2 r; unfold Rmin in |- *; case (Rle_dec r1 r2); intros.
@@ -85,6 +92,25 @@ Proof.
   intros; apply Rmin_Rgt_r; split; [ apply (cond_pos x) | apply (cond_pos y) ].
 Qed.
 
+(*********)
+Lemma Rmin_pos : forall x y:R, 0 < x -> 0 < y -> 0 < Rmin x y.
+Proof.
+  intros; unfold Rmin in |- *.
+  case (Rle_dec x y); intro; assumption.
+Qed.
+
+(*********)
+Lemma Rmin_glb : forall a b c:R, a <= b -> a <= c -> a <= Rmin b c.
+Proof.
+  intros; unfold Rmin in |- *; case (Rle_dec b c); intro; assumption.
+Qed.
+
+(*********)
+Lemma Rmin_glb_lt : forall a b c:R, a < b -> a < c -> a < Rmin b c.
+Proof.
+  intros; unfold Rmin in |- *; case (Rle_dec b c); intro; assumption.
+Qed.
+
 (*******************************)
 (** *        Rmax              *)
 (*******************************)
@@ -97,6 +123,13 @@ Definition Rmax (x y:R) : R :=
   end.
 
 (*********)
+Lemma Rmax_case : forall r1 r2 (P:R -> Type), P r1 -> P r2 -> P (Rmax r1 r2).
+Proof.
+  intros r1 r2 P H1 H2; unfold Rmax in |- *; case (Rle_dec r1 r2);
+    auto with arith.
+Qed.
+
+(*********)
 Lemma Rmax_Rle : forall r1 r2 r, r <= Rmax r1 r2 <-> r <= r1 \/ r <= r2.
 Proof.
   intros; split.
@@ -124,8 +157,25 @@ Proof.
     intros H1 H2; apply Rle_antisym; auto with real.
 Qed.
 
+(* begin hide *)
 Notation RmaxSym := Rmax_comm (only parsing).
+(* end hide *)
 
+(*********)
+Lemma Rmax_l : forall x y:R, x <= Rmax x y.
+Proof.
+  intros; unfold Rmax in |- *; case (Rle_dec x y); intro H1;
+    [ assumption | auto with real ].
+Qed.
+
+(*********)
+Lemma Rmax_r : forall x y:R, y <= Rmax x y.
+Proof.
+  intros; unfold Rmax in |- *; case (Rle_dec x y); intro H1;
+    [ right; reflexivity | auto with real ].
+Qed.
+
+(*********)
 Lemma RmaxRmult :
   forall (p q:R) r, 0 <= r -> Rmax (r * p) (r * q) = r * Rmax p q.
 Proof.
@@ -140,12 +190,33 @@ Proof.
   rewrite <- E1; repeat rewrite Rmult_0_l; auto.
 Qed.
 
+(*********)
 Lemma Rmax_stable_in_negreal : forall x y:negreal, Rmax x y < 0.
 Proof.
   intros; unfold Rmax in |- *; case (Rle_dec x y); intro;
     [ apply (cond_neg y) | apply (cond_neg x) ].
 Qed.
 
+(*********)
+Lemma Rmax_lub : forall a b c:R, a <= b -> a <= c -> a <= Rmax b c.
+Proof.
+  intros; unfold Rmax in |- *; case (Rle_dec b c); intro; assumption.
+Qed.
+
+(*********)
+Lemma Rmax_lub_lt : forall a b c:R, a < b -> a < c -> a < Rmax b c.
+Proof.
+  intros; unfold Rmax in |- *; case (Rle_dec b c); intro; assumption.
+Qed.
+
+(*********)
+Lemma Rmax_neg : forall x y:R, x < 0 -> y < 0 -> Rmax x y < 0.
+Proof.
+  intros; unfold Rmax in |- *.
+  case (Rle_dec x y); intro; assumption.
+Qed.
+
+
 (*******************************)
 (** *        Rabsolu           *)
 (*******************************)