Change the parser and printer so that they use IZR for real constants.

There are two main issues. First, (-cst)%R is no longer syntactically
equal to (-(cst))%R (though they are still convertible). This breaks some
rewriting rules.

Second, the ring/field_simplify tactics did not know how to refold
real constants. This defect is no longer hidden by the pretty-printer,
which makes these tactics almost unusable on goals containing large
constants.

This commit also modifies the ring/field tactics so that real constant
reification is now constant time rather than linear.

Note that there is now a bit of code duplication between z_syntax and
r_syntax. This should be fixed once plugin interdependencies are supported.

Ideally the r_syntax plugin should just disappear by declaring IZR as a
coercion. Unfortunately the coercion mechanism is not powerful enough yet,
be it for parsing (need the ability for a scope to delegate constant
parsing to another scope) or printing (too many visible coercions left).

24 files changed, 129 insertions, 192 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index a98d529fa..0e1608a32 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -78,7 +78,7 @@ Proof.
   ring.
   discrR.
   discrR.
-  pattern 1 at 3; replace 1 with (/ 1);
+  replace 1 with (/ 1);
     [ apply tech7; discrR | apply Rinv_1 ].
   replace (An (S x)) with (An (S x + 0)%nat).
   apply (tech6 (fun i:nat => An (S x + i)%nat) (/ 2)).
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 7d9fff276..67584f775 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -106,7 +106,7 @@ Proof.
   split.
   ring.
   unfold k0; case (Rcase_abs y) as [Hlt|Hge].
-  assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; change (IZR 1) with 1;
+  assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl;
     unfold Rminus.
   replace (- ((1 + - IZR (up (x / - y))) * y)) with
     ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ].
@@ -140,10 +140,10 @@ Proof.
   rewrite <- Ropp_mult_distr_r_reverse; rewrite (Ropp_inv_permute _ H); elim H0;
     unfold Rdiv; intros H1 _; exact H1.
   apply Ropp_neq_0_compat; assumption.
-  assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; change (IZR 1) with 1;
+  assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; simpl;
     cut (0 < y).
   intro; unfold Rminus;
-    replace (- ((IZR (up (x / y)) + -1) * y)) with ((1 - IZR (up (x / y))) * y);
+    replace (- ((IZR (up (x / y)) + -(1)) * y)) with ((1 - IZR (up (x / y))) * y);
       [ idtac | ring ].
   split.
   apply Rmult_le_reg_l with (/ y).
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 4e2a7c3c6..05911cd53 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -31,9 +31,6 @@ Ltac discrR :=
   try
    match goal with
    |  |- (?X1 <> ?X2) =>
-       change 2 with (IZR 2);
-       change 1 with (IZR 1);
-       change 0 with (IZR 0);
        repeat
          rewrite <- plus_IZR ||
            rewrite <- mult_IZR ||
@@ -52,9 +49,6 @@ Ltac prove_sup0 :=
   end.
 
 Ltac omega_sup :=
-  change 2 with (IZR 2);
-  change 1 with (IZR 1);
-  change 0 with (IZR 0);
   repeat
     rewrite <- plus_IZR ||
       rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
@@ -72,9 +66,6 @@ Ltac prove_sup :=
   end.
 
 Ltac Rcompute :=
-  change 2 with (IZR 2);
-  change 1 with (IZR 1);
-  change 0 with (IZR 0);
   repeat
     rewrite <- plus_IZR ||
       rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 569518f7b..e9de24898 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -439,20 +439,16 @@ Proof.
   repeat rewrite <- Rmult_assoc.
   rewrite <- Rinv_r_sym.
   rewrite Rmult_1_l.
-  replace (INR N * INR N) with (Rsqr (INR N)); [ idtac | reflexivity ].
-  rewrite Rmult_assoc.
-  rewrite Rmult_comm.
-  replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ].
+  change 4 with (Rsqr 2).
   rewrite <- Rsqr_mult.
   apply Rsqr_incr_1.
-  replace 2 with (INR 2).
-  rewrite <- mult_INR; apply H1.
-  reflexivity.
+  change 2 with (INR 2).
+  rewrite Rmult_comm, <- mult_INR; apply H1.
   left; apply lt_INR_0; apply H.
   left; apply Rmult_lt_0_compat.
-  prove_sup0.
   apply lt_INR_0; apply div2_not_R0.
   apply lt_n_S; apply H.
+  now apply IZR_lt.
   cut (1 < S N)%nat.
   intro; unfold Rsqr; apply prod_neq_R0; apply not_O_INR; intro;
     assert (H4 := div2_not_R0 _ H2); rewrite H3 in H4;
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index 19db476fd..2d2385703 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -53,7 +53,7 @@ assert (-(PI/4) <= atan x).
  destruct xm1 as [xm1 | xm1].
   rewrite <- atan_1, <- atan_opp; apply Rlt_le, atan_increasing.
   assumption.
- solve[rewrite <- xm1, atan_opp, atan_1; apply Rle_refl].
+ solve[rewrite <- xm1; change (-1) with (-(1)); rewrite atan_opp, atan_1; apply Rle_refl].
 assert (-(PI/4) < atan y).
  rewrite <- atan_1, <- atan_opp; apply atan_increasing.
  assumption.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 686077327..7cd4c00c7 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1812,7 +1812,7 @@ Qed.
 (**********)
 Lemma succ_IZR : forall n:Z, IZR (Z.succ n) = IZR n + 1.
 Proof.
-  intro; change 1 with (IZR 1); unfold Z.succ; apply plus_IZR.
+  intro; unfold Z.succ; apply plus_IZR.
 Qed.
 
 (**********)
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index d0f9aea28..e9b1762af 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -92,7 +92,7 @@ Proof.
     auto with zarith real.
     (*inf a 1*)
   cut (r - IZR (up r) < 0).
-  rewrite <- Z_R_minus; change (IZR 1) with 1; intro; unfold Rminus;
+  rewrite <- Z_R_minus; simpl; intro; unfold Rminus;
     rewrite Ropp_plus_distr; rewrite <- Rplus_assoc;
       fold (r - IZR (up r)); rewrite Ropp_involutive;
         elim (Rplus_ne 1); intros a b; pattern 1 at 2;
@@ -112,21 +112,12 @@ Lemma base_Int_part :
 Proof.
   intro; unfold Int_part; elim (archimed r); intros.
   split; rewrite <- (Z_R_minus (up r) 1); simpl.
-  generalize (Rle_minus (IZR (up r) - r) 1 H0); intro; unfold Rminus in H1;
-    rewrite (Rplus_assoc (IZR (up r)) (- r) (-1)) in H1;
-      rewrite (Rplus_comm (- r) (-1)) in H1;
-        rewrite <- (Rplus_assoc (IZR (up r)) (-1) (- r)) in H1;
-          fold (IZR (up r) - 1) in H1; fold (IZR (up r) - 1 - r) in H1;
-            apply Rminus_le; auto with zarith real.
-  generalize (Rplus_gt_compat_l (-1) (IZR (up r)) r H); intro;
-    rewrite (Rplus_comm (-1) (IZR (up r))) in H1;
-      generalize (Rplus_gt_compat_l (- r) (IZR (up r) + -1) (-1 + r) H1);
-        intro; clear H H0 H1; rewrite (Rplus_comm (- r) (IZR (up r) + -1)) in H2;
-          fold (IZR (up r) - 1) in H2; fold (IZR (up r) - 1 - r) in H2;
-            rewrite (Rplus_comm (- r) (-1 + r)) in H2;
-              rewrite (Rplus_assoc (-1) r (- r)) in H2; rewrite (Rplus_opp_r r) in H2;
-                elim (Rplus_ne (-1)); intros a b; rewrite a in H2;
-                  clear a b; auto with zarith real.
+  apply Rminus_le.
+  replace (IZR (up r) - 1 - r) with (IZR (up r) - r - 1) by ring.
+  now apply Rle_minus.
+  apply Rminus_gt.
+  replace (IZR (up r) - 1 - r - -1) with (IZR (up r) - r) by ring.
+  now apply Rgt_minus.
 Qed.
 
 (**********)
@@ -240,7 +231,6 @@ Proof.
                                                                                                                   clear a b; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
                                                                                                                     rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H;
                                                                                                                       cut (1 = IZR 1); auto with zarith real.
-  intro; rewrite H1 in H; clear H1;
     rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H;
       generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H);
         intros; clear H H0; unfold Int_part at 1;
@@ -324,12 +314,12 @@ Proof.
                                                                                                       rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H0;
                                                                                                         elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H0;
                                                                                                           clear a b; rewrite <- (Rplus_opp_l 1) in H0;
-                                                                                                            rewrite <- (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2)) (-1) 1)
+                                                                                                            rewrite <- (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2)) (-(1)) 1)
                                                                                                               in H0; fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H0;
                                                                                                                 rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0;
                                                                                                                   rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H;
-                                                                                                                    cut (1 = IZR 1); auto with zarith real.
-  intro; rewrite H1 in H; rewrite H1 in H0; clear H1;
+                                                                                                                    auto with zarith real.
+  change (_ + -1) with (IZR (Int_part r1 - Int_part r2) - 1) in H;
     rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H;
       rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H0;
         rewrite <- (plus_IZR (Int_part r1 - Int_part r2 - 1) 1) in H0;
@@ -376,7 +366,7 @@ Proof.
               rewrite (Ropp_involutive (IZR 1));
                 rewrite (Ropp_involutive (IZR (Int_part r2)));
                   rewrite (Ropp_plus_distr (IZR (Int_part r1)));
-                    rewrite (Ropp_involutive (IZR (Int_part r2))); change (IZR 1) with 1;
+                    rewrite (Ropp_involutive (IZR (Int_part r2))); simpl;
                       rewrite <-
                         (Rplus_assoc (r1 + - r2) (- IZR (Int_part r1) + IZR (Int_part r2)) 1)
                         ; rewrite (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2)));
@@ -442,9 +432,9 @@ Proof.
                                                                 in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0;
                                                                   elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H0;
                                                                     clear a b;
+                                                                      change 2 with (1 + 1) in H0;
                                                                       rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) 1 1) in H0;
-                                                                        cut (1 = IZR 1); auto with zarith real.
-  intro; rewrite H1 in H0; rewrite H1 in H; clear H1;
+                                                                        auto with zarith real.
     rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H;
       rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0;
         rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H;
@@ -509,7 +499,6 @@ Proof.
                                                                     intros a b; rewrite a in H0; clear a b; elim (Rplus_ne (r1 + r2));
                                                                       intros a b; rewrite b in H0; clear a b; cut (1 = IZR 1);
                                                                         auto with zarith real.
-  intro; rewrite H in H1; clear H;
     rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0;
       rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1;
         rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1;
@@ -536,7 +525,7 @@ Proof.
                     rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2)));
                       unfold Rminus;
                         rewrite
-                          (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-1))
+                          (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-(1)))
                           ; rewrite <- (Ropp_plus_distr (IZR (Int_part r1) + IZR (Int_part r2)) 1);
                             trivial with zarith real.
 Qed.
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 5c975c3f5..0c1e0b7e8 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -420,10 +420,10 @@ Proof.
   rewrite (Rmult_comm (/ a)).
   rewrite Rmult_assoc.
   rewrite <- Rinv_mult_distr.
-  replace (2 * (2 * a) * a) with (Rsqr (2 * a)).
+  replace (4 * a * a) with (Rsqr (2 * a)).
   reflexivity.
   ring_Rsqr.
-  rewrite <- Rmult_assoc; apply prod_neq_R0;
+  apply prod_neq_R0;
     [ discrR | apply (cond_nonzero a) ].
   apply (cond_nonzero a).
   assumption.
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index 0254218c4..27cb356a0 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -88,17 +88,11 @@ Proof.
   right; unfold Rdiv.
   repeat rewrite Rabs_mult.
   rewrite Rabs_Rinv; discrR.
-  replace (Rabs 8) with 8.
-  replace 8 with 8; [ idtac | ring ].
-  rewrite Rinv_mult_distr; [ idtac | discrR | discrR ].
-  replace (2 * / Rabs (f2 x) * (Rabs eps * Rabs (f2 x) * (/ 2 * / 4))) with
-  (Rabs eps * / 4 * (2 * / 2) * (Rabs (f2 x) * / Rabs (f2 x)));
-  [ idtac | ring ].
-  replace (Rabs eps) with eps.
-  repeat rewrite <- Rinv_r_sym; try discrR || (apply Rabs_no_R0; assumption).
-  ring.
-  symmetry ; apply Rabs_right; left; assumption.
-  symmetry ; apply Rabs_right; left; prove_sup.
+  rewrite (Rabs_pos_eq 8) by now apply IZR_le.
+  rewrite (Rabs_pos_eq eps).
+  field.
+  now apply Rabs_no_R0.
+  now apply Rlt_le.
 Qed.
 
 Lemma maj_term2 :
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index 4e88714d6..d4597aeba 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -201,8 +201,8 @@ Proof.
   apply Rabs_pos_lt.
   unfold Rdiv, Rsqr; repeat rewrite Rmult_assoc.
   repeat apply prod_neq_R0; try assumption.
-  red; intro; rewrite H15 in H6; elim (Rlt_irrefl _ H6).
-  apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption.
+  now apply Rgt_not_eq.
+  apply Rinv_neq_0_compat; apply prod_neq_R0; [discrR | assumption].
   apply H13.
   split.
   apply D_x_no_cond; assumption.
@@ -213,8 +213,7 @@ Proof.
   red; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6).
   assumption.
   assumption.
-  apply Rinv_neq_0_compat; repeat apply prod_neq_R0;
-    [ discrR | discrR | discrR | assumption ].
+  apply Rinv_neq_0_compat; apply prod_neq_R0; [discrR | assumption].
 (***********************************)
 (*        Third case               *)
 (*     (f1 x)<>0  l1=0  l2=0       *)
@@ -224,11 +223,11 @@ Proof.
   elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x))));
     [ idtac
       | apply Rabs_pos_lt; unfold Rdiv, Rsqr; repeat rewrite Rmult_assoc;
-        repeat apply prod_neq_R0;
+        repeat apply prod_neq_R0 ;
           [ assumption
             | assumption
-            | red; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6)
-            | apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption ] ].
+            | now apply Rgt_not_eq
+            | apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption ] ].
   intros alp_f2d H12.
   cut (0 < Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d)).
   intro.
@@ -295,8 +294,10 @@ Proof.
   elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x))));
     [ idtac
       | apply Rabs_pos_lt; unfold Rsqr, Rdiv;
-        repeat rewrite Rinv_mult_distr; repeat apply prod_neq_R0;
-          try assumption || discrR ].
+        repeat apply prod_neq_R0 ;
+          [ assumption..
+            | now apply Rgt_not_eq
+            | apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption ] ].
   intros alp_f2d H11.
   assert (H12 := derivable_continuous_pt _ _ X).
   unfold continuity_pt in H12.
@@ -380,15 +381,9 @@ Proof.
   repeat apply prod_neq_R0; try assumption.
   red; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6).
   apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
   apply Rinv_neq_0_compat; assumption.
   apply Rinv_neq_0_compat; assumption.
   discrR.
-  discrR.
-  discrR.
-  discrR.
-  discrR.
   apply prod_neq_R0; [ discrR | assumption ].
   elim H13; intros.
   apply H19.
@@ -408,16 +403,9 @@ Proof.
   repeat apply prod_neq_R0; try assumption.
   red; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6).
   apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
   apply Rinv_neq_0_compat; assumption.
   apply Rinv_neq_0_compat; assumption.
   apply prod_neq_R0; [ discrR | assumption ].
-  red; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6).
-  apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; assumption.
 (***********************************)
 (*         Fifth case              *)
 (*    (f1 x)<>0  l1<>0  l2=0       *)
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index d172139f5..f9da88aad 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -249,8 +249,10 @@ assert (Sublemma : forall x y lb ub, lb <= x <= ub /\ lb <= y <= ub -> lb <= (x+
   split.
   replace lb with ((lb + lb) * /2) by field.
   unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
+  now apply Rlt_le, Rinv_0_lt_compat, IZR_lt.
   replace ub with ((ub + ub) * /2) by field.
   unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
+  now apply Rlt_le, Rinv_0_lt_compat, IZR_lt.
 intros x y P N x_lt_y.
 induction N.
  simpl ; intuition.
@@ -1030,6 +1032,7 @@ intros x ub lb lb_lt_x x_lt_ub.
  assert (T : 0 < ub - lb).
   fourier.
  unfold Rdiv ; apply Rlt_mult_inv_pos ; intuition.
+now apply IZR_lt.
 Qed.
 
 Definition mkposreal_lb_ub (x lb ub:R) (lb_lt_x:lb<x) (x_lt_ub:x<ub) : posreal.
@@ -1102,7 +1105,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
     rewrite <- Rmult_1_r ; replace 1 with (derive_pt id c (pr2 c P)) by reg.
     replace (- (fn N (x + h) - fn N x)) with (fn N x - fn N (x + h)) by field.
     assumption.
-   solve[apply Rlt_not_eq ; intuition].
+  now apply Rlt_not_eq, IZR_lt.
   rewrite <- Hc'; clear Hc Hc'.
   replace (derive_pt (fn N) c (pr1 c P)) with (fn' N c).
   replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by field.
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index d9aa6b859..3e5362efe 100644
--- a/theories/Reals/Ratan.v
+++ b/theories/Reals/Ratan.v
@@ -132,7 +132,7 @@ intros [ | N] Npos n decr to0 cv nN.
     unfold Rminus; apply Rplus_le_compat_l, Ropp_le_contravar.
     solve[apply Rge_le, (growing_prop _ _ _ (CV_ALT_step0 f decr) dist)].
    unfold Rminus; rewrite tech5, Ropp_plus_distr, <- Rplus_assoc.
-   unfold tg_alt at 2; rewrite pow_1_odd, Ropp_mult_distr_l_reverse; fourier.
+   unfold tg_alt at 2; rewrite pow_1_odd; fourier.
  rewrite Nodd; destruct (alternated_series_ineq _ _ p decr to0 cv) as [B _].
  destruct (alternated_series_ineq _ _ (S p) decr to0 cv) as [_ C].
  assert (keep : (2 * S p = S (S ( 2 * p)))%nat) by ring.
@@ -161,7 +161,6 @@ clear WLOG; intros Hyp [ | n] decr to0 cv _.
  generalize (alternated_series_ineq f l 0 decr to0 cv).
  unfold R_dist, tg_alt; simpl; rewrite !Rmult_1_l, !Rmult_1_r.
  assert (f 1%nat <= f 0%nat) by apply decr.
- rewrite Ropp_mult_distr_l_reverse.
  intros [A B]; rewrite Rabs_pos_eq; fourier.
 apply Rle_trans with (f 1%nat).
  apply (Hyp 1%nat (le_n 1) (S n) decr to0 cv).
@@ -320,31 +319,12 @@ apply PI2_lower_bound;[split; fourier | ].
 destruct (pre_cos_bound (3/2) 1) as [t _]; [fourier | fourier | ].
 apply Rlt_le_trans with (2 := t); clear t.
 unfold cos_approx; simpl; unfold cos_term.
-simpl mult; replace ((-1)^ 0) with 1 by ring; replace ((-1)^2) with 1 by ring;
- replace ((-1)^4) with 1 by ring; replace ((-1)^1) with (-1) by ring;
- replace ((-1)^3) with (-1) by ring; change 3 with (IZR 3);
- change 2 with (IZR 2); simpl Z.of_nat;
- rewrite !INR_IZR_INZ, Ropp_mult_distr_l_reverse, Rmult_1_l.
-match goal with |- _ < ?a =>
-replace a with ((- IZR 3 ^ 6 * IZR (Z.of_nat (fact 0)) * IZR (Z.of_nat (fact 2)) *
-    IZR (Z.of_nat (fact 4)) +
-    IZR 3 ^ 4 * IZR 2 ^ 2 * IZR (Z.of_nat (fact 0)) * IZR (Z.of_nat (fact 2)) *
-    IZR (Z.of_nat (fact 6)) -
-    IZR 3 ^ 2 * IZR 2 ^ 4 * IZR (Z.of_nat (fact 0)) * IZR (Z.of_nat (fact 4)) *
-    IZR (Z.of_nat (fact 6)) +
-    IZR 2 ^ 6 * IZR (Z.of_nat (fact 2)) * IZR (Z.of_nat (fact 4)) *
-    IZR (Z.of_nat (fact 6))) /
-   (IZR 2 ^ 6 * IZR (Z.of_nat (fact 0)) * IZR (Z.of_nat (fact 2)) *
-    IZR (Z.of_nat (fact 4)) * IZR (Z.of_nat (fact 6))));[ | field;
-    repeat apply conj;((rewrite <- INR_IZR_INZ; apply INR_fact_neq_0) ||
-         (apply Rgt_not_eq; apply (IZR_lt 0); reflexivity)) ]
-end.
-rewrite !fact_simpl, !Nat2Z.inj_mul; simpl Z.of_nat.
-unfold Rdiv; apply Rmult_lt_0_compat.
-unfold Rminus; rewrite !pow_IZR, <- !opp_IZR, <- !mult_IZR, <- !opp_IZR, 
-  <- !plus_IZR; apply (IZR_lt 0); reflexivity.
-apply Rinv_0_lt_compat; rewrite !pow_IZR, <- !mult_IZR; apply (IZR_lt 0).
-reflexivity.
+unfold INR.
+simpl.
+field_simplify.
+change (0 */ 1 < 9925632 / 141557760).
+rewrite Rmult_0_l.
+apply Rdiv_lt_0_compat ; now apply IZR_lt.
 Qed.
 
 Lemma PI2_1 : 1 < PI/2.
@@ -502,11 +482,11 @@ split.
   rewrite (Rmult_comm (-1)); simpl ((/(Rabs y + 1)) ^ 0).
   unfold Rdiv; rewrite Rinv_1, !Rmult_assoc, <- !Rmult_plus_distr_l.
   apply tmp;[assumption | ].
-  rewrite Rplus_assoc, Rmult_1_l; pattern 1 at 3; rewrite <- Rplus_0_r.
+  rewrite Rplus_assoc, Rmult_1_l; pattern 1 at 2; rewrite <- Rplus_0_r.
   apply Rplus_lt_compat_l.
   rewrite <- Rmult_assoc.
   match goal with |- (?a * (-1)) + _ < 0 =>
-   rewrite <- (Rplus_opp_l a), Ropp_mult_distr_r_reverse, Rmult_1_r
+   rewrite <- (Rplus_opp_l a); change (-1) with (-(1)); rewrite Ropp_mult_distr_r_reverse, Rmult_1_r
   end.
   apply Rplus_lt_compat_l.
   assert (0 < u ^ 2) by (apply pow_lt; assumption).
@@ -1078,8 +1058,9 @@ apply Rlt_not_eq; apply Rle_lt_trans with 0;[ | apply Rlt_0_1].
 assert (t := pow2_ge_0 x); fourier.
 replace (1 + x ^ 2) with (1 - - (x ^ 2)) by ring; rewrite <- (tech3 _ n dif).
 apply sum_eq; unfold tg_alt, Datan_seq; intros i _.
-rewrite pow_mult, <- Rpow_mult_distr, Ropp_mult_distr_l_reverse, Rmult_1_l.
-reflexivity.
+rewrite pow_mult, <- Rpow_mult_distr.
+f_equal.
+ring.
 Qed.
 
 Lemma Datan_seq_increasing : forall x y n, (n > 0)%nat -> 0 <= x < y -> Datan_seq x n < Datan_seq y n.
@@ -1167,6 +1148,7 @@ assert (tool : forall a b, a / b - /b = (-1 + a) /b).
  reflexivity.
 set (u := 1 + x ^ 2); rewrite tool; unfold Rminus; rewrite <- Rplus_assoc.
 unfold Rdiv, u.
+change (-1) with (-(1)).
 rewrite Rplus_opp_l, Rplus_0_l, Ropp_mult_distr_l_reverse, Rabs_Ropp.
 rewrite Rabs_mult; clear tool u.
 assert (tool : forall k, Rabs ((-x ^ 2) ^ k) = Rabs ((x ^ 2) ^ k)).
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index e9098104c..7f9db3b18 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -115,35 +115,6 @@ Arguments INR n%nat.
 
 
 (**********************************************************)
-(** *    Injection from [Z] to [R]                        *)
-(**********************************************************)
-
-(* compact representation for 2*p *)
-Fixpoint IPR_2 (p:positive) : R :=
-  match p with
-  | xH => 1 + 1
-  | xO p => (1 + 1) * IPR_2 p
-  | xI p => (1 + 1) * (1 + IPR_2 p)
-  end.
-
-Definition IPR (p:positive) : R :=
-  match p with
-  | xH => 1
-  | xO p => IPR_2 p
-  | xI p => 1 + IPR_2 p
-  end.
-Arguments IPR p%positive : simpl never.
-
-(**********)
-Definition IZR (z:Z) : R :=
-  match z with
-  | Z0 => 0
-  | Zpos n => IPR n
-  | Zneg n => - IPR n
-  end.
-Arguments IZR z%Z : simpl never.
-
-(**********************************************************)
 (** *    [R] Archimedean                                  *)
 (**********************************************************)
 
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index fe5402e6e..df1662497 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -451,20 +451,16 @@ Qed.
 
 Lemma Rabs_Ropp : forall x:R, Rabs (- x) = Rabs x.
 Proof.
-  intro; cut (- x = -1 * x).
-  intros; rewrite H.
+  intro; replace (-x) with (-1 * x) by ring.
   rewrite Rabs_mult.
-  cut (Rabs (-1) = 1).
-  intros; rewrite H0.
-  ring.
+  replace (Rabs (-1)) with 1.
+  apply Rmult_1_l.
   unfold Rabs; case (Rcase_abs (-1)).
   intro; ring.
-  intro H0; generalize (Rge_le (-1) 0 H0); intros.
-  generalize (Ropp_le_ge_contravar 0 (-1) H1).
-  rewrite Ropp_involutive; rewrite Ropp_0.
-  intro; generalize (Rgt_not_le 1 0 Rlt_0_1); intro; generalize (Rge_le 0 1 H2);
-    intro; exfalso; auto.
-  ring.
+  rewrite <- Ropp_0.
+  intro H0; apply Ropp_ge_cancel in H0.
+  elim (Rge_not_lt _ _ H0).
+  apply Rlt_0_1.
 Qed.
 
 (*********)
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index f3f8f7409..cb5dea93a 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -69,3 +69,32 @@ 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.
+
+(**********************************************************)
+(** *    Injection from [Z] to [R]                        *)
+(**********************************************************)
+
+(* compact representation for 2*p *)
+Fixpoint IPR_2 (p:positive) : R :=
+  match p with
+  | xH => R1 + R1
+  | xO p => (R1 + R1) * IPR_2 p
+  | xI p => (R1 + R1) * (R1 + IPR_2 p)
+  end.
+
+Definition IPR (p:positive) : R :=
+  match p with
+  | xH => R1
+  | xO p => IPR_2 p
+  | xI p => R1 + IPR_2 p
+  end.
+Arguments IPR p%positive : simpl never.
+
+(**********)
+Definition IZR (z:Z) : R :=
+  match z with
+  | Z0 => R0
+  | Zpos n => IPR n
+  | Zneg n => - IPR n
+  end.
+Arguments IZR z%Z : simpl never.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 0a49d4983..99acdd0a1 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -416,8 +416,9 @@ Proof.
   simpl; apply Rabs_R1.
   replace (S n) with (n + 1)%nat; [ rewrite pow_add | ring ].
   rewrite Rabs_mult.
-  rewrite Hrecn; rewrite Rmult_1_l; simpl; rewrite Rmult_1_r;
-    rewrite Rabs_Ropp; apply Rabs_R1.
+  rewrite Hrecn; rewrite Rmult_1_l; simpl; rewrite Rmult_1_r.
+  change (-1) with (-(1)).
+  rewrite Rabs_Ropp; apply Rabs_R1.
 Qed.
 
 Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = (x ^ n1) ^ n2.
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index 7bd6c916d..b9a9458c8 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -82,7 +82,7 @@ assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R).
   apply Rle_lt_trans with (1 := H1l).
   apply archimed.
   rewrite minus_IZR.
-  change (IZR 2) with 2%R.
+  simpl.
   ring.
 assert (Hl': (/ (INR (S N) + 1) < l)%R).
   rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq.
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
index 791718a45..f331bb203 100644
--- a/theories/Reals/Rpow_def.v
+++ b/theories/Reals/Rpow_def.v
@@ -10,6 +10,6 @@ Require Import Rdefinitions.
 
 Fixpoint pow (r:R) (n:nat) : R :=
   match n with
-    | O => R1
+    | O => 1
     | S n => Rmult r (pow r n)
   end.
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index a053c349e..f62ed2a6c 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -488,12 +488,9 @@ Proof.
   rewrite Rinv_r.
   apply exp_lt_inv.
   apply Rle_lt_trans with (1 := exp_le_3).
-  change (3 < 2 ^R 2).
+  change (3 < 2 ^R (1 + 1)).
   repeat rewrite Rpower_plus; repeat rewrite Rpower_1.
-  repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l;
-    repeat rewrite Rmult_1_l.
-  pattern 3 at 1; rewrite <- Rplus_0_r; replace (2 + 2) with (3 + 1);
-    [ apply Rplus_lt_compat_l; apply Rlt_0_1 | ring ].
+  now apply (IZR_lt 3 4).
   prove_sup0.
   discrR.
 Qed.
@@ -715,7 +712,7 @@ Definition arcsinh x := ln (x + sqrt (x ^ 2 + 1)).
 Lemma arcsinh_sinh : forall x, arcsinh (sinh x) = x.
 intros x; unfold sinh, arcsinh.
 assert (Rminus_eq_0 : forall r, r - r = 0) by (intros; ring).
-pattern 1 at 5; rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus.
+rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus.
 rewrite exp_plus.
 match goal with |- context[sqrt ?a] => 
   replace a with (((exp x + exp(-x))/2)^2) by field
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 744fd6641..c6b0c3f37 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -207,7 +207,7 @@ Section sequence.
 
     assert (Rabs (/2) < 1).
     rewrite Rabs_pos_eq.
-    rewrite <- Rinv_1 at 3.
+    rewrite <- Rinv_1.
     apply Rinv_lt_contravar.
     rewrite Rmult_1_l.
     now apply (IZR_lt 0 2).
diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v
index 6b1754021..48dbd1944 100644
--- a/theories/Reals/Rtrigo1.v
+++ b/theories/Reals/Rtrigo1.v
@@ -182,13 +182,11 @@ destruct (pre_cos_bound _ 0 lo up) as [_ upper].
 apply Rle_lt_trans with (1 := upper).
 apply Rlt_le_trans with (2 := lower).
 unfold cos_approx, sin_approx.
-simpl sum_f_R0; change 7 with (IZR 7).
-change 8 with (IZR 8).
+simpl sum_f_R0.
 unfold cos_term, sin_term; simpl fact; rewrite !INR_IZR_INZ.
-simpl plus; simpl mult.
-field_simplify;
-  try (repeat apply conj; apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity).
-unfold Rminus; rewrite !pow_IZR, <- !mult_IZR, <- !opp_IZR, <- ?plus_IZR.
+simpl plus; simpl mult; simpl Z_of_nat.
+field_simplify.
+change (8073344 / 12582912 < 18760 / 24576).
 match goal with 
   |- IZR ?a / ?b < ?c / ?d =>
   apply Rmult_lt_reg_r with d;[apply (IZR_lt 0); reflexivity |
@@ -323,6 +321,7 @@ Lemma sin_PI : sin PI = 0.
 Proof.
   assert (H := sin2_cos2 PI).
   rewrite cos_PI in H.
+  change (-1) with (-(1)) in H.
   rewrite <- Rsqr_neg in H.
   rewrite Rsqr_1 in H.
   cut (Rsqr (sin PI) = 0).
@@ -533,9 +532,8 @@ Qed.
 
 Lemma sin_PI_x : forall x:R, sin (PI - x) = sin x.
 Proof.
-  intro x; rewrite sin_minus; rewrite sin_PI; rewrite cos_PI; rewrite Rmult_0_l;
-    unfold Rminus in |- *; rewrite Rplus_0_l; rewrite Ropp_mult_distr_l_reverse;
-      rewrite Ropp_involutive; apply Rmult_1_l.
+  intro x; rewrite sin_minus; rewrite sin_PI; rewrite cos_PI.
+  ring.
 Qed.
 
 Lemma sin_period : forall (x:R) (k:nat), sin (x + 2 * INR k * PI) = sin x.
@@ -593,9 +591,9 @@ Proof.
     generalize
       (Rsqr_incrst_1 1 (sin x) H (Rlt_le 0 1 Rlt_0_1)
         (Rlt_le 0 (sin x) (Rlt_trans 0 1 (sin x) Rlt_0_1 H)));
-      rewrite Rsqr_1; intro; rewrite sin2 in H0; unfold Rminus in H0;
+      rewrite Rsqr_1; intro; rewrite sin2 in H0; unfold Rminus in H0.
         generalize (Rplus_lt_compat_l (-1) 1 (1 + - Rsqr (cos x)) H0);
-          repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_l;
+          repeat rewrite <- Rplus_assoc; change (-1) with (-(1)); rewrite Rplus_opp_l;
             rewrite Rplus_0_l; intro; rewrite <- Ropp_0 in H1;
               generalize (Ropp_lt_gt_contravar (-0) (- Rsqr (cos x)) H1);
                 repeat rewrite Ropp_involutive; intro; generalize (Rle_0_sqr (cos x));
@@ -603,6 +601,7 @@ Proof.
   auto with real.
   cut (sin x < -1).
   intro; generalize (Ropp_lt_gt_contravar (sin x) (-1) H);
+    change (-1) with (-(1));
     rewrite Ropp_involutive; clear H; intro;
       generalize
         (Rsqr_incrst_1 1 (- sin x) H (Rlt_le 0 1 Rlt_0_1)
@@ -610,7 +609,7 @@ Proof.
         rewrite Rsqr_1; intro; rewrite <- Rsqr_neg in H0;
           rewrite sin2 in H0; unfold Rminus in H0;
             generalize (Rplus_lt_compat_l (-1) 1 (1 + - Rsqr (cos x)) H0);
-              repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_l;
+              rewrite <- Rplus_assoc; change (-1) with (-(1)); rewrite Rplus_opp_l;
                 rewrite Rplus_0_l; intro; rewrite <- Ropp_0 in H1;
                   generalize (Ropp_lt_gt_contravar (-0) (- Rsqr (cos x)) H1);
                     repeat rewrite Ropp_involutive; intro; generalize (Rle_0_sqr (cos x));
@@ -712,17 +711,16 @@ Proof.
   do 2 rewrite fact_simpl; do 2 rewrite mult_INR.
   repeat rewrite <- Rmult_assoc.
   rewrite <- (Rmult_comm (INR (fact (2 * n + 1)))).
-  rewrite Rmult_assoc.
   apply Rmult_lt_compat_l.
   apply lt_INR_0; apply neq_O_lt.
   assert (H2 := fact_neq_0 (2 * n + 1)).
   red in |- *; intro; elim H2; symmetry  in |- *; assumption.
   do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; set (x := INR n);
     unfold INR in |- *.
-  replace ((2 * x + 1 + 1 + 1) * (2 * x + 1 + 1)) with (4 * x * x + 10 * x + 6);
+  replace (((1 + 1) * x + 1 + 1 + 1) * ((1 + 1) * x + 1 + 1)) with (4 * x * x + 10 * x + 6);
   [ idtac | ring ].
-  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);
+  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.
   cut (0 <= x).
@@ -767,7 +765,7 @@ Proof.
   unfold Rdiv in |- *; pattern PI at 2 in |- *; rewrite <- Rmult_1_r.
   apply Rmult_lt_compat_l.
   apply PI_RGT_0.
-  pattern 1 at 3 in |- *; rewrite <- Rinv_1; apply Rinv_lt_contravar.
+  rewrite <- Rinv_1; apply Rinv_lt_contravar.
   rewrite Rmult_1_l; prove_sup0.
   pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l;
     apply Rlt_0_1.
@@ -1715,7 +1713,7 @@ Proof.
   rewrite H5.
   rewrite mult_INR.
   simpl in |- *.
-  rewrite <- (Rplus_0_l (2 * INR x2 * PI)).
+  rewrite <- (Rplus_0_l ((1 + 1) * INR x2 * PI)).
   rewrite sin_period.
   apply sin_0.
   rewrite H5.
@@ -1725,7 +1723,7 @@ Proof.
   rewrite Rmult_1_l; rewrite sin_plus.
   rewrite sin_PI.
   rewrite Rmult_0_r.
-  rewrite <- (Rplus_0_l (2 * INR x2 * PI)).
+  rewrite <- (Rplus_0_l ((1 + 1) * INR x2 * PI)).
   rewrite sin_period.
   rewrite sin_0; ring.
   apply le_IZR.
@@ -1747,7 +1745,7 @@ Proof.
   rewrite H5.
   rewrite mult_INR.
   simpl in |- *.
-  rewrite <- (Rplus_0_l (2 * INR x2 * PI)).
+  rewrite <- (Rplus_0_l ((1 + 1) * INR x2 * PI)).
   rewrite sin_period.
   rewrite sin_0; ring.
   rewrite H5.
@@ -1757,7 +1755,7 @@ Proof.
   rewrite Rmult_1_l; rewrite sin_plus.
   rewrite sin_PI.
   rewrite Rmult_0_r.
-  rewrite <- (Rplus_0_l (2 * INR x2 * PI)).
+  rewrite <- (Rplus_0_l ((1 + 1) * INR x2 * PI)).
   rewrite sin_period.
   rewrite sin_0; ring.
   apply le_IZR.
@@ -1798,7 +1796,7 @@ Lemma cos_eq_0_0 (x:R) :
 Proof.
   rewrite cos_sin. intros Hx.
   destruct (sin_eq_0_0 (PI/2 + x) Hx) as (k,Hk). clear Hx.
-  exists (k-1)%Z. rewrite <- Z_R_minus; change (IZR 1) with 1.
+  exists (k-1)%Z. rewrite <- Z_R_minus; simpl.
   symmetry in Hk. field_simplify [Hk]. field.
 Qed.
 
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index a5092d22d..092bc30d0 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -320,7 +320,7 @@ Proof.
   (1 - sum_f_R0 (fun i:nat => cos_n i * Rsqr a0 ^ i) (S n1)).
   unfold Rminus; rewrite Ropp_plus_distr; rewrite Ropp_involutive;
     repeat rewrite Rplus_assoc; rewrite (Rplus_comm 1);
-      rewrite (Rplus_comm (-1)); repeat rewrite Rplus_assoc;
+      rewrite (Rplus_comm (-(1))); repeat rewrite Rplus_assoc;
         rewrite Rplus_opp_l; rewrite Rplus_0_r; rewrite <- Rabs_Ropp;
           rewrite Ropp_plus_distr; rewrite Ropp_involutive;
             unfold Rminus in H6; apply H6.
@@ -367,10 +367,10 @@ Proof.
   reflexivity.
   ring.
   intro; elim H2; intros; split.
-  apply Rplus_le_reg_l with (-1).
+  apply Rplus_le_reg_l with (-(1)).
   rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
     rewrite (Rplus_comm (-1)); apply H3.
-  apply Rplus_le_reg_l with (-1).
+  apply Rplus_le_reg_l with (-(1)).
   rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l;
     rewrite (Rplus_comm (-1)); apply H4.
   unfold cos_term; simpl; unfold Rdiv; rewrite Rinv_1;
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 4a1e3179c..d9c18d358 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -251,6 +251,7 @@ Proof.
   exists delta; intros.
   rewrite Rplus_0_l; replace (cos h - cos 0) with (-2 * Rsqr (sin (h / 2))).
   unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r.
+  change (-2) with (-(2)).
   unfold Rdiv; do 2 rewrite Ropp_mult_distr_l_reverse.
   rewrite Rabs_Ropp.
   replace (2 * Rsqr (sin (h * / 2)) * / h) with
@@ -266,7 +267,7 @@ Proof.
   apply Rabs_pos.
   assert (H9 := SIN_bound (h / 2)).
   unfold Rabs; case (Rcase_abs (sin (h / 2))); intro.
-  pattern 1 at 3; rewrite <- (Ropp_involutive 1).
+  rewrite <- (Ropp_involutive 1).
   apply Ropp_le_contravar.
   elim H9; intros; assumption.
   elim H9; intros; assumption.
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index d43baee8c..12d5cbbf0 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -21,6 +21,7 @@ Proof.
   destruct (total_order_T h 0) as [[Hlt|Heq]|Hgt].
   repeat rewrite Rabs_left.
   unfold Rminus; do 2 rewrite <- (Rplus_comm (-1)).
+  change (-1) with (-(1)).
   do 2 rewrite Ropp_plus_distr; rewrite Ropp_involutive;
     apply Rplus_le_compat_l.
   apply Ropp_le_contravar; apply sqrt_le_1.