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

1 files changed, 47 insertions, 1 deletions

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.