Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.

21 files changed, 107 insertions, 104 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 13b333010..38e9bf7f4 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -68,7 +68,7 @@ Proof.
   pattern 2 at 3; rewrite <- Rmult_1_r; rewrite <- (Rmult_comm 2);
     apply Rmult_le_compat_l.
   left; prove_sup0.
-  left; apply Rplus_lt_reg_r with ((/ 2) ^ S (x1 - S x)).
+  left; apply Rplus_lt_reg_l with ((/ 2) ^ S (x1 - S x)).
   replace ((/ 2) ^ S (x1 - S x) + (1 - (/ 2) ^ S (x1 - S x))) with 1;
     [ idtac | ring ].
   rewrite <- (Rplus_comm 1); pattern 1 at 1; rewrite <- Rplus_0_r;
@@ -315,7 +315,7 @@ Proof.
   intro; unfold Wn; unfold Rdiv; rewrite <- (Rmult_0_r (/ 2));
     rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l.
   apply Rinv_0_lt_compat; prove_sup0.
-  apply Rplus_lt_reg_r with (An n); rewrite Rplus_0_r; unfold Rminus;
+  apply Rplus_lt_reg_l with (An n); rewrite Rplus_0_r; unfold Rminus;
     rewrite (Rplus_comm (An n)); rewrite Rplus_assoc;
       rewrite Rplus_opp_l; rewrite Rplus_0_r;
 	apply Rle_lt_trans with (Rabs (An n)).
@@ -325,7 +325,7 @@ Proof.
   intro; unfold Vn; unfold Rdiv; rewrite <- (Rmult_0_r (/ 2));
     rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l.
   apply Rinv_0_lt_compat; prove_sup0.
-  apply Rplus_lt_reg_r with (- An n); rewrite Rplus_0_r; unfold Rminus;
+  apply Rplus_lt_reg_l with (- An n); rewrite Rplus_0_r; unfold Rminus;
     rewrite (Rplus_comm (- An n)); rewrite Rplus_assoc;
       rewrite Rplus_opp_r; rewrite Rplus_0_r;
 	apply Rle_lt_trans with (Rabs (An n)).
@@ -443,14 +443,14 @@ Proof.
   apply tech1.
   intros; apply H.
   apply Rmult_lt_0_compat.
-  apply Rinv_0_lt_compat; apply Rplus_lt_reg_r with x; rewrite Rplus_0_r;
+  apply Rinv_0_lt_compat; apply Rplus_lt_reg_l with x; rewrite Rplus_0_r;
     replace (x + (1 - x)) with 1; [ elim H3; intros; assumption | ring ].
   apply H.
   symmetry ; apply tech2; assumption.
   rewrite b; pattern (sum_f_R0 An x0) at 1; rewrite <- Rplus_0_r;
     apply Rplus_le_compat_l.
   left; apply Rmult_lt_0_compat.
-  apply Rinv_0_lt_compat; apply Rplus_lt_reg_r with x; rewrite Rplus_0_r;
+  apply Rinv_0_lt_compat; apply Rplus_lt_reg_l with x; rewrite Rplus_0_r;
     replace (x + (1 - x)) with 1; [ elim H3; intros; assumption | ring ].
   apply H.
   replace (sum_f_R0 An x2) with
@@ -466,7 +466,7 @@ Proof.
   left; apply H.
   rewrite tech3.
   unfold Rdiv; apply Rmult_le_reg_l with (1 - x).
-  apply Rplus_lt_reg_r with x; rewrite Rplus_0_r.
+  apply Rplus_lt_reg_l with x; rewrite Rplus_0_r.
   replace (x + (1 - x)) with 1; [ elim H3; intros; assumption | ring ].
   do 2 rewrite (Rmult_comm (1 - x)).
   rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index 69f297817..cb3c762cd 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -442,7 +442,7 @@ Proof.
   unfold Rdiv in H;
     apply Rlt_le_trans with (sum_f_R0 (tg_alt PI_tg) (S (2 * 0))).
   simpl; unfold tg_alt; simpl; rewrite Rmult_1_l;
-    rewrite Rmult_1_r; apply Rplus_lt_reg_r with (PI_tg 1).
+    rewrite Rmult_1_r; apply Rplus_lt_reg_l with (PI_tg 1).
   rewrite Rplus_0_r;
     replace (PI_tg 1 + (PI_tg 0 + -1 * PI_tg 1)) with (PI_tg 0);
       [ unfold PI_tg | ring ].
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index c817bdfa4..a9beba23c 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -132,7 +132,7 @@ Proof.
     rewrite <- Ropp_inv_permute; [ idtac | assumption ].
   rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse;
     rewrite <- Rinv_r_sym; [ rewrite Rmult_1_r | assumption ];
-      apply Rplus_lt_reg_r with (IZR (up (x / - y)) - 1).
+      apply Rplus_lt_reg_l with (IZR (up (x / - y)) - 1).
   replace (IZR (up (x / - y)) - 1 + 1) with (IZR (up (x / - y)));
     [ idtac | ring ].
   replace (IZR (up (x / - y)) - 1 + (- (x * / y) + - (IZR (up (x / - y)) - 1)))
@@ -162,7 +162,7 @@ Proof.
   rewrite <- (Rinv_l_sym _ H); rewrite (Rmult_comm (/ y));
     rewrite Rmult_plus_distr_r; rewrite Rmult_assoc; rewrite <- Rinv_r_sym;
       [ rewrite Rmult_1_r | assumption ];
-      apply Rplus_lt_reg_r with (IZR (up (x / y)) - 1);
+      apply Rplus_lt_reg_l with (IZR (up (x / y)) - 1);
 	replace (IZR (up (x / y)) - 1 + 1) with (IZR (up (x / y)));
 	  [ idtac | ring ];
 	  replace (IZR (up (x / y)) - 1 + (x * / y + (1 - IZR (up (x / y))))) with
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index 2ee22b6de..5cada6c5f 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -412,7 +412,7 @@ Proof.
   intros.
   unfold strict_increasing.
   intros.
-  apply Rplus_lt_reg_r with (- f x).
+  apply Rplus_lt_reg_l with (- f x).
   rewrite Rplus_opp_l; rewrite Rplus_comm.
   assert (H1 := MVT_cor1 f _ _ pr H0).
   elim H1; intros.
@@ -421,7 +421,7 @@ Proof.
   rewrite H3.
   apply Rmult_lt_0_compat.
   apply H.
-  apply Rplus_lt_reg_r with x.
+  apply Rplus_lt_reg_l with x.
   rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ].
 Qed.
 
@@ -517,7 +517,7 @@ Lemma derive_increasing_interv_ax :
 Proof.
   intros.
   split; intros.
-  apply Rplus_lt_reg_r with (- f x).
+  apply Rplus_lt_reg_l with (- f x).
   rewrite Rplus_opp_l; rewrite Rplus_comm.
   assert (H4 := MVT_cor1 f _ _ pr H3).
   elim H4; intros.
@@ -532,7 +532,7 @@ Proof.
   apply Rle_lt_trans with x; assumption.
   elim H2; intros.
   apply Rlt_le_trans with y; assumption.
-  apply Rplus_lt_reg_r with x.
+  apply Rplus_lt_reg_l with x.
   rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ].
   apply Rplus_le_reg_l with (- f x).
   rewrite Rplus_opp_l; rewrite Rplus_comm.
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index 67e353eea..f67659b5b 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -393,7 +393,7 @@ Proof.
   case (Rle_dec (x + h) b); intro.
   cut (b < x + h).
   intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 H14)).
-  apply Rplus_lt_reg_r with (- h - b); replace (- h - b + b) with (- h);
+  apply Rplus_lt_reg_l with (- h - b); replace (- h - b + b) with (- h);
     [ idtac | ring ]; replace (- h - b + (x + h)) with (x - b);
     [ idtac | ring ]; apply Rle_lt_trans with (Rabs h).
   rewrite <- Rabs_Ropp; apply RRle_abs.
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v
index d4d91137e..1982d2dc8 100644
--- a/theories/Reals/PSeries_reg.v
+++ b/theories/Reals/PSeries_reg.v
@@ -153,7 +153,7 @@ Proof.
   unfold Boule; replace (y + h - x) with (h + (y - x));
     [ idtac | ring ]; apply Rle_lt_trans with (Rabs h + Rabs (y - x)).
   apply Rabs_triang.
-  apply Rplus_lt_reg_r with (- Rabs (x - y)).
+  apply Rplus_lt_reg_l with (- Rabs (x - y)).
   rewrite <- (Rabs_Ropp (y - x)); rewrite Ropp_minus_distr'.
   replace (- Rabs (x - y) + r) with (r - Rabs (x - y)).
   replace (- Rabs (x - y) + (Rabs h + Rabs (x - y))) with (Rabs h).
@@ -161,7 +161,7 @@ Proof.
   ring.
   ring.
   unfold Boule in H1; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr';
-    apply Rplus_lt_reg_r with (Rabs (y - x)).
+    apply Rplus_lt_reg_l with (Rabs (y - x)).
   rewrite Rplus_0_r; replace (Rabs (y - x) + (r - Rabs (y - x))) with (pos r);
     [ apply H1 | ring ].
 Qed.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index d765cf787..59e52fe3a 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -522,7 +522,7 @@ Proof.
   intro; unfold R_dist in H5; rewrite Rabs_right in H5.
   cut (sum_f_R0 An N0 < l1).
   intro; elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H7 H6)).
-  apply Rplus_lt_reg_r with (- l).
+  apply Rplus_lt_reg_l with (- l).
   do 2 rewrite (Rplus_comm (- l)).
   apply H5.
   apply Rle_ge; apply Rplus_le_reg_l with l.
@@ -535,7 +535,7 @@ Proof.
   apply H1.
   unfold ge, N0; apply le_max_r.
   unfold ge, N0; apply le_max_l.
-  apply Rplus_lt_reg_r with l; rewrite Rplus_0_r;
+  apply Rplus_lt_reg_l with l; rewrite Rplus_0_r;
     replace (l + (l1 - l)) with l1; [ apply r | ring ].
   unfold Un_growing; intro; simpl;
     pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r;
@@ -578,7 +578,7 @@ Proof.
   discrR.
   apply (Rminus_lt _ _ r0).
   rewrite (Rabs_right _ r0) in H7.
-  apply Rplus_lt_reg_r with ((Rabs l1 - l2) / 2 - Rabs (SP fn N x)).
+  apply Rplus_lt_reg_l with ((Rabs l1 - l2) / 2 - Rabs (SP fn N x)).
   replace ((Rabs l1 - l2) / 2 - Rabs (SP fn N x) + (Rabs l1 + l2) / 2) with
   (Rabs l1 - Rabs (SP fn N x)).
   unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l;
@@ -597,7 +597,7 @@ Proof.
   rewrite Rmult_1_r; rewrite (Rplus_comm (Rabs l1)); apply Rplus_lt_compat_l;
     apply r.
   discrR.
-  rewrite (Rabs_right _ r0) in H6; apply Rplus_lt_reg_r with (- l2).
+  rewrite (Rabs_right _ r0) in H6; apply Rplus_lt_reg_l with (- l2).
   replace (- l2 + (Rabs l1 + l2) / 2) with ((Rabs l1 - l2) / 2).
   rewrite Rplus_comm; apply H6.
   unfold Rdiv; rewrite <- (Rmult_comm (/ 2));
@@ -610,7 +610,7 @@ Proof.
   apply H4; unfold ge, N; apply le_max_l.
   apply H5; unfold ge, N; apply le_max_r.
   unfold Rdiv; apply Rmult_lt_0_compat.
-  apply Rplus_lt_reg_r with l2.
+  apply Rplus_lt_reg_l with l2.
   rewrite Rplus_0_r; replace (l2 + (Rabs l1 - l2)) with (Rabs l1);
     [ apply r | ring ].
   apply Rinv_0_lt_compat; prove_sup0.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 3adea5a10..2472f4c3c 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -973,7 +973,7 @@ Qed.
 
 (** *** Cancellation *)
 
-Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
+Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
 Proof.
   intros; cut (- r + r + r1 < - r + r + r2).
   rewrite Rplus_opp_l.
@@ -983,10 +983,17 @@ Proof.
     apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H).
 Qed.
 
+Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2.
+Proof.
+  intros.
+  apply (Rplus_lt_reg_l r).
+  now rewrite 2!(Rplus_comm r).
+Qed.
+
 Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
 Proof.
   unfold Rle; intros; elim H; intro.
-  left; apply (Rplus_lt_reg_r r r1 r2 H0).
+  left; apply (Rplus_lt_reg_l r r1 r2 H0).
   right; apply (Rplus_eq_reg_l r r1 r2 H0).
 Qed.
 
@@ -999,7 +1006,7 @@ Qed.
 
 Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2.
 Proof.
-  unfold Rgt; intros; apply (Rplus_lt_reg_r r r2 r1 H).
+  unfold Rgt; intros; apply (Rplus_lt_reg_l r r2 r1 H).
 Qed.
 
 Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2.
@@ -1051,12 +1058,10 @@ Qed.
 Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
 Proof.
   unfold Rgt; intros.
-  apply (Rplus_lt_reg_r (r2 + r1)).
-  replace (r2 + r1 + - r1) with r2.
-  replace (r2 + r1 + - r2) with r1.
-  trivial.
-  ring.
-  ring.
+  apply (Rplus_lt_reg_l (r2 + r1)).
+  replace (r2 + r1 + - r1) with r2 by ring.
+  replace (r2 + r1 + - r2) with r1 by ring.
+  exact H.
 Qed.
 Hint Resolve Ropp_gt_lt_contravar.
 
@@ -1328,19 +1333,17 @@ Qed.
 
 Lemma Rlt_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.
+  intros; apply (Rplus_lt_reg_l r2).
+  replace (r2 + (r1 - r2)) with r1 by ring.
+  now rewrite Rplus_0_r.
 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.
+  intros; apply (Rplus_lt_reg_l r2).
+  replace (r2 + (r1 - r2)) with r1 by ring.
+  now rewrite Rplus_0_r.
 Qed.
 
 (**********)
@@ -1629,7 +1632,7 @@ Proof.
     apply (Rlt_irrefl 0); auto.
   do 2 rewrite S_INR in H1; cut (INR n1 < INR n0).
   intro H2; generalize (H0 n0 H2); intro; auto with arith.
-  apply (Rplus_lt_reg_r 1 (INR n1) (INR n0)).
+  apply (Rplus_lt_reg_l 1 (INR n1) (INR n0)).
   rewrite Rplus_comm; rewrite (Rplus_comm 1 (INR n0)); trivial.
 Qed.
 Hint Resolve INR_lt: real.
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 2f54ee94b..5cdb39dd6 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -1555,7 +1555,7 @@ Proof.
       [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ].
   unfold Rdiv; rewrite <- Ropp_mult_distr_l_reverse;
     apply Rmult_lt_0_compat.
-  apply Rplus_lt_reg_r with l.
+  apply Rplus_lt_reg_l with l.
   unfold Rminus; rewrite Rplus_opp_r; rewrite Rplus_0_r; assumption.
   apply Rinv_0_lt_compat; prove_sup0.
 Qed.
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index 5eaf5a575..84fd462d3 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -731,7 +731,7 @@ Proof.
   rewrite <- (Rabs_Ropp (f2 a - f2 x)) in H6.
   rewrite Ropp_minus_distr in H6.
   assert (H7 := Rle_lt_trans _ _ _ (Rabs_triang_inv _ _) H6).
-  apply Rplus_lt_reg_r with (- Rabs (f2 a) + Rabs (f2 x) / 2).
+  apply Rplus_lt_reg_l with (- Rabs (f2 a) + Rabs (f2 x) / 2).
   rewrite Rplus_assoc.
   rewrite <- double_var.
   do 2 rewrite (Rplus_comm (- Rabs (f2 a))).
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index 00c07592e..45c79af48 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -119,7 +119,7 @@ Proof.
   apply Rle_ge.
   case (Rcase_abs h); intro.
   rewrite (Rabs_left h r) in H2.
-  left; rewrite Rplus_comm; apply Rplus_lt_reg_r with (- h); rewrite Rplus_0_r;
+  left; rewrite Rplus_comm; apply Rplus_lt_reg_l with (- h); rewrite Rplus_0_r;
     rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
       apply H2.
   apply Rplus_le_le_0_compat.
@@ -151,7 +151,7 @@ Proof.
   apply H1.
   apply Ropp_0_gt_lt_contravar; apply r.
   rewrite (Rabs_right h r) in H3.
-  apply Rplus_lt_reg_r with (- x); rewrite Rplus_0_r; rewrite <- Rplus_assoc;
+  apply Rplus_lt_reg_l with (- x); rewrite Rplus_0_r; rewrite <- Rplus_assoc;
     rewrite Rplus_opp_l; rewrite Rplus_0_l; apply H3.
   apply H.
   apply Ropp_0_gt_lt_contravar; apply H.
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index c8a2e1a83..ba19e0a53 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -375,7 +375,7 @@ intros. (* f x y f_cont_interv x_lt_y fx_neg fy_pos.*)
   rewrite Rabs_right in H11.
   pattern (- f x0) at 1 in H11; rewrite <- Rplus_0_r in H11.
   unfold Rminus in H11; rewrite (Rplus_comm (f (Wn x2))) in H11.
-  assert (H12 := Rplus_lt_reg_r _ _ _ H11).
+  assert (H12 := Rplus_lt_reg_l _ _ _ H11).
   assert (H13 := H6 x2).
   elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H12)).
   apply Rle_ge; left; unfold Rminus in |- *; apply Rplus_le_lt_0_compat.
@@ -398,14 +398,14 @@ intros. (* f x y f_cont_interv x_lt_y fx_neg fy_pos.*)
   pattern (f x0) at 2 in H10; rewrite <- Rplus_0_r in H10.
   rewrite Ropp_minus_distr' in H10.
   unfold Rminus in H10.
-  assert (H11 := Rplus_lt_reg_r _ _ _ H10).
+  assert (H11 := Rplus_lt_reg_l _ _ _ H10).
   assert (H12 := H6 x2).
   cut (0 < f (Vn x2)).
   intro.
   elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H13 H12)).
   rewrite <- (Ropp_involutive (f (Vn x2))).
   apply Ropp_0_gt_lt_contravar; assumption.
-  apply Rplus_lt_reg_r with (f x0 - f (Vn x2)).
+  apply Rplus_lt_reg_l with (f x0 - f (Vn x2)).
   rewrite Rplus_0_r; replace (f x0 - f (Vn x2) + (f (Vn x2) - f x0)) with 0;
     [ unfold Rminus in |- *; apply Rplus_lt_le_0_compat | ring ].
   assumption.
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 3fe3694f9..87f5c8e26 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -725,7 +725,7 @@ Proof.
     elim (lt_n_O _ H9).
   unfold co_interval in H10; elim H10; clear H10; intros; rewrite Rabs_right.
   rewrite SubEqui_P5 in H9; simpl in H9; inversion H9.
-  apply Rplus_lt_reg_r with (pos_Rl (SubEqui del H) (max_N del H)).
+  apply Rplus_lt_reg_l with (pos_Rl (SubEqui del H) (max_N del H)).
   replace
   (pos_Rl (SubEqui del H) (max_N del H) +
     (t - pos_Rl (SubEqui del H) (max_N del H))) with t;
@@ -739,7 +739,7 @@ Proof.
   unfold max_N; case (maxN del H); intros; elim a0; clear a0;
     intros _ H13; replace (a + INR x * del + del) with (a + INR (S x) * del);
       [ assumption | rewrite S_INR; ring ].
-  apply Rplus_lt_reg_r with (pos_Rl (SubEqui del H) I);
+  apply Rplus_lt_reg_l with (pos_Rl (SubEqui del H) I);
     replace (pos_Rl (SubEqui del H) I + (t - pos_Rl (SubEqui del H) I)) with t;
     [ idtac | ring ];
     replace (pos_Rl (SubEqui del H) I + del) with (pos_Rl (SubEqui del H) (S I)).
@@ -768,7 +768,7 @@ Proof.
   unfold max_N; case (maxN del H); intros; apply INR_lt;
     apply Rmult_lt_reg_l with (pos del).
   apply (cond_pos del).
-  apply Rplus_lt_reg_r with a; do 2 rewrite (Rmult_comm del);
+  apply Rplus_lt_reg_l with a; do 2 rewrite (Rmult_comm del);
     apply Rle_lt_trans with t0; unfold I in H5; try assumption;
       elim a0; intros; apply Rlt_le_trans with b; try assumption;
         elim H8; intros.
@@ -1583,7 +1583,7 @@ Proof.
     set (N := max x x0); cut (Vn N < Un N).
   intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (H N) H4)).
   apply Rlt_trans with ((l1 + l2) / 2).
-  apply Rplus_lt_reg_r with (- l2);
+  apply Rplus_lt_reg_l with (- l2);
     replace (- l2 + (l1 + l2) / 2) with ((l1 - l2) / 2).
   rewrite Rplus_comm; apply Rle_lt_trans with (Rabs (Vn N - l2)).
   apply RRle_abs.
@@ -1594,7 +1594,7 @@ Proof.
         repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym;
           [ ring | discrR ]
       | discrR ].
-  apply Ropp_lt_cancel; apply Rplus_lt_reg_r with l1;
+  apply Ropp_lt_cancel; apply Rplus_lt_reg_l with l1;
     replace (l1 + - ((l1 + l2) / 2)) with ((l1 - l2) / 2).
   apply Rle_lt_trans with (Rabs (Un N - l1)).
   rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs.
@@ -2683,7 +2683,7 @@ Proof.
   repeat split.
   assumption.
   rewrite Rabs_right.
-  apply Rplus_lt_reg_r with x; replace (x + (x1 - x)) with x1; [ idtac | ring ].
+  apply Rplus_lt_reg_l with x; replace (x + (x1 - x)) with x1; [ idtac | ring ].
   apply Rlt_le_trans with (x + h0).
   elim H8; intros; assumption.
   apply Rplus_le_compat_l; apply Rle_trans with del.
@@ -2706,7 +2706,7 @@ Proof.
   assumption.
   apply Rle_ge; left; apply Rinv_0_lt_compat.
   elim r; intro.
-  apply Rplus_lt_reg_r with x; rewrite Rplus_0_r; assumption.
+  apply Rplus_lt_reg_l with x; rewrite Rplus_0_r; assumption.
   elim H5; symmetry ; apply Rplus_eq_reg_l with x; rewrite Rplus_0_r;
     assumption.
   apply Rle_lt_trans with
@@ -2746,7 +2746,7 @@ Proof.
   repeat split.
   assumption.
   rewrite Rabs_left.
-  apply Rplus_lt_reg_r with (x1 - x0); replace (x1 - x0 + x0) with x1;
+  apply Rplus_lt_reg_l with (x1 - x0); replace (x1 - x0 + x0) with x1;
     [ idtac | ring ].
   replace (x1 - x0 + - (x1 - x)) with (x - x0); [ idtac | ring ].
   apply Rle_lt_trans with (x + h0).
@@ -2756,7 +2756,7 @@ Proof.
   apply Rle_trans with del;
     [ left; assumption | unfold del; apply Rmin_l ].
   elim H8; intros; assumption.
-  apply Rplus_lt_reg_r with x; rewrite Rplus_0_r;
+  apply Rplus_lt_reg_l with x; rewrite Rplus_0_r;
     replace (x + (x1 - x)) with x1; [ elim H8; intros; assumption | ring ].
   unfold fct_cte; ring.
   rewrite RiemannInt_P15.
@@ -2776,7 +2776,7 @@ Proof.
   apply Rinv_lt_0_compat.
   assert (H8 : x + h0 < x).
   auto with real.
-  apply Rplus_lt_reg_r with x; rewrite Rplus_0_r; assumption.
+  apply Rplus_lt_reg_l with x; rewrite Rplus_0_r; assumption.
   rewrite
     (RiemannInt_P13 H7 (RiemannInt_P14 x (x + h0) (f x))
       (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x))))
@@ -2912,7 +2912,7 @@ Proof.
   repeat split.
   assumption.
   rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; rewrite Rabs_right.
-  apply Rplus_lt_reg_r with (x2 - x1);
+  apply Rplus_lt_reg_l with (x2 - x1);
     replace (x2 - x1 + (b - x2)) with (b - x1); [ idtac | ring ].
   replace (x2 - x1 + x1) with x2; [ idtac | ring ].
   apply Rlt_le_trans with (b + h0).
@@ -3095,7 +3095,7 @@ Proof.
   elim H8; intros; left; apply H17; repeat split.
   assumption.
   rewrite Rabs_right.
-  apply Rplus_lt_reg_r with a; replace (a + (x2 - a)) with x2; [ idtac | ring ].
+  apply Rplus_lt_reg_l with a; replace (a + (x2 - a)) with x2; [ idtac | ring ].
   apply Rlt_le_trans with (a + h0).
   elim H14; intros; assumption.
   apply Rplus_le_compat_l; left; apply Rle_lt_trans with (Rabs h0).
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index c5ee828a4..658ffd12f 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -312,7 +312,7 @@ Proof.
   rewrite (Rplus_comm 1 (Rabs l)); unfold Rgt; apply Rle_lt_0_plus_1;
     exact (Rabs_pos l).
   unfold R_dist in H9;
-    apply (Rplus_lt_reg_r (- Rabs l) (Rabs (f x2)) (1 + Rabs l)).
+    apply (Rplus_lt_reg_l (- Rabs l) (Rabs (f x2)) (1 + Rabs l)).
   rewrite <- (Rplus_assoc (- Rabs l) 1 (Rabs l));
     rewrite (Rplus_comm (- Rabs l) 1);
       rewrite (Rplus_assoc 1 (- Rabs l) (Rabs l)); rewrite (Rplus_opp_l (Rabs l));
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 43f326a03..555bdcfab 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -137,7 +137,7 @@ Qed.
 
 Lemma exp_ineq1 : forall x:R, 0 < x -> 1 + x < exp x.
 Proof.
-  intros; apply Rplus_lt_reg_r with (- exp 0); rewrite <- (Rplus_comm (exp x));
+  intros; apply Rplus_lt_reg_l with (- exp 0); rewrite <- (Rplus_comm (exp x));
     assert (H0 := MVT_cor1 exp 0 x derivable_exp H); elim H0;
       intros; elim H1; intros; unfold Rminus in H2; rewrite H2;
         rewrite Ropp_0; rewrite Rplus_0_r;
@@ -313,12 +313,12 @@ Proof.
   red; apply P_Rmin.
   apply Rmult_lt_0_compat.
   assumption.
-  apply Rplus_lt_reg_r with 1.
+  apply Rplus_lt_reg_l with 1.
   rewrite Rplus_0_r; replace (1 + (exp eps - 1)) with (exp eps);
     [ apply H1 | ring ].
   apply Rmult_lt_0_compat.
   assumption.
-  apply Rplus_lt_reg_r with (exp (- eps)).
+  apply Rplus_lt_reg_l with (exp (- eps)).
   rewrite Rplus_0_r; replace (exp (- eps) + (1 - exp (- eps))) with 1;
     [ apply H2 | ring ].
   unfold dist, R_met, R_dist; simpl.
@@ -335,7 +335,7 @@ Proof.
   apply H.
   rewrite Hxyy.
   apply Ropp_lt_cancel.
-  apply Rplus_lt_reg_r with (r := y).
+  apply Rplus_lt_reg_l with (r := y).
   replace (y + - (y * exp (- eps))) with (y * (1 - exp (- eps)));
   [ idtac | ring ].
   replace (y + - x) with (Rabs (x - y)).
@@ -358,7 +358,7 @@ Proof.
   apply Rmult_lt_reg_l with (r := y).
   apply H.
   rewrite Hxyy.
-  apply Rplus_lt_reg_r with (r := - y).
+  apply Rplus_lt_reg_l with (r := - y).
   replace (- y + y * exp eps) with (y * (exp eps - 1)); [ idtac | ring ].
   replace (- y + x) with (Rabs (x - y)).
   apply Rlt_le_trans with (1 := H5); apply Rmin_l.
@@ -619,7 +619,7 @@ Proof.
   unfold Rdiv; apply Rmult_lt_0_compat;
     [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
   rewrite Rabs_left in H7.
-  apply Rplus_lt_reg_r with (- h - x / 2).
+  apply Rplus_lt_reg_l with (- h - x / 2).
   replace (- h - x / 2 + x / 2) with (- h); [ idtac | ring ].
   pattern x at 2; rewrite double_var.
   replace (- h - x / 2 + (x / 2 + x / 2 + h)) with (x / 2); [ apply H7 | ring ].
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 3c10725bd..a5e4f8f7e 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -108,7 +108,7 @@ Section sequence.
     intros n H4.
     unfold R_dist.
     rewrite Rabs_left1, Ropp_minus_distr.
-    apply Rplus_lt_reg_r with (Un n - eps).
+    apply Rplus_lt_reg_l with (Un n - eps).
     apply Rlt_le_trans with (Un N).
     now replace (Un n - eps + (l - Un n)) with (l - eps) by ring.
     replace (Un n - eps + eps) with (Un n) by ring.
@@ -171,7 +171,7 @@ Section sequence.
     rewrite H1.
     apply Rle_trans with (1 := proj2 (Hsum n)).
     apply Rlt_le.
-    apply Rplus_lt_reg_r with ((/2)^n - 1).
+    apply Rplus_lt_reg_l with ((/2)^n - 1).
     now ring_simplify.
     exists 0. now exists O.
 
@@ -202,7 +202,7 @@ Section sequence.
     refine (False_ind _ (Rle_not_lt _ _ (H (l - eps) _) _)).
     intros x (n, H1).
     now rewrite H1.
-    apply Rplus_lt_reg_r with (eps - l).
+    apply Rplus_lt_reg_l with (eps - l).
     now ring_simplify.
 
     assert (Rabs (/2) < 1).
@@ -247,7 +247,7 @@ Section sequence.
     rewrite Hs, Rplus_0_l.
     set (k := (N + (n - N))%nat).
     apply Rlt_le.
-    apply Rplus_lt_reg_r with ((/2)^k - (/2)^N).
+    apply Rplus_lt_reg_l with ((/2)^k - (/2)^N).
     now ring_simplify.
     apply Rle_trans with (sum N).
     rewrite le_plus_minus with (1 := Hn).
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index a6e48f83a..48ed16fd4 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -373,7 +373,7 @@ Proof.
   assumption.
   unfold Rdiv; apply Rmult_lt_0_compat;
     [ assumption | apply Rinv_0_lt_compat; assumption ].
-  apply Rplus_lt_reg_r with x; rewrite Rplus_0_r.
+  apply Rplus_lt_reg_l with x; rewrite Rplus_0_r.
   replace (x + (y - x)) with y; [ assumption | ring ].
   exists 0%nat; intros.
   replace (dicho_lb x y P n - dicho_up x y P n - 0) with
@@ -559,7 +559,7 @@ Proof.
   rewrite Rabs_right in H11.
   pattern (- f x0) at 1 in H11; rewrite <- Rplus_0_r in H11.
   unfold Rminus in H11; rewrite (Rplus_comm (f (Wn x2))) in H11.
-  assert (H12 := Rplus_lt_reg_r _ _ _ H11).
+  assert (H12 := Rplus_lt_reg_l _ _ _ H11).
   assert (H13 := H6 x2).
   elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H12)).
   apply Rle_ge; left; unfold Rminus; apply Rplus_le_lt_0_compat.
@@ -580,14 +580,14 @@ Proof.
   pattern (f x0) at 2 in H10; rewrite <- Rplus_0_r in H10.
   rewrite Ropp_minus_distr' in H10.
   unfold Rminus in H10.
-  assert (H11 := Rplus_lt_reg_r _ _ _ H10).
+  assert (H11 := Rplus_lt_reg_l _ _ _ H10).
   assert (H12 := H6 x2).
   cut (0 < f (Vn x2)).
   intro.
   elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H13 H12)).
   rewrite <- (Ropp_involutive (f (Vn x2))).
   apply Ropp_0_gt_lt_contravar; assumption.
-  apply Rplus_lt_reg_r with (f x0 - f (Vn x2)).
+  apply Rplus_lt_reg_l with (f x0 - f (Vn x2)).
   rewrite Rplus_0_r; replace (f x0 - f (Vn x2) + (f (Vn x2) - f x0)) with 0;
     [ unfold Rminus; apply Rplus_lt_le_0_compat | ring ].
   assumption.
@@ -635,7 +635,7 @@ Proof.
   apply Ropp_eq_0_compat; assumption.
   unfold opp_fct; apply Ropp_0_gt_lt_contravar; assumption.
   unfold opp_fct.
-  apply Rplus_lt_reg_r with (f x); rewrite Rplus_opp_r; rewrite Rplus_0_r;
+  apply Rplus_lt_reg_l with (f x); rewrite Rplus_opp_r; rewrite Rplus_0_r;
     assumption.
   inversion H0.
   assumption.
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v
index 51d0b99ed..f05539379 100644
--- a/theories/Reals/Rtopology.v
+++ b/theories/Reals/Rtopology.v
@@ -84,7 +84,7 @@ Proof.
     apply H4.
   unfold del; rewrite <- (Rabs_Ropp (x - x1)); rewrite Ropp_minus_distr;
     ring.
-  unfold del; apply Rplus_lt_reg_r with (Rabs (x - x1));
+  unfold del; apply Rplus_lt_reg_l with (Rabs (x - x1));
     rewrite Rplus_0_r;
       replace (Rabs (x - x1) + (x0 - Rabs (x - x1))) with (pos x0);
       [ idtac | ring ].
@@ -139,7 +139,7 @@ Proof.
     apply H10.
   unfold del; simpl; rewrite <- (Rabs_Ropp (x - x1));
     rewrite Ropp_minus_distr; ring.
-  apply Rplus_lt_reg_r with (Rabs (x - x1)); rewrite Rplus_0_r;
+  apply Rplus_lt_reg_l with (Rabs (x - x1)); rewrite Rplus_0_r;
     replace (Rabs (x - x1) + (x0 - Rabs (x - x1))) with (pos x0);
     [ rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H6 | ring ].
 Qed.
@@ -254,7 +254,7 @@ Proof.
   apply H4.
   unfold del2; simpl; rewrite <- (Rabs_Ropp (x - x0));
     rewrite Ropp_minus_distr; ring.
-  apply Rplus_lt_reg_r with (Rabs (x - x0)); rewrite Rplus_0_r;
+  apply Rplus_lt_reg_l with (Rabs (x - x0)); rewrite Rplus_0_r;
     replace (Rabs (x - x0) + (del - Rabs (x - x0))) with (pos del);
     [ rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H2 | ring ].
   apply interior_P1.
@@ -664,7 +664,7 @@ Proof.
   apply Rlt_trans with (b - x).
   unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_gt_contravar;
     auto with real.
-  elim H10; intros H15 _; apply Rplus_lt_reg_r with (x - eps);
+  elim H10; intros H15 _; apply Rplus_lt_reg_l with (x - eps);
     replace (x - eps + (b - x)) with (b - eps);
     [ replace (x - eps + eps) with x; [ apply H15 | ring ] | ring ].
   apply Rge_minus; apply Rle_ge; elim H14; intros _ H15; apply H15.
@@ -734,7 +734,7 @@ Proof.
   rewrite Ropp_minus_distr; apply Rlt_trans with (m - x).
   unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_gt_contravar;
     auto with real.
-  apply Rplus_lt_reg_r with (x - eps);
+  apply Rplus_lt_reg_l with (x - eps);
     replace (x - eps + (m - x)) with (m - eps).
   replace (x - eps + eps) with x.
   elim H10; intros; assumption.
@@ -743,7 +743,7 @@ Proof.
   apply Rle_lt_trans with (m' - m).
   unfold Rminus; do 2 rewrite <- (Rplus_comm (- m));
     apply Rplus_le_compat_l; elim H14; intros; assumption.
-  apply Rplus_lt_reg_r with m; replace (m + (m' - m)) with m'.
+  apply Rplus_lt_reg_l with m; replace (m + (m' - m)) with m'.
   apply Rle_lt_trans with (m + eps / 2).
   unfold m'; apply Rmin_l.
   apply Rplus_lt_compat_l; apply Rmult_lt_reg_l with 2.
@@ -984,7 +984,7 @@ Qed.
 
 Lemma Rlt_Rminus : forall a b:R, a < b -> 0 < b - a.
 Proof.
-  intros; apply Rplus_lt_reg_r with a; rewrite Rplus_0_r;
+  intros; apply Rplus_lt_reg_l with a; rewrite Rplus_0_r;
     replace (a + (b - a)) with b; [ assumption | ring ].
 Qed.
 
@@ -1020,7 +1020,7 @@ Proof.
   case (Rle_dec x a); intro.
   case (Rle_dec x0 a); intro.
   unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption.
-  elim n; left; apply Rplus_lt_reg_r with (- x);
+  elim n; left; apply Rplus_lt_reg_l with (- x);
     do 2 rewrite (Rplus_comm (- x)); apply Rle_lt_trans with (Rabs (x0 - x)).
   apply RRle_abs.
   assumption.
@@ -1052,7 +1052,7 @@ Proof.
   apply Rmin_l.
   elim n0; left; assumption.
   elim n; right; assumption.
-  apply Rplus_lt_reg_r with (- a); do 2 rewrite (Rplus_comm (- a));
+  apply Rplus_lt_reg_l with (- a); do 2 rewrite (Rplus_comm (- a));
     rewrite H4 in H9; apply Rle_lt_trans with (Rabs (x1 - a)).
   apply RRle_abs.
   apply Rlt_le_trans with (Rmin x0 (b - a)).
@@ -1096,7 +1096,7 @@ Proof.
   elim n1; left; assumption.
   elim n0; left; assumption.
   split.
-  apply Ropp_lt_cancel; apply Rplus_lt_reg_r with x;
+  apply Ropp_lt_cancel; apply Rplus_lt_reg_l with x;
     apply Rle_lt_trans with (Rabs (x1 - x)).
   rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs.
   apply Rlt_le_trans with (Rmin x0 (Rmin (x - a) (b - x))).
@@ -1104,7 +1104,7 @@ Proof.
   apply Rle_trans with (Rmin (x - a) (b - x)).
   apply Rmin_r.
   apply Rmin_l.
-  apply Rplus_lt_reg_r with (- x); do 2 rewrite (Rplus_comm (- x));
+  apply Rplus_lt_reg_l with (- x); do 2 rewrite (Rplus_comm (- x));
     apply Rle_lt_trans with (Rabs (x1 - x)).
   apply RRle_abs.
   apply Rlt_le_trans with (Rmin x0 (Rmin (x - a) (b - x))).
@@ -1143,7 +1143,7 @@ Proof.
   rewrite H6; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0;
     assumption.
   elim n1; right; assumption.
-  rewrite H6 in H11; apply Ropp_lt_cancel; apply Rplus_lt_reg_r with b;
+  rewrite H6 in H11; apply Ropp_lt_cancel; apply Rplus_lt_reg_l with b;
     apply Rle_lt_trans with (Rabs (x1 - b)).
   rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs.
   apply Rlt_le_trans with (Rmin x0 (b - a)).
@@ -1156,7 +1156,7 @@ Proof.
   change (0 < x - b); apply Rlt_Rminus; assumption.
   intros; elim H8; clear H8; intros.
   assert (H10 : b < x0).
-  apply Ropp_lt_cancel; apply Rplus_lt_reg_r with x;
+  apply Ropp_lt_cancel; apply Rplus_lt_reg_l with x;
     apply Rle_lt_trans with (Rabs (x0 - x)).
   rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs.
   assumption.
@@ -1233,7 +1233,7 @@ Proof.
   apply r.
   elim (H9 x); unfold intersection_domain, disc, image_dir; split.
   rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; rewrite Rabs_right.
-  apply Rplus_lt_reg_r with (x - eps);
+  apply Rplus_lt_reg_l with (x - eps);
     replace (x - eps + (M - x)) with (M - eps).
   replace (x - eps + eps) with x.
   auto with real.
diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v
index 6174ef32c..672eae678 100644
--- a/theories/Reals/Rtrigo1.v
+++ b/theories/Reals/Rtrigo1.v
@@ -670,11 +670,11 @@ Proof.
     replace (Un 0%nat + - Un 1%nat + Un 2%nat + - Un 3%nat) with
     (Un 0%nat - Un 1%nat + (Un 2%nat - Un 3%nat)); [ idtac | ring ].
   apply Rplus_lt_0_compat.
-  unfold Rminus in |- *; apply Rplus_lt_reg_r with (Un 1%nat);
+  unfold Rminus in |- *; apply Rplus_lt_reg_l with (Un 1%nat);
     rewrite Rplus_0_r; rewrite (Rplus_comm (Un 1%nat));
       rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
         apply H1.
-  unfold Rminus in |- *; apply Rplus_lt_reg_r with (Un 3%nat);
+  unfold Rminus in |- *; apply Rplus_lt_reg_l with (Un 3%nat);
     rewrite Rplus_0_r; rewrite (Rplus_comm (Un 3%nat));
       rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
         apply H1.
@@ -722,7 +722,7 @@ Proof.
     unfold INR in |- *.
   replace ((2 * x + 1 + 1 + 1) * (2 * x + 1 + 1)) with (4 * x * x + 10 * x + 6);
   [ idtac | ring ].
-  apply Rplus_lt_reg_r with (-4); rewrite Rplus_opp_l;
+  apply Rplus_lt_reg_l with (-4); rewrite Rplus_opp_l;
     replace (-4 + (4 * x * x + 10 * x + 6)) with (4 * x * x + 10 * x + 2);
     [ idtac | ring ].
   apply Rplus_le_lt_0_compat.
@@ -1201,7 +1201,7 @@ Proof.
   replace (- (PI - x)) with (x - PI).
   replace (- (PI - y)) with (y - PI).
   intros; change (sin (y - PI) < sin (x - PI)) in H8;
-    apply Rplus_lt_reg_r with (- PI); rewrite Rplus_comm;
+    apply Rplus_lt_reg_l with (- PI); rewrite Rplus_comm;
       replace (y + - PI) with (y - PI).
   rewrite Rplus_comm; replace (x + - PI) with (x - PI).
   apply (sin_increasing_0 (y - PI) (x - PI) H4 H5 H6 H7 H8).
@@ -1273,7 +1273,7 @@ Proof.
   replace (-3 * (PI / 2) + 2 * PI) with (PI / 2).
   replace (-3 * (PI / 2) + PI) with (- (PI / 2)).
   clear H1 H2 H3 H4; intros H1 H2 H3 H4;
-    apply Rplus_lt_reg_r with (-3 * (PI / 2));
+    apply Rplus_lt_reg_l with (-3 * (PI / 2));
       replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)).
   replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)).
   apply (sin_increasing_0 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H4 H3 H2 H1 H5).
@@ -1352,7 +1352,7 @@ Proof.
             generalize (Rplus_le_compat_l PI 0 y H1);
               generalize (Rplus_le_compat_l PI y PI H2); rewrite Rplus_0_r.
   rewrite <- double.
-  clear H H0 H1 H2 H3; intros; apply Rplus_lt_reg_r with PI;
+  clear H H0 H1 H2 H3; intros; apply Rplus_lt_reg_l with PI;
     apply (cos_increasing_0 (PI + y) (PI + x) H0 H H2 H1 H4).
 Qed.
 
@@ -1919,7 +1919,7 @@ Proof.
       apply (Rmult_lt_reg_r PI); [apply PI_RGT_0|rewrite Rmult_1_l].
       replace (3*(PI/2)) with (PI/2 + PI) in GT by field.
       rewrite Rplus_comm in GT.
-      now apply Rplus_lt_reg_r in GT. }
+      now apply Rplus_lt_reg_l in GT. }
     omega.
 Qed.
 
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 41e853ccc..5254ff2cc 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -470,7 +470,7 @@ Proof.
   rewrite Rabs_right in H1.
   elim (Rlt_irrefl _ H1).
   left; assumption.
-  apply Rplus_lt_reg_r with x.
+  apply Rplus_lt_reg_l with x.
   rewrite Rplus_0_r; replace (x + (y - x)) with y; [ assumption | ring ].
   assumption.
   cut (0 < x - y).
@@ -479,7 +479,7 @@ Proof.
   rewrite Rabs_right in H1.
   elim (Rlt_irrefl _ H1).
   left; assumption.
-  apply Rplus_lt_reg_r with y.
+  apply Rplus_lt_reg_l with y.
   rewrite Rplus_0_r; replace (y + (x - y)) with x; [ assumption | ring ].
 Qed.
 
@@ -860,7 +860,7 @@ Proof.
   split.
   pattern k at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l.
   unfold Rdiv; apply Rmult_lt_0_compat.
-  apply Rplus_lt_reg_r with k; rewrite Rplus_0_r; replace (k + (1 - k)) with 1;
+  apply Rplus_lt_reg_l with k; rewrite Rplus_0_r; replace (k + (1 - k)) with 1;
     [ elim H; intros; assumption | ring ].
   apply Rinv_0_lt_compat; prove_sup0.
   apply Rmult_lt_reg_l with 2.
@@ -881,12 +881,12 @@ Proof.
     apply Rle_lt_trans with (Rabs (Rabs (An (S n) / An n) - k) + Rabs k).
   apply Rabs_triang.
   rewrite (Rabs_right k).
-  apply Rplus_lt_reg_r with (- k); rewrite <- (Rplus_comm k);
+  apply Rplus_lt_reg_l with (- k); rewrite <- (Rplus_comm k);
     repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l;
       repeat rewrite Rplus_0_l; apply H4.
   apply Rle_ge; elim H; intros; assumption.
   unfold Rdiv; apply Rmult_lt_0_compat.
-  apply Rplus_lt_reg_r with k; rewrite Rplus_0_r; elim H; intros;
+  apply Rplus_lt_reg_l with k; rewrite Rplus_0_r; elim H; intros;
     replace (k + (1 - k)) with 1; [ assumption | ring ].
   apply Rinv_0_lt_compat; prove_sup0.
 Qed.
@@ -916,7 +916,7 @@ Proof.
   apply tech9.
   assumption.
   unfold N; apply le_max_l.
-  apply Rplus_lt_reg_r with l.
+  apply Rplus_lt_reg_l with l.
   rewrite Rplus_0_r.
   replace (l + (Un n - l)) with (Un n); [ assumption | ring ].
 Qed.
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index 89c178213..985faa21e 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -32,7 +32,7 @@ Proof.
   apply H0.
   pattern 1 at 2; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
     assumption.
-  apply Rplus_lt_reg_r with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
+  apply Rplus_lt_reg_l with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
     unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l;
       rewrite Rplus_0_r.
   pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1.
@@ -43,7 +43,7 @@ Proof.
     assumption.
   apply H0.
   left; apply Rlt_0_1.
-  apply Rplus_lt_reg_r with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
+  apply Rplus_lt_reg_l with 1; rewrite Rplus_0_r; rewrite Rplus_comm;
     unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_l;
       rewrite Rplus_0_r.
   pattern 1 at 2; rewrite <- sqrt_1; apply sqrt_lt_1.
@@ -75,7 +75,7 @@ Proof.
     assumption.
   left; apply Rlt_0_1.
   apply H0.
-  apply Rle_ge; left; apply Rplus_lt_reg_r with 1.
+  apply Rle_ge; left; apply Rplus_lt_reg_l with 1.
   rewrite Rplus_0_r; rewrite Rplus_comm; unfold Rminus;
     rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r.
   pattern 1 at 1; rewrite <- sqrt_1; apply sqrt_lt_1.