Added the following lemmas to homogenize Reals a bit:

- Rmult_eq_compat_r, Rmult_eq_reg_r, Rplus_le_reg_r, Rmult_lt_reg_r,
  Rmult_le_reg_r (mirrored variants of the existing _l lemmas);
- minus_IZR, opp_IZR (Ropp_Ropp_IZR), abs_IZR (mirrored Rabs_Zabs);
- Rle_abs (RRle_abs);
- Zpower_pos_powerRZ (signed variant of Zpower_nat_powerRZ).

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

4 files changed, 68 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 70f183d15..6335a6b1d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -76,6 +76,7 @@ Library
 - The function Compare_dec.nat_compare is now defined directly,
   instead of relying on lt_eq_lt_dec. The earlier version is still
   available under the name nat_compare_alt.
+- Lemmas in library Reals have been homogenized a bit.
 
 Changes from V8.1 to V8.2
 =========================
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 55e3896a8..b2e561922 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -515,6 +515,13 @@ Qed.
 
 (*i Old i*)Hint Resolve Rmult_eq_compat_l: v62.
 
+Lemma Rmult_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 * r = r2 * r.
+Proof.
+  intros.
+  rewrite <- 2!(Rmult_comm r).
+  now apply Rmult_eq_compat_l.
+Qed.
+
 (**********)
 Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2.
 Proof.
@@ -525,6 +532,13 @@ Proof.
   field; trivial.
 Qed.
 
+Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r = r2 * r -> r <> 0 -> r1 = r2.
+Proof.
+  intros.
+  apply Rmult_eq_reg_l with (2 := H0).
+  now rewrite 2!(Rmult_comm r).
+Qed.
+
 (**********)
 Lemma Rmult_integral : forall r1 r2, r1 * r2 = 0 -> r1 = 0 \/ r2 = 0.
 Proof.
@@ -973,6 +987,13 @@ Proof.
   right; apply (Rplus_eq_reg_l r r1 r2 H0).
 Qed.
 
+Lemma Rplus_le_reg_r : forall r r1 r2, r1 + r <= r2 + r -> r1 <= r2.
+Proof.
+  intros.
+  apply (Rplus_le_reg_l r).
+  now rewrite 2!(Rplus_comm r).
+Qed.
+
 Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2.
 Proof.
   unfold Rgt in |- *; intros; apply (Rplus_lt_reg_r r r2 r1 H).
@@ -1267,6 +1288,14 @@ Proof.
       intro; apply (Rlt_irrefl (z * x)); auto.
 Qed.
 
+Lemma Rmult_lt_reg_r : forall r r1 r2 : R, 0 < r -> r1 * r < r2 * r -> r1 < r2.
+Proof.
+  intros.
+  apply Rmult_lt_reg_l with r.
+  exact H.
+  now rewrite 2!(Rmult_comm r).
+Qed.
+
 Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
 Proof. eauto using Rmult_lt_reg_l with rorders. Qed.
 
@@ -1282,6 +1311,14 @@ Proof.
   rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
 Qed.
 
+Lemma Rmult_le_reg_r : forall r r1 r2, 0 < r -> r1 * r <= r2 * r -> r1 <= r2.
+Proof.
+  intros.
+  apply Rmult_le_reg_l with r.
+  exact H.
+  now rewrite 2!(Rmult_comm r).
+Qed.
+
 (*********************************************************)
 (** ** Order and substraction                            *)
 (*********************************************************)
@@ -1741,11 +1778,20 @@ Proof.
 Qed.
 
 (**********)
-Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n.
+Lemma opp_IZR : forall n:Z, IZR (- n) = - IZR n.
 Proof.
   intro z; case z; simpl in |- *; auto with real.
 Qed.
 
+Definition Ropp_Ropp_IZR := opp_IZR.
+
+Lemma minus_IZR : forall n m:Z, IZR (n - m) = IZR n - IZR m.
+Proof.
+  intros; unfold Zminus, Rminus.
+  rewrite <- opp_IZR.
+  apply plus_IZR.
+Qed.
+
 (**********)
 Lemma Z_R_minus : forall n m:Z, IZR n - IZR m = IZR (n - m).
 Proof.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 9856b5452..1fcf6f61e 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -220,11 +220,13 @@ Proof.
   apply Rge_le; assumption.
 Qed.
 
-Lemma RRle_abs : forall x:R, x <= Rabs x.
+Lemma Rle_abs : forall x:R, x <= Rabs x.
 Proof.
   intro; unfold Rabs in |- *; case (Rcase_abs x); intros; fourier.
 Qed.
 
+Definition RRle_abs := Rle_abs.
+
 (*********)
 Lemma Rabs_pos_eq : forall x:R, 0 <= x -> Rabs x = x.
 Proof.
@@ -507,3 +509,8 @@ Proof.
   apply Rabs_right; auto with real zarith.
 Qed.
  
+Lemma abs_IZR : forall z, IZR (Zabs z) = Rabs (IZR z).
+Proof.
+  intros.
+  now rewrite Rabs_Zabs.
+Qed.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index da28184f2..68862f492 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -619,6 +619,18 @@ Proof.
   unfold Zpower_nat in |- *; auto.
 Qed.
 
+Lemma Zpower_pos_powerRZ :
+  forall n m, IZR (Zpower_pos n m) = IZR n ^Z Zpos m.
+Proof.
+  intros.
+  rewrite Zpower_pos_nat; simpl.
+  induction (nat_of_P m).
+  easy.
+  unfold Zpower_nat; simpl.
+  rewrite mult_IZR.
+  now rewrite <- IHn0.
+Qed.
+
 Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z.
 Proof.
   intros x z; case z; simpl in |- *; auto with real.