- Amélioration de la présentation de RIneq, même si un nettoyage des

  Hints reste à faire. (dommage que Rge et Rle ne soient pas
  convertibles)
- Ajout de Nnat et Ndigits dans NArith.v



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

3 files changed, 577 insertions, 445 deletions

diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index 5a2eeda48..53ba50ffe 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -12,5 +12,7 @@
 
 Require Export BinPos.
 Require Export BinNat.
+Require Export Nnat.
+Require Export Ndigits.
 
 Require Export NArithRing.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 8b3847340..0f1b9fdf0 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -8,9 +8,9 @@
 
 (*i $Id$ i*)
 
-(***************************************************************************)
-(**              Basic lemmas for the classical reals numbers              *)
-(***************************************************************************)
+(*********************************************************)
+(** * Basic lemmas for the classical real numbers        *)
+(*********************************************************)
 
 Require Export Raxioms.
 Require Import Rpow_def.
@@ -24,21 +24,32 @@ Open Local Scope R_scope.
 
 Implicit Type r : R.
 
-(**************************************************************************)
-(** * Relation between orders and equality                                *)
-(**************************************************************************)
+(*********************************************************)
+(** ** Relation between orders and equality              *)
+(*********************************************************)
+
+(** Reflexivity of the large order *)
+
+Lemma Rle_refl : forall r, r <= r.
+Proof.
+  intro; right; reflexivity.
+Qed.
+Hint Resolve Rle_refl : real2.
+
+Lemma Rge_refl : forall r, r <= r.
+Proof. exact Rle_refl. Qed.
+Hint Resolve Rge_refl : real2.
+
+(** Irreflexivity of the strict order *)
 
-(**********)
 Lemma Rlt_irrefl : forall r, ~ r < r.
 Proof.
   generalize Rlt_asym. intuition eauto.
 Qed.
 Hint Resolve Rlt_irrefl: real.
 
-Lemma Rle_refl : forall r, r <= r.
-Proof.
-  intro; right; reflexivity.
-Qed.
+Lemma Rgt_irrefl : forall r, ~ r > r.
+Proof. exact Rlt_irrefl. Qed.
 
 Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2.
 Proof.
@@ -58,7 +69,7 @@ Proof.
 Qed.
 Hint Resolve Rlt_dichotomy_converse: real.
 
-(** Reasoning by case on equalities and order *)
+(** Reasoning by case on equality and order *)
 
 (**********)
 Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2.
@@ -80,17 +91,27 @@ Proof.
   intros; generalize (total_order_T r1 r2); tauto.
 Qed.
 
+(*********************************************************)
+(** ** Relating [<], [>], [<=] and [>=]  	         *)
+(*********************************************************)
 
-(*********************************************************************************)
-(** *     Order Lemma  : relating [<], [>], [<=] and [>=]  	                 *)
-(*********************************************************************************)
+(*********************************************************)
+(** ** Order                                             *)
+(*********************************************************)
+
+(** *** Relating strict and large orders *)
 
-(**********)
 Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2.
 Proof.
   intros; red in |- *; tauto.
 Qed.
-Hint Resolve Rlt_le: real.
+
+Hint Resolve Rlt_le: real real2.
+
+Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2.
+Proof.
+  intros; red; tauto.
+Qed.
 
 (**********)
 Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1.
@@ -99,47 +120,77 @@ Proof.
 Qed.
 
 Hint Immediate Rle_ge: real.
+Hint Resolve Rle_ge: real2.
 
-(**********)
 Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1.
 Proof.
   destruct 1; red in |- *; auto with real.
 Qed.
 
 Hint Resolve Rge_le: real.
+Hint Immediate Rge_le: real2.
 
 (**********)
 Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1.
-Proof. trivial. Qed.
+Proof. 
+  trivial.
+Qed.
+Hint Resolve Rlt_gt: real2.
 
-(**********)
 Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1.
-Proof. trivial. Qed.
+Proof.
+  trivial.
+Qed.
+Hint Immediate Rgt_lt: real2.
 
 (**********)
+
 Lemma Rnot_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1.
 Proof.
   intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle in |- *; tauto.
 Qed.
-
 Hint Immediate Rnot_le_lt: real.
 
+Lemma Rnot_ge_gt : forall r1 r2, ~ r1 >= r2 -> r2 > r1.
+Proof. intros; red; apply Rnot_le_lt. auto with real. Qed.
+
+Lemma Rnot_le_gt : forall r1 r2, ~ r1 <= r2 -> r1 > r2.
+Proof. intros; red; apply Rnot_le_lt. auto with real. Qed.
+
 Lemma Rnot_ge_lt : forall r1 r2, ~ r1 >= r2 -> r1 < r2.
+Proof. intros; apply Rnot_le_lt. auto with real. Qed.
+
+Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1.
 Proof.
-  intros; apply Rnot_le_lt; auto with real.
+  intros r1 r2 H; destruct (Rtotal_order r1 r2) as [ | [ H0 | H0 ] ].
+    contradiction. subst; auto with real2. auto with real2.
 Qed.
 
+Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2.
+Proof. auto using Rnot_lt_le with real. Qed.
+
+Lemma Rnot_gt_ge : forall r1 r2, ~ r1 > r2 -> r2 >= r1.
+Proof. intros; eauto using Rnot_lt_le with real2. Qed.
+
+Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2.
+Proof. eauto using Rnot_gt_ge with real2. Qed.
+
 (**********)
 Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
 Proof.
   generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle in |- *.
   intuition eauto 3.
 Qed.
+Hint Immediate Rlt_not_le: real.
 
 Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2.
-Proof Rlt_not_le.
+Proof. exact Rlt_not_le. Qed.
 
-Hint Immediate Rlt_not_le: real.
+Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2.
+Proof. red; intros; eapply Rlt_not_le; eauto with real. Qed.
+
+Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2.
+Proof. exact Rlt_not_ge. Qed.
 
 Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> ~ r1 < r2.
 Proof.
@@ -147,13 +198,14 @@ Proof.
   unfold Rle in |- *; intuition.
 Qed.
 
-(**********)
-Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2.
-Proof.
-  generalize Rlt_not_le. unfold Rle, Rge in |- *. intuition eauto 3.
-Qed.
+Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> ~ r1 < r2.
+Proof. intros; apply Rle_not_lt; auto with real. Qed.
 
-Hint Immediate Rlt_not_ge: real.
+Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> ~ r1 > r2.
+Proof. do 2 intro; apply Rle_not_lt. Qed.
+
+Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> ~ r1 > r2.
+Proof. do 2 intro; apply Rge_not_lt. Qed.
 
 (**********)
 Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2.
@@ -180,25 +232,51 @@ Proof.
 Qed.
 Hint Immediate Req_ge_sym: real.
 
+(** *** Asymmetry *)
+
+(** Remark: [Rlt_asym] is an axiom *)
+
+Lemma Rgt_asym : forall r1 r2:R, r1 > r2 -> ~ r2 > r1.
+Proof. do 2 intro; apply Rlt_asym. Qed.
+
+(** *** Antisymmetry *)
+
 Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2.
 Proof.
   intros r1 r2; generalize (Rlt_asym r1 r2); unfold Rle in |- *; intuition.
 Qed.
 Hint Resolve Rle_antisym: real.
 
+Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2.
+Proof. auto with real. Qed.
+
 (**********)
 Lemma Rle_le_eq : forall r1 r2, r1 <= r2 /\ r2 <= r1 <-> r1 = r2.
 Proof.
   intuition.
 Qed.
 
+Lemma Rge_ge_eq : forall r1 r2, r1 >= r2 /\ r2 >= r1 <-> r1 = r2.
+Proof.
+  intuition.
+Qed.
+
+(** *** Compatibility with equality *)
+
 Lemma Rlt_eq_compat :
   forall r1 r2 r3 r4, r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3.
 Proof.
   intros x x' y y'; intros; replace x with x'; replace y with y'; assumption.
 Qed.
 
-(**********)
+Lemma Rgt_eq_compat :
+  forall r1 r2 r3 r4, r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3.
+Proof. intros; red; apply Rlt_eq_compat with (r2:=r4) (r4:=r2); auto. Qed.
+
+(** *** Transitivity *)
+
+(** Remark: [Rlt_trans] is an axiom *)
+
 Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3.
 Proof.
   generalize trans_eq Rlt_trans Rlt_eq_compat.
@@ -206,6 +284,12 @@ Proof.
   intuition eauto 2.
 Qed.
 
+Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3.
+Proof. eauto using Rle_trans with real2. Qed.
+
+Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3.
+Proof. eauto using Rlt_trans with real2. Qed.
+
 (**********)
 Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3.
 Proof.
@@ -214,14 +298,19 @@ Proof.
   intuition eauto 2.
 Qed.
 
-(**********)
 Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3.
 Proof.
   generalize Rlt_trans Rlt_eq_compat; unfold Rle in |- *; intuition eauto 2.
 Qed.
 
+Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3.
+Proof. eauto using Rlt_le_trans with real2. Qed.
+
+Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3.
+Proof. eauto using Rle_lt_trans with real2. Qed.
+
+(** *** (Classical) decidability *)
 
-(** Decidability of the order *)
 Lemma Rlt_dec : forall r1 r2, {r1 < r2} + {~ r1 < r2}.
 Proof.
   intros; generalize (total_order_T r1 r2) (Rlt_dichotomy_converse r1 r2);
@@ -236,35 +325,43 @@ Proof.
 Qed.
 
 Lemma Rgt_dec : forall r1 r2, {r1 > r2} + {~ r1 > r2}.
-Proof.
-  intros; unfold Rgt in |- *; intros; apply Rlt_dec.
-Qed.
+Proof. do 2 intro; apply Rlt_dec. Qed.
 
 Lemma Rge_dec : forall r1 r2, {r1 >= r2} + {~ r1 >= r2}.
-Proof.
-  intros; generalize (Rle_dec r2 r1); intuition.
-Qed.
+Proof. intros; edestruct Rle_dec; [left|right]; eauto with real2. Qed.
 
 Lemma Rlt_le_dec : forall r1 r2, {r1 < r2} + {r2 <= r1}.
 Proof.
   intros; generalize (total_order_T r1 r2); intuition.
 Qed.
 
+Lemma Rgt_ge_dec : forall r1 r2, {r1 > r2} + {r2 >= r1}.
+Proof. intros; edestruct Rlt_le_dec; [left|right]; eauto with real2. Qed.
+
 Lemma Rle_lt_dec : forall r1 r2, {r1 <= r2} + {r2 < r1}.
 Proof.
   intros; generalize (total_order_T r1 r2); intuition.
 Qed.
 
+Lemma Rge_gt_dec : forall r1 r2, {r1 >= r2} + {r2 > r1}.
+Proof. intros; edestruct Rle_lt_dec; [left|right]; eauto with real2. Qed.
+
 Lemma Rlt_or_le : forall r1 r2, r1 < r2 \/ r2 <= r1.
 Proof.
   intros n m; elim (Rle_lt_dec m n); auto with real.
 Qed.
 
+Lemma Rgt_or_ge : forall r1 r2, r1 > r2 \/ r2 >= r1.
+Proof. intros; edestruct Rlt_or_le; [left|right]; eauto with real2. Qed.
+
 Lemma Rle_or_lt : forall r1 r2, r1 <= r2 \/ r2 < r1.
 Proof.
   intros n m; elim (Rlt_le_dec m n); auto with real.
 Qed.
 
+Lemma Rge_or_gt : forall r1 r2, r1 >= r2 \/ r2 > r1.
+Proof. intros; edestruct Rle_or_lt; [left|right]; eauto with real2. Qed.
+
 Lemma Rle_lt_or_eq_dec : forall r1 r2, r1 <= r2 -> {r1 < r2} + {r1 = r2}.
 Proof.
   intros r1 r2 H; generalize (total_order_T r1 r2); intuition.
@@ -277,19 +374,11 @@ Proof.
   intros n m p q; intros; generalize (Rlt_le_dec m q); intuition.
 Qed.
 
-(****************************************************************)
-(** *      Field Lemmas                                         *)
-(* This part contains lemma involving the Fields operations     *)
-(****************************************************************)
 (*********************************************************)
-(** **   Addition                                        *)
+(** ** Addition                                          *)
 (*********************************************************)
 
-Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r.
-Proof.
-  split; ring.
-Qed.
-Hint Resolve Rplus_ne: real v62.
+(** Remark: [Rplus_0_l] is an axiom *)
 
 Lemma Rplus_0_r : forall r, r + 0 = r.
 Proof.
@@ -297,14 +386,22 @@ Proof.
 Qed.
 Hint Resolve Rplus_0_r: real.
 
+Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r.
+Proof.
+  split; ring.
+Qed.
+Hint Resolve Rplus_ne: real v62.
+
 (**********)
+
+(** Remark: [Rplus_opp_r] is an axiom *)
+
 Lemma Rplus_opp_l : forall r, - r + r = 0.
 Proof.
   intro; ring.
 Qed.
 Hint Resolve Rplus_opp_l: real.
 
-
 (**********)
 Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 = 0 -> r2 = - r1.
 Proof.
@@ -313,7 +410,6 @@ Proof.
   rewrite Rplus_assoc; rewrite H; ring.
 Qed.
 
-(*i New i*)
 Hint Resolve (f_equal (A:=R)): real.
 
 Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2.
@@ -340,9 +436,31 @@ Proof.
   intros r b; pattern r at 2 in |- *; replace r with (r + 0); eauto with real.
 Qed.
 
-(***********************************************************)       
-(** **    Multiplication                                   *)
-(***********************************************************)
+(***********)
+Lemma Rplus_eq_0_l :
+  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0.
+Proof.
+  intros a b H [H0| H0] H1; auto with real.
+    absurd (0 < a + b).
+      rewrite H1; auto with real.
+      apply Rle_lt_trans with (a + 0).
+        rewrite Rplus_0_r in |- *; assumption.
+        auto using Rplus_lt_compat_l with real.
+    rewrite <- H0, Rplus_0_r in H1; assumption.
+Qed.
+
+Lemma Rplus_eq_R0 :
+  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0.
+Proof.
+  intros a b; split.
+  apply Rplus_eq_0_l with b; auto with real.
+  apply Rplus_eq_0_l with a; auto with real.
+  rewrite Rplus_comm; auto with real.
+Qed.
+
+(*********************************************************)       
+(** ** Multiplication                                    *)
+(*********************************************************)
 
 (**********)
 Lemma Rinv_r : forall r, r <> 0 -> r * / r = 1.
@@ -362,7 +480,6 @@ Proof.
 Qed.
 Hint Resolve Rinv_l_sym Rinv_r_sym: real.
 
-
 (**********)
 Lemma Rmult_0_r : forall r, r * 0 = 0.
 Proof.
@@ -397,7 +514,7 @@ Proof.
   auto with real.
 Qed.
 
-(*i OLD i*)Hint Resolve Rmult_eq_compat_l: v62.
+(*i Old i*)Hint Resolve Rmult_eq_compat_l: v62.
 
 (**********)
 Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2.
@@ -438,7 +555,6 @@ Proof.
   auto with real.
 Qed.
 
-
 (**********) 
 Lemma Rmult_neq_0_reg : forall r1 r2, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0.
 Proof.
@@ -454,6 +570,10 @@ Proof.
 Qed.
 Hint Resolve Rmult_integral_contrapositive: real.
 
+Lemma Rmult_integral_contrapositive_currified : 
+  forall r1 r2, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0.
+Proof. auto using Rmult_integral_contrapositive. Qed.
+
 (**********) 
 Lemma Rmult_plus_distr_r :
   forall r1 r2 r3, (r1 + r2) * r3 = r1 * r3 + r2 * r3.
@@ -461,7 +581,9 @@ Proof.
   intros; ring.
 Qed.
 
-(** ** Square function *)
+(*********************************************************)
+(** ** Square function                                   *)
+(*********************************************************)
 
 (***********)
 Definition Rsqr r : R := r * r.
@@ -479,7 +601,7 @@ Lemma Rsqr_0_uniq : forall r, Rsqr r = 0 -> r = 0.
 Qed.
 
 (*********************************************************)
-(** **   Opposite                                        *)
+(** ** Opposite                                          *)
 (*********************************************************)
 
 (**********)
@@ -526,8 +648,9 @@ Proof.
 Qed.
 Hint Resolve Ropp_plus_distr: real.
 
-
-(** ** Opposite and multiplication *)
+(*********************************************************)
+(** ** Opposite and multiplication                       *)
+(*********************************************************)
 
 Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 = - (r1 * r2).
 Proof.
@@ -547,7 +670,9 @@ Proof.
   intros; ring.
 Qed.
 
-(** ** Substraction *)
+(*********************************************************)
+(** ** Substraction                                      *)
+(*********************************************************)
 
 Lemma Rminus_0_r : forall r, r - 0 = r.
 Proof.
@@ -622,7 +747,6 @@ Proof.
 Qed.
 Hint Resolve Rminus_not_eq_right: real. 
 
-
 (**********)
 Lemma Rmult_minus_distr_l :
   forall r1 r2 r3, r1 * (r2 - r3) = r1 * r2 - r1 * r3.
@@ -630,7 +754,10 @@ Proof.
   intros; ring.
 Qed.
 
-(** ** Inverse *)
+(*********************************************************)
+(** ** Inverse                                           *)
+(*********************************************************)
+
 Lemma Rinv_1 : / 1 = 1.
 Proof.
   field.
@@ -694,28 +821,28 @@ Proof.
   ring.
 Qed.
 
-(** * Field operations and order *)
+(*********************************************************)
+(** ** Order and addition                                *)
+(*********************************************************)
+
+(** *** Compatibility *)
 
-(** ** Order and addition *)
+(** Remark: [Rplus_lt_compat_l] is an axiom *)
 
+Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2.
+Proof. eauto using Rplus_lt_compat_l with real2. Qed.
+Hint Resolve Rplus_gt_compat_l: real.
+
+(**********)
 Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r.
 Proof.
   intros.
   rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r); auto with real.
 Qed.
-
 Hint Resolve Rplus_lt_compat_r: real.
 
-(**********)
-Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
-Proof.
-  intros; cut (- r + r + r1 < - r + r + r2).
-  rewrite Rplus_opp_l.
-  elim (Rplus_ne r1); elim (Rplus_ne r2); intros; rewrite <- H3; rewrite <- H1;
-    auto with zarith real.
-  rewrite Rplus_assoc; rewrite Rplus_assoc;
-    apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H).
-Qed.
+Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r.
+Proof. do 3 intro; apply Rplus_lt_compat_r. Qed.
 
 (**********)
 Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.
@@ -725,6 +852,10 @@ Proof.
   right; rewrite <- H0; auto with zarith real.
 Qed.
 
+Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2.
+Proof. auto using Rplus_le_compat_l with real2. Qed.
+Hint Resolve Rplus_ge_compat_l: real.
+
 (**********)
 Lemma Rplus_le_compat_r : forall r r1 r2, r1 <= r2 -> r1 + r <= r2 + r.
 Proof.
@@ -735,23 +866,8 @@ Qed.
 
 Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real.
 
-(**********)
-Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
-Proof.
-  unfold Rle in |- *; intros; elim H; intro.
-  left; apply (Rplus_lt_reg_r r r1 r2 H0).
-  right; apply (Rplus_eq_reg_l r r1 r2 H0).
-Qed.
-
-(**********)
-Lemma sum_inequa_Rle_lt :
-  forall a x b c y d:R,
-    a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.
-Proof.
-  intros; split.
-  apply Rlt_le_trans with (a + y); auto with real.
-  apply Rlt_le_trans with (b + y); auto with real.
-Qed.
+Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r.
+Proof. auto using Rplus_le_compat_r with real2. Qed.
 
 (*********)
 Lemma Rplus_lt_compat :
@@ -766,6 +882,16 @@ Proof.
   intros; apply Rle_trans with (r2 + r3); auto with real.
 Qed.
 
+Hint Immediate Rplus_lt_compat Rplus_le_compat: real.
+
+Lemma Rplus_gt_compat :
+  forall r1 r2 r3 r4, r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4.
+Proof. auto using Rplus_lt_compat with real2. Qed.
+
+Lemma Rplus_ge_compat :
+  forall r1 r2 r3 r4, r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4.
+Proof. auto using Rplus_le_compat with real2. Qed.
+
 (*********)
 Lemma Rplus_lt_le_compat :
   forall r1 r2 r3 r4, r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4.
@@ -773,19 +899,133 @@ Proof.
   intros; apply Rlt_le_trans with (r2 + r3); auto with real.
 Qed.
 
-(*********)
 Lemma Rplus_le_lt_compat :
   forall r1 r2 r3 r4, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
 Proof.
   intros; apply Rle_lt_trans with (r2 + r3); auto with real.
 Qed.
 
-Hint Immediate Rplus_lt_compat Rplus_le_compat Rplus_lt_le_compat
-  Rplus_le_lt_compat: real.
+Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: real.
 
-(** ** Order and Opposite *)
+Lemma Rplus_gt_ge_compat :
+  forall r1 r2 r3 r4, r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4.
+Proof. auto using Rplus_lt_le_compat with real2. Qed.
+
+Lemma Rplus_ge_gt_compat :
+  forall r1 r2 r3 r4, r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4.
+Proof. auto using Rplus_le_lt_compat with real2. Qed.
 
 (**********)
+Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2.
+Proof.
+  intros x y; intros; apply Rlt_trans with x;
+    [ assumption
+      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
+        assumption ].
+Qed.
+
+Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2.
+Proof.
+  intros x y; intros; apply Rle_lt_trans with x;
+    [ assumption
+      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
+        assumption ].
+Qed.
+
+Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2.
+Proof.
+  intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat;
+    assumption.
+Qed.
+
+Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2.
+Proof.
+  intros x y; intros; apply Rle_trans with x;
+    [ assumption
+      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
+        assumption ].
+Qed.
+
+(**********)
+Lemma sum_inequa_Rle_lt :
+  forall a x b c y d:R,
+    a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.
+Proof.
+  intros; split.
+  apply Rlt_le_trans with (a + y); auto with real.
+  apply Rlt_le_trans with (b + y); auto with real.
+Qed.
+
+(** *** Cancellation *)
+
+Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
+Proof.
+  intros; cut (- r + r + r1 < - r + r + r2).
+  rewrite Rplus_opp_l.
+  elim (Rplus_ne r1); elim (Rplus_ne r2); intros; rewrite <- H3; rewrite <- H1;
+    auto with zarith real.
+  rewrite Rplus_assoc; rewrite Rplus_assoc;
+    apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H).
+Qed.
+
+Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
+Proof.
+  unfold Rle in |- *; intros; elim H; intro.
+  left; apply (Rplus_lt_reg_r r r1 r2 H0).
+  right; apply (Rplus_eq_reg_l r r1 r2 H0).
+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).
+Qed.
+
+Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2.
+Proof.
+  intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with real.
+Qed.
+
+(**********)
+Lemma Rplus_le_reg_pos_r :
+  forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3.
+Proof.
+  intros x y z; intros; apply Rle_trans with (x + y);
+    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
+      assumption
+      | assumption ].
+Qed.
+
+Lemma Rplus_lt_reg_pos_r : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3.
+Proof.
+  intros x y z; intros; apply Rle_lt_trans with (x + y);
+    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
+      assumption
+      | assumption ].
+Qed.
+
+Lemma Rplus_ge_reg_neg_r :
+  forall r1 r2 r3, 0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3.
+Proof.
+  intros x y z; intros; apply Rge_trans with (x + y);
+    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l;
+      assumption
+      | assumption ].
+Qed.
+
+Lemma Rplus_gt_reg_neg_r : forall r1 r2 r3, 0 >= r2 -> r1 + r2 > r3 -> r1 > r3.
+Proof.
+  intros x y z; intros; apply Rge_gt_trans with (x + y);
+    [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l;
+      assumption
+      | assumption ].
+Qed.
+
+(*********************************************************)
+(** ** Order and opposite                                *)
+(*********************************************************)
+
+(** *** Contravariant compatibility *)
+
 Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
 Proof.
   unfold Rgt in |- *; intros.
@@ -798,27 +1038,22 @@ Proof.
 Qed.
 Hint Resolve Ropp_gt_lt_contravar.
 
-(**********)
 Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
 Proof.
   unfold Rgt in |- *; auto with real.
 Qed.
 Hint Resolve Ropp_lt_gt_contravar: real.
 
-Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2.
-Proof.
-  intros x y H'.
-  rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
-    auto with real.
-Qed.
-Hint Immediate Ropp_lt_cancel: real.
-
+(**********)
 Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2.
 Proof.
   auto with real.
 Qed.
 Hint Resolve Ropp_lt_contravar: real.
 
+Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2.
+Proof. auto with real. Qed.
+
 (**********)
 Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2.
 Proof.
@@ -826,27 +1061,21 @@ Proof.
 Qed.
 Hint Resolve Ropp_le_ge_contravar: real.
 
-Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2.
+Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
 Proof.
-  intros x y H.
-  elim H; auto with real.
-  intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
-    rewrite H1; auto with real.
+  unfold Rge in |- *; intros r1 r2 [H| H]; auto with real.
 Qed.
-Hint Immediate Ropp_le_cancel: real.
+Hint Resolve Ropp_ge_le_contravar: real.
 
+(**********)
 Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2.
 Proof.
   intros r1 r2 H; elim H; auto with real.
 Qed.
 Hint Resolve Ropp_le_contravar: real.
 
-(**********)
-Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
-Proof.
-  unfold Rge in |- *; intros r1 r2 [H| H]; auto with real.
-Qed.
-Hint Resolve Ropp_ge_le_contravar: real.
+Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2.
+Proof. auto using Ropp_le_contravar with real. Qed.
 
 (**********)
 Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r.
@@ -855,7 +1084,6 @@ Proof.
 Qed.
 Hint Resolve Ropp_0_lt_gt_contravar: real.
 
-(**********)
 Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r.
 Proof.
   intros; replace 0 with (-0); auto with real.
@@ -868,7 +1096,6 @@ Proof.
   intros; rewrite <- Ropp_0; auto with real.
 Qed.
 
-(**********)
 Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0.
 Proof.
   intros; rewrite <- Ropp_0; auto with real.
@@ -882,40 +1109,57 @@ Proof.
 Qed.
 Hint Resolve Ropp_0_le_ge_contravar: real.
 
-(**********)
 Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r.
 Proof.
   intros; replace 0 with (-0); auto with real.
 Qed.
 Hint Resolve Ropp_0_ge_le_contravar: real.
 
-(** ** Order and multiplication *)
+(** *** Cancellation *)
 
-Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r.
+Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2.
 Proof.
-  intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real.
+  intros x y H'.
+  rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
+    auto with real.
 Qed.
-Hint Resolve Rmult_lt_compat_r.
+Hint Immediate Ropp_lt_cancel: real.
 
-Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
+Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2.
+Proof. auto using Ropp_lt_cancel with real2. Qed.
+
+Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2.
 Proof.
-  intros z x y H H0.
-  case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0.
-  rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto.
-  generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False;
-    generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1); 
-      intro; apply (Rlt_irrefl (z * x)); auto.
+  intros x y H.
+  elim H; auto with real.
+  intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
+    rewrite H1; auto with real.
 Qed.
+Hint Immediate Ropp_le_cancel: real.
 
+Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2.
+Proof. auto using Ropp_le_cancel with real2. Qed.
 
-Lemma Rmult_lt_gt_compat_neg_l :
-  forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2.
+(*********************************************************)
+(** ** Order and multiplication                          *)
+(*********************************************************)
+
+(** Remark: [Rmult_lt_compat_l] is an axiom *)
+
+(** *** Covariant compatibility *)
+
+Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r.
 Proof.
-  intros; replace r with (- - r); auto with real.
-  rewrite (Ropp_mult_distr_l_reverse (- r));
-    rewrite (Ropp_mult_distr_l_reverse (- r)).
-  apply Ropp_lt_gt_contravar; auto with real.
+  intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real.
 Qed.
+Hint Resolve Rmult_lt_compat_r.
+
+Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r.
+Proof. eauto using Rmult_lt_compat_r with real2. Qed.
+
+Lemma Rmult_gt_compat_l : forall r r1 r2, r > 0 -> r1 > r2 -> r * r1 > r * r2.
+Proof. eauto using Rmult_lt_compat_l with real2. Qed.
+Hint Resolve Rplus_gt_compat_l: real.
 
 (**********)
 Lemma Rmult_le_compat_l :
@@ -935,17 +1179,58 @@ Proof.
 Qed.
 Hint Resolve Rmult_le_compat_r: real.
 
-Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2.
+Lemma Rmult_ge_compat_l :
+  forall r r1 r2, r >= 0 -> r1 >= r2 -> r * r1 >= r * r2.
+Proof. eauto using Rmult_le_compat_l with real2. Qed.
+
+Lemma Rmult_ge_compat_r :
+  forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r.
+Proof. eauto using Rmult_le_compat_r with real2. Qed.
+
+(**********)
+Lemma Rmult_le_compat :
+  forall r1 r2 r3 r4,
+    0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
 Proof.
-  intros z x y H H0; case H0; auto with real.
-  intros H1; apply Rlt_le.
-  apply Rmult_lt_reg_l with (r := z); auto.
-  intros H1; replace x with (/ z * (z * x)); auto with real.
-  replace y with (/ z * (z * y)).
-  rewrite H1; auto with real.
-  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
-  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
+  intros x y z t H' H'0 H'1 H'2.
+  apply Rle_trans with (r2 := x * t); auto with real.
+  repeat rewrite (fun x => Rmult_comm x t).
+  apply Rmult_le_compat_l; auto.
+  apply Rle_trans with z; auto.
 Qed.
+Hint Resolve Rmult_le_compat: real.
+
+Lemma Rmult_ge_compat :
+  forall r1 r2 r3 r4,
+    0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
+Proof. auto with real real2. Qed.
+
+Lemma Rmult_gt_0_lt_compat :
+  forall r1 r2 r3 r4,
+    r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
+Proof.
+  intros; apply Rlt_trans with (r2 * r3); auto with real.
+Qed.
+
+(*********)
+Lemma Rmult_le_0_lt_compat :
+  forall r1 r2 r3 r4,
+    0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
+Proof.
+  intros; apply Rle_lt_trans with (r2 * r3);
+    [ apply Rmult_le_compat_r; [ assumption | left; assumption ]
+      | apply Rmult_lt_compat_l;
+        [ apply Rle_lt_trans with r1; assumption | assumption ] ].
+Qed.
+
+(*********)
+Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2.
+Proof. intros; replace 0 with (0 * r2); auto with real. Qed.
+
+Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0.
+Proof Rmult_lt_0_compat.
+
+(** *** Contravariant compatibility *)
 
 Lemma Rmult_le_compat_neg_l :
   forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1.
@@ -963,35 +1248,45 @@ Proof.
 Qed.
 Hint Resolve Rmult_le_ge_compat_neg_l: real.
 
-Lemma Rmult_le_compat :
-  forall r1 r2 r3 r4,
-    0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
+Lemma Rmult_lt_gt_compat_neg_l :
+  forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2.
 Proof.
-  intros x y z t H' H'0 H'1 H'2.
-  apply Rle_trans with (r2 := x * t); auto with real.
-  repeat rewrite (fun x => Rmult_comm x t).
-  apply Rmult_le_compat_l; auto.
-  apply Rle_trans with z; auto.
+  intros; replace r with (- - r); auto with real.
+  rewrite (Ropp_mult_distr_l_reverse (- r));
+    rewrite (Ropp_mult_distr_l_reverse (- r)).
+  apply Ropp_lt_gt_contravar; auto with real.
 Qed.
-Hint Resolve Rmult_le_compat: real.
 
-Lemma Rmult_gt_0_lt_compat :
-  forall r1 r2 r3 r4,
-    r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
+(** *** Cancellation *)
+
+Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
 Proof.
-  intros; apply Rlt_trans with (r2 * r3); auto with real.
+  intros z x y H H0.
+  case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0.
+  rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto.
+  generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False;
+    generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1); 
+      intro; apply (Rlt_irrefl (z * x)); auto.
 Qed.
 
-(*********)
-Lemma Rmult_ge_0_gt_0_lt_compat :
-  forall r1 r2 r3 r4,
-    r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
+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 real2. Qed.
+
+Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2.
 Proof.
-  intros; apply Rle_lt_trans with (r2 * r3); auto with real.
+  intros z x y H H0; case H0; auto with real.
+  intros H1; apply Rlt_le.
+  apply Rmult_lt_reg_l with (r := z); auto.
+  intros H1; replace x with (/ z * (z * x)); auto with real.
+  replace y with (/ z * (z * y)).
+  rewrite H1; auto with real.
+  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
+  rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
 Qed.
 
-
-(** ** Order and Substractions *)
+(*********************************************************)
+(** ** Order and substraction                            *)
+(*********************************************************)
 
 Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0.
 Proof.
@@ -1002,12 +1297,27 @@ Proof.
 Qed.
 Hint Resolve Rlt_minus: real.
 
+Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0.
+Proof. 
+  intros; apply (Rplus_lt_reg_r r2).
+  replace (r2 + (r1 - r2)) with r1.
+  replace (r2 + 0) with r2; auto with real.
+  ring.
+Qed.
+
 (**********)
 Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0.
 Proof.
   destruct 1; unfold Rle in |- *; auto with real.
 Qed.
 
+Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.
+Proof. 
+  destruct 1.
+    auto using Rgt_minus, Rgt_ge.
+    right; auto using Rminus_diag_eq with real2.
+Qed.
+
 (**********)
 Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2.
 Proof.
@@ -1016,6 +1326,14 @@ Proof.
   ring.
 Qed.
 
+Lemma Rminus_gt : forall r1 r2, r1 - r2 > 0 -> r1 > r2.
+Proof.
+  intros; replace r2 with (0 + r2); auto with real.
+  replace r1 with (r1 - r2 + r2).
+  apply Rplus_gt_compat_r; assumption.
+  ring.
+Qed.
+
 (**********)
 Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2.
 Proof.
@@ -1024,6 +1342,14 @@ Proof.
   ring.
 Qed.
 
+Lemma Rminus_ge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2.
+Proof.
+  intros; replace r2 with (0 + r2); auto with real.
+  replace r1 with (r1 - r2 + r2).
+  apply Rplus_ge_compat_r; assumption.
+  ring.
+Qed.
+
 (**********)
 Lemma tech_Rplus : forall r (s:R), 0 <= r -> 0 < s -> r + s <> 0.
 Proof.
@@ -1032,8 +1358,9 @@ Proof.
 Qed.
 Hint Immediate tech_Rplus: real.
 
-
-(** ** Order and the square function *)
+(*********************************************************)
+(** ** Order and square function                         *)
+(*********************************************************)
 
 Lemma Rle_0_sqr : forall r, 0 <= Rsqr r.
 Proof.
@@ -1053,7 +1380,26 @@ Proof.
 Qed.
 Hint Resolve Rle_0_sqr Rlt_0_sqr: real.
 
-(** ** Zero is less than one *)
+(***********)
+Lemma Rplus_sqr_eq_0_l : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0.
+Proof.
+  intros a b; intros; apply Rsqr_0_uniq; apply Rplus_eq_0_l with (Rsqr b);
+    auto with real.
+Qed.
+
+Lemma Rplus_sqr_eq_0 :
+  forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0.
+Proof.
+  intros a b; split.
+  apply Rplus_sqr_eq_0_l with b; auto with real.
+  apply Rplus_sqr_eq_0_l with a; auto with real.
+  rewrite Rplus_comm; auto with real.
+Qed.
+
+(*********************************************************)
+(** ** Zero is less than one                             *)
+(*********************************************************)
+
 Lemma Rlt_0_1 : 0 < 1.
 Proof.
   replace 1 with (Rsqr 1); auto with real.
@@ -1067,7 +1413,10 @@ Proof.
   exact Rlt_0_1.
 Qed.
 
-(** ** Order and inverse *)
+(*********************************************************)
+(** ** Order and inverse                                 *)
+(*********************************************************)
+
 Lemma Rinv_0_lt_compat : forall r, 0 < r -> 0 < / r.
 Proof.
   intros; apply Rnot_le_lt; red in |- *; intros.
@@ -1116,68 +1465,9 @@ Proof.
 Qed.
 Hint Resolve Rinv_1_lt_contravar: real.
 
-(********************************************************)        
-(** *     Greater                                       *)
-(********************************************************)
-
-(**********)
-Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2.
-Proof.
-  intros; apply Rle_antisym; auto with real.
-Qed.
-
-(**********)
-Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2.
-Proof.
-  intros; unfold Rge in |- *; elim (Rtotal_order r1 r2); intro.
-  absurd (r1 < r2); trivial.
-  case H0; auto.
-Qed.
-
-(**********)
-Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1.
-Proof.
-  intros; apply Rge_le; apply Rnot_lt_ge; assumption.
-Qed.
-
-(**********)
-Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2.
-Proof.
-  intros r1 r2 H; apply Rge_le.
-  exact (Rnot_lt_ge r2 r1 H).
-Qed.
-
-(**********)
-Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2.
-Proof.
-  red in |- *; auto with real.
-Qed.
-
-
-(**********)
-Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3.
-Proof.
-  unfold Rgt in |- *; intros; apply Rlt_le_trans with r2; auto with real.
-Qed.
-
-(**********)
-Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3.
-Proof.
-  unfold Rgt in |- *; intros; apply Rle_lt_trans with r2; auto with real.
-Qed.
-
-(**********)
-Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3.
-Proof.
-  unfold Rgt in |- *; intros; apply Rlt_trans with r2; auto with real.
-Qed.
-
-(**********)
-Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3.
-Proof.
-  intros; apply Rle_ge.
-  apply Rle_trans with r2; auto with real.
-Qed.
+(*********************************************************)        
+(** ** Miscellaneous                                     *)
+(*********************************************************)
 
 (**********)
 Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1.
@@ -1203,121 +1493,9 @@ Proof.
   pattern r1 at 2 in |- *; replace r1 with (r1 + 0); auto with real.
 Qed.
 
-(***********)
-Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2.
-Proof.
-  unfold Rgt in |- *; auto with real.
-Qed.
-Hint Resolve Rplus_gt_compat_l: real.
-
-(***********)
-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).
-Qed.
-
-(***********)
-Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2.
-Proof.
-  intros; apply Rle_ge; auto with real.
-Qed.
-Hint Resolve Rplus_ge_compat_l: real.
-
-(***********)
-Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2.
-Proof.
-  intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with real.
-Qed.
-
-(***********)
-Lemma Rmult_ge_compat_r :
-  forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r.
-Proof.
-  intros; apply Rle_ge; apply Rmult_le_compat_r; apply Rge_le; assumption.
-Qed.
-
-(***********)
-Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0.
-Proof.
-  intros; replace 0 with (r2 - r2); auto with real.
-  unfold Rgt, Rminus in |- *; auto with real.
-Qed.
-
-(*********)
-Lemma minus_Rgt : forall r1 r2, r1 - r2 > 0 -> r1 > r2.
-Proof.
-  intros; replace r2 with (r2 + 0); auto with real.
-  intros; replace r1 with (r2 + (r1 - r2)); auto with real.
-Qed.
-
-(**********)
-Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.
-Proof.
-  unfold Rge in |- *; intros; elim H; intro.
-  left; apply (Rgt_minus r1 r2 H0).
-  right; apply (Rminus_diag_eq r1 r2 H0).
-Qed.
-
-(*********)
-Lemma minus_Rge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2.
-Proof.
-  intros; replace r2 with (r2 + 0); auto with real.
-  intros; replace r1 with (r2 + (r1 - r2)); auto with real.
-Qed.
-
-
-(*********)
-Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0.
-Proof.
-  unfold Rgt in |- *; intros.
-  replace 0 with (0 * r2); auto with real.
-Qed.
-
-(*********)
-Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2.
-Proof Rmult_gt_0_compat.
-
-(***********)
-Lemma Rplus_eq_0_l :
-  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0.
-Proof.
-  intros a b [H| H] H0 H1; auto with real.
-  absurd (0 < a + b).
-  rewrite H1; auto with real.
-  replace 0 with (0 + 0); auto with real.
-Qed.
-
-
-Lemma Rplus_eq_R0 :
-  forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0.
-Proof.
-  intros a b; split.
-  apply Rplus_eq_0_l with b; auto with real.
-  apply Rplus_eq_0_l with a; auto with real.
-  rewrite Rplus_comm; auto with real.
-Qed.
-
-
-(***********)
-Lemma Rplus_sqr_eq_0_l : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0.
-Proof.
-  intros a b; intros; apply Rsqr_0_uniq; apply Rplus_eq_0_l with (Rsqr b);
-    auto with real.
-Qed.
-
-Lemma Rplus_sqr_eq_0 :
-  forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0.
-Proof.
-  intros a b; split.
-  apply Rplus_sqr_eq_0_l with b; auto with real.
-  apply Rplus_sqr_eq_0_l with a; auto with real.
-  rewrite Rplus_comm; auto with real.
-Qed.
-
-
-(**********************************************************) 
-(** *     Injection from [N] to [R]                       *)
-(**********************************************************)
+(*********************************************************) 
+(** ** Injection from [N] to [R]                         *)
+(*********************************************************)
 
 (**********)
 Lemma S_INR : forall n:nat, INR (S n) = INR n + 1.
@@ -1482,9 +1660,9 @@ Proof.
 Qed.
 Hint Resolve not_1_INR: real.
 
-(**********************************************************) 
-(** *    Injection from [Z] to [R]                        *)
-(**********************************************************)
+(*********************************************************) 
+(** ** Injection from [Z] to [R]                         *)
+(*********************************************************)
 
 
 (**********)
@@ -1708,32 +1886,6 @@ Proof.
   apply H3; apply single_z_r_R1 with r; trivial.
 Qed.
 
-(*****************************************************************)
-(** * Definitions of new types                                   *)
-(*****************************************************************)
-
-Record nonnegreal : Type := mknonnegreal
-  {nonneg :> R; cond_nonneg : 0 <= nonneg}.
-
-Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.
-
-Record nonposreal : Type := mknonposreal
-  {nonpos :> R; cond_nonpos : nonpos <= 0}.
-
-Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}.
-
-Record nonzeroreal : Type := mknonzeroreal
-  {nonzero :> R; cond_nonzero : nonzero <> 0}.
-
-(**********)
-Lemma prod_neq_R0 : forall r1 r2, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0.
-Proof.
-  intros x y; intros; red in |- *; intro; generalize (Rmult_integral x y H1);
-    intro; elim H2; intro;
-      [ rewrite H3 in H; elim H | rewrite H3 in H0; elim H0 ]; 
-      reflexivity.
-Qed.
-
 (*********)
 Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
 Proof.
@@ -1754,64 +1906,15 @@ Proof.
   [ apply not_O_INR; discriminate | unfold INR in |- *; ring ].
 Qed.
 
-(**********************************************************)
-(** * Other rules about < and <=                          *)
-(**********************************************************)
-
-Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2.
-Proof.
-  intros x y; intros; apply Rlt_trans with x;
-    [ assumption
-      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
-        assumption ].
-Qed.
-
-Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2.
-Proof.
-  intros x y; intros; apply Rle_lt_trans with x;
-    [ assumption
-      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
-        assumption ].
-Qed.
-
-Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2.
-Proof.
-  intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat;
-    assumption.
-Qed.
-
-Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2.
-Proof.
-  intros x y; intros; apply Rle_trans with x;
-    [ assumption
-      | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
-        assumption ].
-Qed.
-
-Lemma plus_le_is_le : forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3.
-Proof.
-  intros x y z; intros; apply Rle_trans with (x + y);
-    [ pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
-      assumption
-      | assumption ].
-Qed.
-
-Lemma plus_lt_is_lt : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3.
-Proof.
-  intros x y z; intros; apply Rle_lt_trans with (x + y);
-    [ pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
-      assumption
-      | assumption ].
-Qed.
+(*********************************************************)
+(** ** Other rules about < and <=                        *)
+(*********************************************************)
 
-Lemma Rmult_le_0_lt_compat :
+Lemma Rmult_ge_0_gt_0_lt_compat :
   forall r1 r2 r3 r4,
-    0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
+    r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
 Proof.
-  intros; apply Rle_lt_trans with (r2 * r3);
-    [ apply Rmult_le_compat_r; [ assumption | left; assumption ]
-      | apply Rmult_lt_compat_l;
-        [ apply Rle_lt_trans with r1; assumption | assumption ] ].
+  intros; apply Rle_lt_trans with (r2 * r3); auto with real.
 Qed.
 
 Lemma le_epsilon :
@@ -1862,3 +1965,28 @@ Lemma completeness_weak :
 Proof.
   intros; elim (completeness E H H0); intros; split with x; assumption.
 Qed.
+
+(*********************************************************)
+(** * Definitions of new types                           *)
+(*********************************************************)
+
+Record nonnegreal : Type := mknonnegreal
+  {nonneg :> R; cond_nonneg : 0 <= nonneg}.
+
+Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.
+
+Record nonposreal : Type := mknonposreal
+  {nonpos :> R; cond_nonpos : nonpos <= 0}.
+
+Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}.
+
+Record nonzeroreal : Type := mknonzeroreal
+  {nonzero :> R; cond_nonzero : nonzero <> 0}.
+
+(** Compatibility *)
+
+Notation prod_neq_R0 := Rmult_integral_contrapositive_currified (only parsing).
+Notation minus_Rgt := Rminus_gt (only parsing).
+Notation minus_Rge := Rminus_ge (only parsing).
+Notation plus_le_is_le := Rplus_le_reg_pos_r (only parsing).
+Notation plus_lt_is_lt := Rplus_lt_reg_pos_r (only parsing).
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 3447aa0e4..63b8928fb 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -22,6 +22,8 @@ Delimit Scope R_scope with R.
 (* Automatically open scope R_scope for arguments of type R *)
 Bind Scope R_scope with R.
 
+Open Local Scope R_scope.
+
 Parameter R0 : R.
 Parameter R1 : R.
 Parameter Rplus : R -> R -> R.
@@ -38,33 +40,33 @@ Notation "/ x" := (Rinv x) : R_scope.
 
 Infix "<" := Rlt : R_scope.
 
-(*i*******************************************************i*)
+(***********************************************************)
 
 (**********)
-Definition Rgt (r1 r2:R) : Prop := (r2 < r1)%R.
+Definition Rgt (r1 r2:R) : Prop := r2 < r1.
 
 (**********)
-Definition Rle (r1 r2:R) : Prop := (r1 < r2)%R \/ r1 = r2.
+Definition Rle (r1 r2:R) : Prop := r1 < r2 \/ r1 = r2.
 
 (**********)
 Definition Rge (r1 r2:R) : Prop := Rgt r1 r2 \/ r1 = r2.
 
 (**********)
-Definition Rminus (r1 r2:R) : R := (r1 + - r2)%R.
+Definition Rminus (r1 r2:R) : R := r1 + - r2.
 
 (**********)
-Definition Rdiv (r1 r2:R) : R := (r1 * / r2)%R.
+Definition Rdiv (r1 r2:R) : R := r1 * / r2.
 
 (**********)
 
 Infix "-" := Rminus : R_scope.
-Infix "/" := Rdiv : R_scope.
+Infix "/" := Rdiv   : R_scope.
 
 Infix "<=" := Rle : R_scope.
 Infix ">=" := Rge : R_scope.
-Infix ">" := Rgt : R_scope.
+Infix ">"  := Rgt : R_scope.
 
-Notation "x <= y <= z" := ((x <= y)%R /\ (y <= z)%R) : R_scope.
-Notation "x <= y < z" := ((x <= y)%R /\ (y < z)%R) : R_scope.
-Notation "x < y < z" := ((x < y)%R /\ (y < z)%R) : R_scope.
-Notation "x < y <= z" := ((x < y)%R /\ (y <= z)%R) : R_scope.
+Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope.
+Notation "x <= y < z"  := (x <= y /\ y <  z) : R_scope.
+Notation "x < y < z"   := (x <  y /\ y <  z) : R_scope.
+Notation "x < y <= z"  := (x <  y /\ y <= z) : R_scope.