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, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 70f183d15b..6335a6b1d7 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
 =========================