Simplify some proofs.

This commit does not modify the signature of the involved modules, only
the opaque proof terms.

One has to wonder how proofs can bitrot so much that several occurrences
of "replace 4 with 4" start appearing.

13 files changed, 172 insertions, 422 deletions

diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index c3ab8edc5..17ffc0fe3 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -339,51 +339,24 @@ Proof.
   symmetry ; apply S_pred with 0%nat.
   assumption.
   apply Rle_lt_trans with (/ INR (2 * N)).
-  apply Rmult_le_reg_l with (INR (2 * N)).
+  apply Rinv_le_contravar.
   rewrite mult_INR; apply Rmult_lt_0_compat;
     [ simpl; prove_sup0 | apply lt_INR_0; assumption ].
-  rewrite <- Rinv_r_sym.
-  apply Rmult_le_reg_l with (INR (2 * n)).
-  rewrite mult_INR; apply Rmult_lt_0_compat;
-    [ simpl; prove_sup0 | apply lt_INR_0; assumption ].
-  rewrite (Rmult_comm (INR (2 * n))); rewrite Rmult_assoc;
-    rewrite <- Rinv_l_sym.
-  do 2 rewrite Rmult_1_r; apply le_INR.
-  apply (fun m n p:nat => mult_le_compat_l p n m); assumption.
-  replace n with (S (pred n)).
-  apply not_O_INR; discriminate.
-  symmetry ; apply S_pred with 0%nat.
-  assumption.
-  replace N with (S (pred N)).
-  apply not_O_INR; discriminate.
-  symmetry ; apply S_pred with 0%nat.
-  assumption.
+  apply le_INR.
+  now apply mult_le_compat_l.
   rewrite mult_INR.
-  rewrite Rinv_mult_distr.
-  replace (INR 2) with 2; [ idtac | reflexivity ].
-  apply Rmult_lt_reg_l with 2.
-  prove_sup0.
-  rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym; [ idtac | discrR ].
-  rewrite Rmult_1_l; apply Rmult_lt_reg_l with (INR N).
-  apply lt_INR_0; assumption.
-  rewrite <- Rinv_r_sym.
-  apply Rmult_lt_reg_l with (/ (2 * eps)).
-  apply Rinv_0_lt_compat; assumption.
-  rewrite Rmult_1_r;
-    replace (/ (2 * eps) * (INR N * (2 * eps))) with
-      (INR N * (2 * eps * / (2 * eps))); [ idtac | ring ].
-  rewrite <- Rinv_r_sym.
-  rewrite Rmult_1_r; replace (INR N) with (IZR (Z.of_nat N)).
-  rewrite <- H4.
-  elim H1; intros; assumption.
-  symmetry ; apply INR_IZR_INZ.
-  apply prod_neq_R0;
-    [ discrR | red; intro; rewrite H8 in H; elim (Rlt_irrefl _ H) ].
-  apply not_O_INR.
-  red; intro; rewrite H8 in H5; elim (lt_irrefl _ H5).
-  replace (INR 2) with 2; [ discrR | reflexivity ].
-  apply not_O_INR.
-  red; intro; rewrite H8 in H5; elim (lt_irrefl _ H5).
+  apply Rmult_lt_reg_l with (INR N / eps).
+  apply Rdiv_lt_0_compat with (2 := H).
+  now apply (lt_INR 0).
+  replace (_ */ _) with (/(2 * eps)).
+  replace (_ / _ * _) with (INR N).
+  rewrite INR_IZR_INZ.
+  now rewrite <- H4.
+  field.
+  now apply Rgt_not_eq.
+  simpl (INR 2); field; split.
+  now apply Rgt_not_eq, (lt_INR 0).
+  now apply Rgt_not_eq.
   apply Rle_ge; apply PI_tg_pos.
   apply lt_le_trans with N; assumption.
   elim H1; intros H5 _.
@@ -395,7 +368,6 @@ Proof.
   elim (Rlt_irrefl _ (Rlt_trans _ _ _ H6 H5)).
   elim (lt_n_O _ H6).
   apply le_IZR.
-  simpl.
   left; apply Rlt_trans with (/ (2 * eps)).
   apply Rinv_0_lt_compat; assumption.
   elim H1; intros; assumption.
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index b14d807d2..eb4a3b804 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -289,11 +289,9 @@ Proof.
   apply INR_fact_lt_0.
   rewrite <- Rinv_r_sym.
   rewrite Rmult_1_r.
-  replace 1 with (INR 1).
-  apply le_INR.
+  apply (le_INR 1).
   apply lt_le_S.
   apply INR_lt; apply INR_fact_lt_0.
-  reflexivity.
   apply INR_fact_neq_0.
   apply Rmult_le_reg_l with (INR (fact (S (N + n)))).
   apply INR_fact_lt_0.
@@ -576,11 +574,9 @@ Proof.
   apply INR_fact_lt_0.
   rewrite <- Rinv_r_sym.
   rewrite Rmult_1_r.
-  replace 1 with (INR 1).
-  apply le_INR.
+  apply (le_INR 1).
   apply lt_le_S.
   apply INR_lt; apply INR_fact_lt_0.
-  reflexivity.
   apply INR_fact_neq_0.
   apply Rmult_le_reg_l with (INR (fact (S (S (N + n))))).
   apply INR_fact_lt_0.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index e9de24898..76f4e1449 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -532,7 +532,7 @@ Proof.
   apply Rmult_le_reg_l with (INR (fact (div2 (pred n)))).
   apply INR_fact_lt_0.
   rewrite Rmult_1_r; rewrite <- Rinv_r_sym.
-  replace 1 with (INR 1); [ apply le_INR | reflexivity ].
+  apply (le_INR 1).
   apply lt_le_S.
   apply INR_lt.
   apply INR_fact_lt_0.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 8bebb5237..7e1cc3e03 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1629,7 +1629,7 @@ Hint Resolve lt_INR: real.
 
 Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n.
 Proof.
-  intros; replace 1 with (INR 1); auto with real.
+  apply lt_INR.
 Qed.
 Hint Resolve lt_1_INR: real.
 
@@ -1653,17 +1653,16 @@ Hint Resolve pos_INR: real.
 
 Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
 Proof.
-  double induction n m; intros.
-  simpl; exfalso; apply (Rlt_irrefl 0); auto.
-  auto with arith.
-  generalize (pos_INR (S n0)); intro; cut (INR 0 = 0);
-    [ intro H2; rewrite H2 in H0; idtac | simpl; trivial ].
-  generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; exfalso;
-    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_l 1 (INR n1) (INR n0)).
-  rewrite Rplus_comm; rewrite (Rplus_comm 1 (INR n0)); trivial.
+  intros n m. revert n.
+  induction m ; intros n H.
+  - elim (Rlt_irrefl 0).
+    apply Rle_lt_trans with (2 := H).
+    apply pos_INR.
+  - destruct n as [|n].
+    apply Nat.lt_0_succ.
+    apply lt_n_S, IHm.
+    rewrite 2!S_INR in H.
+    apply Rplus_lt_reg_r with (1 := H).
 Qed.
 Hint Resolve INR_lt: real.
 
@@ -1707,14 +1706,10 @@ Hint Resolve not_INR: real.
 
 Lemma INR_eq : forall n m:nat, INR n = INR m -> n = m.
 Proof.
-  intros; case (le_or_lt n m); intros H1.
-  case (le_lt_or_eq _ _ H1); intros H2; auto.
-  cut (n <> m).
-  intro H3; generalize (not_INR n m H3); intro H4; exfalso; auto.
-  omega.
-  symmetry ; cut (m <> n).
-  intro H3; generalize (not_INR m n H3); intro H4; exfalso; auto.
-  omega.
+  intros n m HR.
+  destruct (dec_eq_nat n m) as [H|H].
+  exact H.
+  now apply not_INR in H.
 Qed.
 Hint Resolve INR_eq: real.
 
@@ -1728,7 +1723,8 @@ Hint Resolve INR_le: real.
 
 Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n <> 1.
 Proof.
-  replace 1 with (INR 1); auto with real.
+  intros n.
+  apply not_INR.
 Qed.
 Hint Resolve not_1_INR: real.
 
@@ -1905,8 +1901,8 @@ Qed.
 (**********)
 Lemma le_IZR_R1 : forall n:Z, IZR n <= 1 -> (n <= 1)%Z.
 Proof.
-  pattern 1 at 1; replace 1 with (IZR 1); intros; auto.
-  apply le_IZR; trivial.
+  intros n.
+  apply le_IZR.
 Qed.
 
 (**********)
@@ -1935,7 +1931,7 @@ Proof.
   intros z [H1 H2].
   apply Z.le_antisymm.
   apply Z.lt_succ_r; apply lt_IZR; trivial.
-  replace 0%Z with (Z.succ (-1)); trivial.
+  change 0%Z with (Z.succ (-1)).
   apply Z.le_succ_l; apply lt_IZR; trivial.
 Qed.
 
@@ -2012,8 +2008,7 @@ Lemma double_var : forall r1, r1 = r1 / 2 + r1 / 2.
 Proof.
   intro; rewrite <- double; unfold Rdiv; rewrite <- Rmult_assoc;
     symmetry ; apply Rinv_r_simpl_m.
-  replace 2 with (INR 2);
-  [ apply not_0_INR; discriminate | unfold INR; ring ].
+  now apply not_0_IZR.
 Qed.
 
 Lemma R_rm : ring_morph
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v
index e9b1762af..46583d374 100644
--- a/theories/Reals/R_Ifp.v
+++ b/theories/Reals/R_Ifp.v
@@ -42,28 +42,23 @@ Qed.
 Lemma up_tech :
   forall (r:R) (z:Z), IZR z <= r -> r < IZR (z + 1) -> (z + 1)%Z = up r.
 Proof.
-  intros; generalize (Rplus_le_compat_l 1 (IZR z) r H); intro; clear H;
-    rewrite (Rplus_comm 1 (IZR z)) in H1; rewrite (Rplus_comm 1 r) in H1;
-      cut (1 = IZR 1); auto with zarith real.
-  intro; generalize H1; pattern 1 at 1; rewrite H; intro; clear H H1;
-    rewrite <- (plus_IZR z 1) in H2; apply (tech_up r (z + 1));
-      auto with zarith real.
+  intros.
+  apply tech_up with (1 := H0).
+  rewrite plus_IZR.
+  now apply Rplus_le_compat_r.
 Qed.
 
 (**********)
 Lemma fp_R0 : frac_part 0 = 0.
 Proof.
-  unfold frac_part; unfold Int_part; elim (archimed 0); intros;
-    unfold Rminus; elim (Rplus_ne (- IZR (up 0 - 1)));
-      intros a b; rewrite b; clear a b; rewrite <- Z_R_minus;
-        cut (up 0 = 1%Z).
-  intro; rewrite H1;
-    rewrite (Rminus_diag_eq (IZR 1) (IZR 1) (eq_refl (IZR 1)));
-      apply Ropp_0.
-  elim (archimed 0); intros; clear H2; unfold Rgt in H1;
-    rewrite (Rminus_0_r (IZR (up 0))) in H0; generalize (lt_O_IZR (up 0) H1);
-      intro; clear H1; generalize (le_IZR_R1 (up 0) H0);
-        intro; clear H H0; omega.
+  unfold frac_part, Int_part.
+  replace (up 0) with 1%Z.
+  now rewrite <- minus_IZR.
+  destruct (archimed 0) as [H1 H2].
+  apply lt_IZR in H1.
+  rewrite <- minus_IZR in H2.
+  apply le_IZR in H2.
+  omega.
 Qed.
 
 (**********)
@@ -229,8 +224,7 @@ Proof.
                                                                                                               rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H;
                                                                                                                 elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H;
                                                                                                                   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.
+                                                                                                                    rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H.
     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;
@@ -497,8 +491,7 @@ Proof.
                                                                 in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0;
                                                                   elim (Rplus_ne (IZR (Int_part r1) + IZR (Int_part r2)));
                                                                     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.
+                                                                      intros a b; rewrite b in H0; clear a b.
     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;
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index 27cb356a0..b749da0d2 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -423,10 +423,7 @@ Proof.
   intro; rewrite H11 in H10; assert (H12 := Rmult_lt_compat_l 2 _ _ Hyp H10);
     rewrite Rmult_1_r in H12; rewrite <- Rinv_r_sym in H12;
       [ idtac | discrR ].
-  cut (IZR 1 < IZR 2).
-  unfold IZR; unfold INR, Pos.to_nat; simpl; intro;
-    elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)).
-  apply IZR_lt; omega.
+  now apply lt_IZR in H12.
   unfold Rabs; case (Rcase_abs (/ 2)) as [Hlt|Hge].
   assert (Hyp : 0 < 2).
   prove_sup0.
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 7885d697f..af7cbb940 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -83,11 +83,10 @@ Proof.
   cut (x = INR (pred x0)).
   intro H19; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18;
     rewrite <- H19; assumption.
-  rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; replace 1 with (INR 1);
-    [ idtac | reflexivity ]; rewrite <- minus_INR.
-  replace (x0 - 1)%nat with (pred x0);
-  [ reflexivity
-    | case x0; [ reflexivity | intro; simpl; apply minus_n_O ] ].
+  rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ;
+    rewrite <- (minus_INR _ 1).
+  apply f_equal;
+    case x0; [ reflexivity | intro; apply sym_eq, minus_n_O ].
   induction x0 as [|x0 Hrecx0].
     rewrite H8 in H3. rewrite <- INR_IZR_INZ in H3; simpl in H3.
       elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H3)).
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index f07140752..843aa2752 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -29,59 +29,28 @@ Qed.
 Lemma eps2 : forall eps:R, eps * / 2 + eps * / 2 = eps.
 Proof.
   intro esp.
-  assert (H := double_var esp).
-  unfold Rdiv in H.
-  symmetry ; exact H.
+  apply eq_sym, double_var.
 Qed.
 
 (*********)
 Lemma eps4 : forall eps:R, eps * / (2 + 2) + eps * / (2 + 2) = eps * / 2.
 Proof.
   intro eps.
-  replace (2 + 2) with 4.
-  pattern eps at 3; rewrite double_var.
-  rewrite (Rmult_plus_distr_r (eps / 2) (eps / 2) (/ 2)).
-  unfold Rdiv.
-  repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_mult_distr.
-  reflexivity.
-  discrR.
-  discrR.
-  ring.
+  field.
 Qed.
 
 (*********)
 Lemma Rlt_eps2_eps : forall eps:R, eps > 0 -> eps * / 2 < eps.
 Proof.
   intros.
-  pattern eps at 2; rewrite <- Rmult_1_r.
-  repeat rewrite (Rmult_comm eps).
-  apply Rmult_lt_compat_r.
-  exact H.
-  apply Rmult_lt_reg_l with 2.
   fourier.
-  rewrite Rmult_1_r; rewrite <- Rinv_r_sym.
-  fourier.
-  discrR.
 Qed.
 
 (*********)
 Lemma Rlt_eps4_eps : forall eps:R, eps > 0 -> eps * / (2 + 2) < eps.
 Proof.
   intros.
-  replace (2 + 2) with 4.
-  pattern eps at 2; rewrite <- Rmult_1_r.
-  repeat rewrite (Rmult_comm eps).
-  apply Rmult_lt_compat_r.
-  exact H.
-  apply Rmult_lt_reg_l with 4.
-  replace 4 with 4.
-  apply Rmult_lt_0_compat; fourier.
-  ring.
-  rewrite Rmult_1_r; rewrite <- Rinv_r_sym.
   fourier.
-  discrR.
-  ring.
 Qed.
 
 (*********)
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index f62ed2a6c..b8040bb4f 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -456,7 +456,7 @@ Proof.
   unfold Rpower; auto.
   rewrite Rpower_mult.
   rewrite Rinv_l.
-  replace 1 with (INR 1); auto.
+  change 1 with (INR 1).
   repeat rewrite Rpower_pow; simpl.
   pattern x at 1; rewrite <- (sqrt_sqrt x (Rlt_le _ _ H)).
   ring.
diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v
index 17b9677ef..5a999eebe 100644
--- a/theories/Reals/Rtrigo1.v
+++ b/theories/Reals/Rtrigo1.v
@@ -694,16 +694,15 @@ Proof.
     rewrite <- Rinv_l_sym.
   do 2 rewrite Rmult_1_r; apply Rle_lt_trans with (INR (fact (2 * n + 1)) * 4).
   apply Rmult_le_compat_l.
-  replace 0 with (INR 0); [ idtac | reflexivity ]; apply le_INR; apply le_O_n.
-  simpl in |- *; rewrite Rmult_1_r; replace 4 with (Rsqr 2);
-    [ idtac | ring_Rsqr ]; replace (a * a) with (Rsqr a);
-    [ idtac | reflexivity ]; apply Rsqr_incr_1.
+  apply pos_INR.
+  simpl in |- *; rewrite Rmult_1_r; change 4 with (Rsqr 2);
+    apply Rsqr_incr_1.
   apply Rle_trans with (PI / 2);
     [ assumption
       | unfold Rdiv in |- *; apply Rmult_le_reg_l with 2;
         [ prove_sup0
           | rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m;
-            [ replace 4 with 4; [ apply PI_4 | ring ] | discrR ] ] ].
+            [ apply PI_4 | discrR ] ] ].
   left; assumption.
   left; prove_sup0.
   rewrite H1; replace (2 * n + 1 + 2)%nat with (S (S (2 * n + 1))).
@@ -725,9 +724,8 @@ Proof.
   cut (0 <= x).
   intro; apply Rplus_le_le_0_compat; repeat apply Rmult_le_pos;
     assumption || left; prove_sup.
-  unfold x in |- *; replace 0 with (INR 0);
-    [ apply le_INR; apply le_O_n | reflexivity ].
-  prove_sup0.
+  apply pos_INR.
+  now apply IZR_lt.
   ring.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
@@ -735,39 +733,33 @@ Proof.
 Qed.
 
 Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a.
+Proof.
   intros; unfold sin_lb, sin_ub in |- *; apply (sin_bound a 1 H H0).
 Qed.
 
 Lemma COS :
   forall a:R, - PI / 2 <= a -> a <= PI / 2 -> cos_lb a <= cos a <= cos_ub a.
+Proof.
   intros; unfold cos_lb, cos_ub in |- *; apply (cos_bound a 1 H H0).
 Qed.
 
 (**********)
 Lemma _PI2_RLT_0 : - (PI / 2) < 0.
 Proof.
-  rewrite <- Ropp_0; apply Ropp_lt_contravar; apply PI2_RGT_0.
+  assert (H := PI_RGT_0).
+  fourier.
 Qed.
 
 Lemma PI4_RLT_PI2 : PI / 4 < PI / 2.
 Proof.
-  unfold Rdiv in |- *; apply Rmult_lt_compat_l.
-  apply PI_RGT_0.
-  apply Rinv_lt_contravar.
-  apply Rmult_lt_0_compat; prove_sup0.
-  pattern 2 at 1 in |- *; rewrite <- Rplus_0_r.
-  replace 4 with (2 + 2); [ apply Rplus_lt_compat_l; prove_sup0 | ring ].
+  assert (H := PI_RGT_0).
+  fourier.
 Qed.
 
 Lemma PI2_Rlt_PI : PI / 2 < PI.
 Proof.
-  unfold Rdiv in |- *; pattern PI at 2 in |- *; rewrite <- Rmult_1_r.
-  apply Rmult_lt_compat_l.
-  apply PI_RGT_0.
-  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.
+  assert (H := PI_RGT_0).
+  fourier.
 Qed.
 
 (***************************************************)
@@ -784,12 +776,10 @@ Proof.
   rewrite H3; rewrite sin_PI2; apply Rlt_0_1.
   rewrite <- sin_PI_x; generalize (Ropp_gt_lt_contravar x (PI / 2) H3);
     intro H4; generalize (Rplus_lt_compat_l PI (- x) (- (PI / 2)) H4).
-  replace (PI + - x) with (PI - x).
   replace (PI + - (PI / 2)) with (PI / 2).
   intro H5; generalize (Ropp_lt_gt_contravar x PI H0); intro H6;
     change (- PI < - x) in H6; generalize (Rplus_lt_compat_l PI (- PI) (- x) H6).
   rewrite Rplus_opp_r.
-  replace (PI + - x) with (PI - x).
   intro H7;
     elim
       (SIN (PI - x) (Rlt_le 0 (PI - x) H7)
@@ -797,9 +787,7 @@ Proof.
       intros H8 _;
         generalize (sin_lb_gt_0 (PI - x) H7 (Rlt_le (PI - x) (PI / 2) H5));
           intro H9; apply (Rlt_le_trans 0 (sin_lb (PI - x)) (sin (PI - x)) H9 H8).
-  reflexivity.
-  pattern PI at 2 in |- *; rewrite double_var; ring.
-  reflexivity.
+  field.
 Qed.
 
 Theorem cos_gt_0 : forall x:R, - (PI / 2) < x -> x < PI / 2 -> 0 < cos x.
@@ -852,16 +840,12 @@ Proof.
     rewrite <- (Ropp_involutive (cos x)); apply Ropp_le_ge_contravar;
       rewrite <- neg_cos; replace (x + PI) with (x - PI + 2 * INR 1 * PI).
   rewrite cos_period; apply cos_ge_0.
-  replace (- (PI / 2)) with (- PI + PI / 2).
+  replace (- (PI / 2)) with (- PI + PI / 2) by field.
   unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_le_compat_l;
     assumption.
-  pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr;
-    ring.
   unfold Rminus in |- *; rewrite Rplus_comm;
-    replace (PI / 2) with (- PI + 3 * (PI / 2)).
+    replace (PI / 2) with (- PI + 3 * (PI / 2)) by field.
   apply Rplus_le_compat_l; assumption.
-  pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr;
-    ring.
   unfold INR in |- *; ring.
 Qed.
 
@@ -902,16 +886,12 @@ Proof.
     apply Ropp_lt_gt_contravar; rewrite <- neg_cos;
       replace (x + PI) with (x - PI + 2 * INR 1 * PI).
   rewrite cos_period; apply cos_gt_0.
-  replace (- (PI / 2)) with (- PI + PI / 2).
+  replace (- (PI / 2)) with (- PI + PI / 2) by field.
   unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_lt_compat_l;
     assumption.
-  pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr;
-    ring.
   unfold Rminus in |- *; rewrite Rplus_comm;
-    replace (PI / 2) with (- PI + 3 * (PI / 2)).
+    replace (PI / 2) with (- PI + 3 * (PI / 2)) by field.
   apply Rplus_lt_compat_l; assumption.
-  pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr;
-    ring.
   unfold INR in |- *; ring.
 Qed.
 
@@ -948,7 +928,7 @@ Lemma cos_ge_0_3PI2 :
   forall x:R, 3 * (PI / 2) <= x -> x <= 2 * PI -> 0 <= cos x.
 Proof.
   intros; rewrite <- cos_neg; rewrite <- (cos_period (- x) 1);
-    unfold INR in |- *; replace (- x + 2 * 1 * PI) with (2 * PI - x).
+    unfold INR in |- *; replace (- x + 2 * 1 * PI) with (2 * PI - x) by ring.
   generalize (Ropp_le_ge_contravar x (2 * PI) H0); intro H1;
     generalize (Rge_le (- x) (- (2 * PI)) H1); clear H1;
       intro H1; generalize (Rplus_le_compat_l (2 * PI) (- (2 * PI)) (- x) H1).
@@ -957,36 +937,30 @@ Proof.
     generalize (Rge_le (- (3 * (PI / 2))) (- x) H3); clear H3;
       intro H3;
         generalize (Rplus_le_compat_l (2 * PI) (- x) (- (3 * (PI / 2))) H3).
-  replace (2 * PI + - (3 * (PI / 2))) with (PI / 2).
+  replace (2 * PI + - (3 * (PI / 2))) with (PI / 2) by field.
   intro H4;
     apply
       (cos_ge_0 (2 * PI - x)
         (Rlt_le (- (PI / 2)) (2 * PI - x)
           (Rlt_le_trans (- (PI / 2)) 0 (2 * PI - x) _PI2_RLT_0 H2)) H4).
-  rewrite double; pattern PI at 2 3 in |- *; rewrite double_var; ring.
-  ring.
 Qed.
 
 Lemma form1 :
   forall p q:R, cos p + cos q = 2 * cos ((p - q) / 2) * cos ((p + q) / 2).
 Proof.
   intros p q; pattern p at 1 in |- *;
-    replace p with ((p - q) / 2 + (p + q) / 2).
-  rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2).
+    replace p with ((p - q) / 2 + (p + q) / 2) by field.
+  rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field.
   rewrite cos_plus; rewrite cos_minus; ring.
-  pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
-  pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
 Qed.
 
 Lemma form2 :
   forall p q:R, cos p - cos q = -2 * sin ((p - q) / 2) * sin ((p + q) / 2).
 Proof.
   intros p q; pattern p at 1 in |- *;
-    replace p with ((p - q) / 2 + (p + q) / 2).
-  rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2).
+    replace p with ((p - q) / 2 + (p + q) / 2) by field.
+  rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field.
   rewrite cos_plus; rewrite cos_minus; ring.
-  pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
-  pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
 Qed.
 
 Lemma form3 :
@@ -1004,11 +978,9 @@ Lemma form4 :
   forall p q:R, sin p - sin q = 2 * cos ((p + q) / 2) * sin ((p - q) / 2).
 Proof.
   intros p q; pattern p at 1 in |- *;
-    replace p with ((p - q) / 2 + (p + q) / 2).
-  pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2).
+    replace p with ((p - q) / 2 + (p + q) / 2) by field.
+  pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2) by field.
   rewrite sin_plus; rewrite sin_minus; ring.
-  pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
-  pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring.
 
 Qed.
 
@@ -1064,13 +1036,13 @@ Proof.
   repeat rewrite (Rmult_comm (/ 2)).
   clear H4; intro H4;
     generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) y H H1);
-      replace (- (PI / 2) + - (PI / 2)) with (- PI).
+      replace (- (PI / 2) + - (PI / 2)) with (- PI) by field.
   intro H5;
     generalize
       (Rmult_le_compat_l (/ 2) (- PI) (x + y)
         (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H5).
-  replace (/ 2 * (x + y)) with ((x + y) / 2).
-  replace (/ 2 * - PI) with (- (PI / 2)).
+  replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm.
+  replace (/ 2 * - PI) with (- (PI / 2)) by field.
   clear H5; intro H5; elim H4; intro H40.
   elim H5; intro H50.
   generalize (cos_gt_0 ((x + y) / 2) H50 H40); intro H6;
@@ -1092,13 +1064,6 @@ Proof.
   rewrite H40 in H3; assert (H50 := cos_PI2); unfold Rdiv in H50;
     rewrite H50 in H3; rewrite Rmult_0_r in H3; rewrite Rmult_0_l in H3;
       elim (Rlt_irrefl 0 H3).
-  unfold Rdiv in |- *.
-  rewrite <- Ropp_mult_distr_l_reverse.
-  apply Rmult_comm.
-  unfold Rdiv in |- *; apply Rmult_comm.
-  pattern PI at 1 in |- *; rewrite double_var.
-  rewrite Ropp_plus_distr.
-  reflexivity.
 Qed.
 
 Lemma sin_increasing_1 :
@@ -1108,43 +1073,42 @@ Lemma sin_increasing_1 :
 Proof.
   intros; generalize (Rplus_lt_compat_l x x y H3); intro H4;
     generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) x H H);
-      replace (- (PI / 2) + - (PI / 2)) with (- PI).
+      replace (- (PI / 2) + - (PI / 2)) with (- PI) by field.
   assert (Hyp : 0 < 2).
   prove_sup0.
   intro H5; generalize (Rle_lt_trans (- PI) (x + x) (x + y) H5 H4); intro H6;
     generalize
       (Rmult_lt_compat_l (/ 2) (- PI) (x + y) (Rinv_0_lt_compat 2 Hyp) H6);
-      replace (/ 2 * - PI) with (- (PI / 2)).
-  replace (/ 2 * (x + y)) with ((x + y) / 2).
+      replace (/ 2 * - PI) with (- (PI / 2)) by field.
+  replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm.
   clear H4 H5 H6; intro H4; generalize (Rplus_lt_compat_l y x y H3); intro H5;
     rewrite Rplus_comm in H5;
       generalize (Rplus_le_compat y (PI / 2) y (PI / 2) H2 H2).
   rewrite <- double_var.
   intro H6; generalize (Rlt_le_trans (x + y) (y + y) PI H5 H6); intro H7;
     generalize (Rmult_lt_compat_l (/ 2) (x + y) PI (Rinv_0_lt_compat 2 Hyp) H7);
-      replace (/ 2 * PI) with (PI / 2).
-  replace (/ 2 * (x + y)) with ((x + y) / 2).
+      replace (/ 2 * PI) with (PI / 2) by apply Rmult_comm.
+  replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm.
   clear H5 H6 H7; intro H5; generalize (Ropp_le_ge_contravar (- (PI / 2)) y H1);
     rewrite Ropp_involutive; clear H1; intro H1;
       generalize (Rge_le (PI / 2) (- y) H1); clear H1; intro H1;
         generalize (Ropp_le_ge_contravar y (PI / 2) H2); clear H2;
           intro H2; generalize (Rge_le (- y) (- (PI / 2)) H2);
             clear H2; intro H2; generalize (Rplus_lt_compat_l (- y) x y H3);
-              replace (- y + x) with (x - y).
+              replace (- y + x) with (x - y) by apply Rplus_comm.
   rewrite Rplus_opp_l.
   intro H6;
     generalize (Rmult_lt_compat_l (/ 2) (x - y) 0 (Rinv_0_lt_compat 2 Hyp) H6);
-      rewrite Rmult_0_r; replace (/ 2 * (x - y)) with ((x - y) / 2).
+      rewrite Rmult_0_r; replace (/ 2 * (x - y)) with ((x - y) / 2) by apply Rmult_comm.
   clear H6; intro H6;
     generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) (- y) H H2);
-      replace (- (PI / 2) + - (PI / 2)) with (- PI).
-  replace (x + - y) with (x - y).
+      replace (- (PI / 2) + - (PI / 2)) with (- PI) by field.
   intro H7;
     generalize
       (Rmult_le_compat_l (/ 2) (- PI) (x - y)
         (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H7);
-      replace (/ 2 * - PI) with (- (PI / 2)).
-  replace (/ 2 * (x - y)) with ((x - y) / 2).
+      replace (/ 2 * - PI) with (- (PI / 2)) by field.
+  replace (/ 2 * (x - y)) with ((x - y) / 2) by apply Rmult_comm.
   clear H7; intro H7; clear H H0 H1 H2; apply Rminus_lt; rewrite form4;
     generalize (cos_gt_0 ((x + y) / 2) H4 H5); intro H8;
       generalize (Rmult_lt_0_compat 2 (cos ((x + y) / 2)) Hyp H8);
@@ -1159,23 +1123,6 @@ Proof.
             2 * cos ((x + y) / 2)) H10 H8); intro H11; rewrite Rmult_0_r in H11;
           rewrite Rmult_comm; assumption.
   apply Ropp_lt_gt_contravar; apply PI2_Rlt_PI.
-  unfold Rdiv in |- *; apply Rmult_comm.
-  unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse; apply Rmult_comm.
-  reflexivity.
-  pattern PI at 1 in |- *; rewrite double_var.
-  rewrite Ropp_plus_distr.
-  reflexivity.
-  unfold Rdiv in |- *; apply Rmult_comm.
-  unfold Rminus in |- *; apply Rplus_comm.
-  unfold Rdiv in |- *; apply Rmult_comm.
-  unfold Rdiv in |- *; apply Rmult_comm.
-  unfold Rdiv in |- *; apply Rmult_comm.
-  unfold Rdiv in |- *.
-  rewrite <- Ropp_mult_distr_l_reverse.
-  apply Rmult_comm.
-  pattern PI at 1 in |- *; rewrite double_var.
-  rewrite Ropp_plus_distr.
-  reflexivity.
 Qed.
 
 Lemma sin_decreasing_0 :
@@ -1190,33 +1137,16 @@ Proof.
           generalize (Rplus_le_compat_l (- PI) (PI / 2) x H0);
             generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1);
               generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2);
-                replace (- PI + x) with (x - PI).
-  replace (- PI + PI / 2) with (- (PI / 2)).
-  replace (- PI + y) with (y - PI).
-  replace (- PI + 3 * (PI / 2)) with (PI / 2).
-  replace (- (PI - x)) with (x - PI).
-  replace (- (PI - y)) with (y - PI).
+                replace (- PI + x) with (x - PI) by apply Rplus_comm.
+  replace (- PI + PI / 2) with (- (PI / 2)) by field.
+  replace (- PI + y) with (y - PI) by apply Rplus_comm.
+  replace (- PI + 3 * (PI / 2)) with (PI / 2) by field.
+  replace (- (PI - x)) with (x - PI) by ring.
+  replace (- (PI - y)) with (y - PI) by ring.
   intros; change (sin (y - PI) < sin (x - PI)) in H8;
-    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 Rplus_lt_reg_l with (- PI); rewrite Rplus_comm.
+  rewrite (Rplus_comm _ x).
   apply (sin_increasing_0 (y - PI) (x - PI) H4 H5 H6 H7 H8).
-  reflexivity.
-  reflexivity.
-  unfold Rminus in |- *; rewrite Ropp_plus_distr.
-  rewrite Ropp_involutive.
-  apply Rplus_comm.
-  unfold Rminus in |- *; rewrite Ropp_plus_distr.
-  rewrite Ropp_involutive.
-  apply Rplus_comm.
-  pattern PI at 2 in |- *; rewrite double_var.
-  rewrite Ropp_plus_distr.
-  ring.
-  unfold Rminus in |- *; apply Rplus_comm.
-  pattern PI at 2 in |- *; rewrite double_var.
-  rewrite Ropp_plus_distr.
-  ring.
-  unfold Rminus in |- *; apply Rplus_comm.
 Qed.
 
 Lemma sin_decreasing_1 :
@@ -1230,24 +1160,14 @@ Proof.
         generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1);
           generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2);
             generalize (Rplus_lt_compat_l (- PI) x y H3);
-              replace (- PI + PI / 2) with (- (PI / 2)).
-  replace (- PI + y) with (y - PI).
-  replace (- PI + 3 * (PI / 2)) with (PI / 2).
-  replace (- PI + x) with (x - PI).
+              replace (- PI + PI / 2) with (- (PI / 2)) by field.
+  replace (- PI + y) with (y - PI) by apply Rplus_comm.
+  replace (- PI + 3 * (PI / 2)) with (PI / 2) by field.
+  replace (- PI + x) with (x - PI) by apply Rplus_comm.
   intros; apply Ropp_lt_cancel; repeat rewrite <- sin_neg;
-    replace (- (PI - x)) with (x - PI).
-  replace (- (PI - y)) with (y - PI).
+    replace (- (PI - x)) with (x - PI) by ring.
+  replace (- (PI - y)) with (y - PI) by ring.
   apply (sin_increasing_1 (x - PI) (y - PI) H7 H8 H5 H6 H4).
-  unfold Rminus in |- *; rewrite Ropp_plus_distr.
-  rewrite Ropp_involutive.
-  apply Rplus_comm.
-  unfold Rminus in |- *; rewrite Ropp_plus_distr.
-  rewrite Ropp_involutive.
-  apply Rplus_comm.
-  unfold Rminus in |- *; apply Rplus_comm.
-  pattern PI at 2 in |- *; rewrite double_var; ring.
-  unfold Rminus in |- *; apply Rplus_comm.
-  pattern PI at 2 in |- *; rewrite double_var; ring.
 Qed.
 
 Lemma cos_increasing_0 :
@@ -1287,31 +1207,16 @@ Proof.
             generalize (Rplus_lt_compat_l (-3 * (PI / 2)) x y H5);
               rewrite <- (cos_neg x); rewrite <- (cos_neg y);
                 rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1);
-                  unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)).
-  replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)).
-  replace (-3 * (PI / 2) + PI) with (- (PI / 2)).
-  replace (-3 * (PI / 2) + 2 * PI) with (PI / 2).
+                  unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring.
+  replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring.
+  replace (-3 * (PI / 2) + PI) with (- (PI / 2)) by field.
+  replace (-3 * (PI / 2) + 2 * PI) with (PI / 2) by field.
   clear H1 H2 H3 H4 H5; intros H1 H2 H3 H4 H5;
-    replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))).
-  replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))).
+    replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))) by field.
+  replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))) by field.
   repeat rewrite cos_shift;
     apply
       (sin_increasing_1 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H5 H4 H3 H2 H1).
-  rewrite Rmult_1_r.
-  rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var.
-  ring.
-  rewrite Rmult_1_r.
-  rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var.
-  ring.
-  rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var.
-  ring.
-  pattern PI at 3 in |- *; rewrite double_var; ring.
-  unfold Rminus in |- *.
-  rewrite <- Ropp_mult_distr_l_reverse.
-  apply Rplus_comm.
-  unfold Rminus in |- *.
-  rewrite <- Ropp_mult_distr_l_reverse.
-  apply Rplus_comm.
 Qed.
 
 Lemma cos_decreasing_0 :
@@ -1350,31 +1255,8 @@ Lemma tan_diff :
     cos x <> 0 -> cos y <> 0 -> tan x - tan y = sin (x - y) / (cos x * cos y).
 Proof.
   intros; unfold tan in |- *; rewrite sin_minus.
-  unfold Rdiv in |- *.
-  unfold Rminus in |- *.
-  rewrite Rmult_plus_distr_r.
-  rewrite Rinv_mult_distr.
-  repeat rewrite (Rmult_comm (sin x)).
-  repeat rewrite Rmult_assoc.
-  rewrite (Rmult_comm (cos y)).
-  repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r.
-  rewrite (Rmult_comm (sin x)).
-  apply Rplus_eq_compat_l.
-  rewrite <- Ropp_mult_distr_l_reverse.
-  rewrite <- Ropp_mult_distr_r_reverse.
-  rewrite (Rmult_comm (/ cos x)).
-  repeat rewrite Rmult_assoc.
-  rewrite (Rmult_comm (cos x)).
-  repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r.
-  reflexivity.
-  assumption.
-  assumption.
-  assumption.
-  assumption.
+  field.
+  now split.
 Qed.
 
 Lemma tan_increasing_0 :
@@ -1411,10 +1293,9 @@ Proof.
         intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11);
           clear H11; intro H11;
             generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11);
-              generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10);
-                replace (x + - y) with (x - y).
-  replace (PI / 4 + PI / 4) with (PI / 2).
-  replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)).
+              generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10).
+  replace (PI / 4 + PI / 4) with (PI / 2) by field.
+  replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field.
   intros; case (Rtotal_order 0 (x - y)); intro H14.
   generalize
     (sin_gt_0 (x - y) H14 (Rle_lt_trans (x - y) (PI / 2) PI H12 PI2_Rlt_PI));
@@ -1422,28 +1303,6 @@ Proof.
   elim H14; intro H15.
   rewrite <- H15 in H9; rewrite sin_0 in H9; elim (Rlt_irrefl 0 H9).
   apply Rminus_lt; assumption.
-  pattern PI at 1 in |- *; rewrite double_var.
-  unfold Rdiv in |- *.
-  rewrite Rmult_plus_distr_r.
-  repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_mult_distr.
-  rewrite Ropp_plus_distr.
-  replace 4 with 4.
-  reflexivity.
-  ring.
-  discrR.
-  discrR.
-  pattern PI at 1 in |- *; rewrite double_var.
-  unfold Rdiv in |- *.
-  rewrite Rmult_plus_distr_r.
-  repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_mult_distr.
-  replace 4 with 4.
-  reflexivity.
-  ring.
-  discrR.
-  discrR.
-  reflexivity.
   case (Rcase_abs (sin (x - y))); intro H9.
   assumption.
   generalize (Rge_le (sin (x - y)) 0 H9); clear H9; intro H9;
@@ -1457,8 +1316,7 @@ Proof.
         (Rlt_le 0 (/ (cos x * cos y)) H12)); intro H13;
       elim
         (Rlt_irrefl 0 (Rle_lt_trans 0 (sin (x - y) * / (cos x * cos y)) 0 H13 H3)).
-  rewrite Rinv_mult_distr.
-  reflexivity.
+  apply Rinv_mult_distr.
   assumption.
   assumption.
 Qed.
@@ -1496,9 +1354,8 @@ Proof.
   clear H10 H11; intro H8; generalize (Ropp_le_ge_contravar y (PI / 4) H2);
     intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11);
       clear H11; intro H11;
-        generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11);
-          replace (x + - y) with (x - y).
-  replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)).
+        generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11).
+  replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field.
   clear H11; intro H9; generalize (Rlt_minus x y H3); clear H3; intro H3;
     clear H H0 H1 H2 H4 H5 HP1 HP2; generalize PI2_Rlt_PI;
       intro H1; generalize (Ropp_lt_gt_contravar (PI / 2) PI H1);
@@ -1509,18 +1366,6 @@ Proof.
               generalize
                 (Rmult_lt_gt_compat_neg_l (sin (x - y)) 0 (/ (cos x * cos y)) H2 H8);
                 rewrite Rmult_0_r; intro H4; assumption.
-  pattern PI at 1 in |- *; rewrite double_var.
-  unfold Rdiv in |- *.
-  rewrite Rmult_plus_distr_r.
-  repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_mult_distr.
-  replace 4 with 4.
-  rewrite Ropp_plus_distr.
-  reflexivity.
-  ring.
-  discrR.
-  discrR.
-  reflexivity.
   apply Rinv_mult_distr; assumption.
 Qed.
 
@@ -1762,8 +1607,7 @@ Proof.
   rewrite Rplus_0_r.
   rewrite Ropp_Ropp_IZR.
   rewrite Rplus_opp_r.
-  left; replace 0 with (IZR 0); [ apply IZR_lt | reflexivity ].
-  assumption.
+  now apply Rlt_le, IZR_lt.
   rewrite <- sin_neg.
   rewrite Ropp_mult_distr_l_reverse.
   rewrite Ropp_involutive.
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index 092bc30d0..55cb74e35 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -99,24 +99,22 @@ Proof.
   apply Rle_trans with 20.
   apply Rle_trans with 16.
   replace 16 with (Rsqr 4); [ idtac | ring_Rsqr ].
-  replace (a * a) with (Rsqr a); [ idtac | reflexivity ].
   apply Rsqr_incr_1.
   assumption.
   assumption.
-  left; prove_sup0.
-  rewrite <- (Rplus_0_r 16); replace 20 with (16 + 4);
-    [ apply Rplus_le_compat_l; left; prove_sup0 | ring ].
-  rewrite <- (Rplus_comm 20); pattern 20 at 1; rewrite <- Rplus_0_r;
-    apply Rplus_le_compat_l.
+  now apply IZR_le.
+  now apply IZR_le.
+  rewrite <- (Rplus_0_l 20) at 1;
+    apply Rplus_le_compat_r.
   apply Rplus_le_le_0_compat.
-  repeat apply Rmult_le_pos.
-  left; prove_sup0.
-  left; prove_sup0.
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
   apply Rmult_le_pos.
-  left; prove_sup0.
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
+  apply Rmult_le_pos.
+  now apply IZR_le.
+  apply pos_INR.
+  apply pos_INR.
+  apply Rmult_le_pos.
+  now apply IZR_le.
+  apply pos_INR.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   simpl; ring.
@@ -182,16 +180,14 @@ Proof.
   replace (- sum_f_R0 (tg_alt Un) (S (2 * n))) with
   (-1 * sum_f_R0 (tg_alt Un) (S (2 * n))); [ rewrite scal_sum | ring ].
   apply sum_eq; intros; unfold sin_term, Un, tg_alt;
-    replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+    change ((-1) ^ S i) with (-1 * (-1) ^ i).
   unfold Rdiv; ring.
-  reflexivity.
   replace (- sum_f_R0 (tg_alt Un) (2 * n)) with
   (-1 * sum_f_R0 (tg_alt Un) (2 * n)); [ rewrite scal_sum | ring ].
   apply sum_eq; intros.
   unfold sin_term, Un, tg_alt;
-    replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+    change ((-1) ^ S i) with (-1 * (-1) ^ i).
   unfold Rdiv; ring.
-  reflexivity.
   replace (2 * (n + 1))%nat with (S (S (2 * n))).
   reflexivity.
   ring.
@@ -279,26 +275,23 @@ Proof.
     with (4 * INR n1 * INR n1 + 14 * INR n1 + 12); [ idtac | ring ].
   apply Rle_trans with 12.
   apply Rle_trans with 4.
-  replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ].
-  replace (a0 * a0) with (Rsqr a0); [ idtac | reflexivity ].
+  change 4 with (Rsqr 2).
   apply Rsqr_incr_1.
   assumption.
-  discrR.
   assumption.
-  left; prove_sup0.
-  pattern 4 at 1; rewrite <- Rplus_0_r; replace 12 with (4 + 8);
-    [ apply Rplus_le_compat_l; left; prove_sup0 | ring ].
-  rewrite <- (Rplus_comm 12); pattern 12 at 1; rewrite <- Rplus_0_r;
-    apply Rplus_le_compat_l.
+  now apply IZR_le.
+  now apply IZR_le.
+  rewrite <- (Rplus_0_l 12) at 1;
+    apply Rplus_le_compat_r.
   apply Rplus_le_le_0_compat.
-  repeat apply Rmult_le_pos.
-  left; prove_sup0.
-  left; prove_sup0.
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
   apply Rmult_le_pos.
-  left; prove_sup0.
-  replace 0 with (INR 0); [ apply le_INR; apply le_O_n | reflexivity ].
+  apply Rmult_le_pos.
+  now apply IZR_le.
+  apply pos_INR.
+  apply pos_INR.
+  apply Rmult_le_pos.
+  now apply IZR_le.
+  apply pos_INR.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   simpl; ring.
@@ -351,15 +344,13 @@ Proof.
   replace (- sum_f_R0 (tg_alt Un) (S (2 * n0))) with
   (-1 * sum_f_R0 (tg_alt Un) (S (2 * n0))); [ rewrite scal_sum | ring ].
   apply sum_eq; intros; unfold cos_term, Un, tg_alt;
-    replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+    change ((-1) ^ S i) with (-1 * (-1) ^ i).
   unfold Rdiv; ring.
-  reflexivity.
   replace (- sum_f_R0 (tg_alt Un) (2 * n0)) with
   (-1 * sum_f_R0 (tg_alt Un) (2 * n0)); [ rewrite scal_sum | ring ];
   apply sum_eq; intros; unfold cos_term, Un, tg_alt;
-    replace ((-1) ^ S i) with (-1 * (-1) ^ i).
+    change ((-1) ^ S i) with (-1 * (-1) ^ i).
   unfold Rdiv; ring.
-  reflexivity.
   replace (2 * (n0 + 1))%nat with (S (S (2 * n0))).
   reflexivity.
   ring.
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v
index 0d2a9a8ba..b46df202e 100644
--- a/theories/Reals/Rtrigo_def.v
+++ b/theories/Reals/Rtrigo_def.v
@@ -157,7 +157,7 @@ Proof.
   apply Rinv_0_lt_compat; assumption.
   rewrite H3 in H0; assumption.
   apply lt_le_trans with 1%nat; [ apply lt_O_Sn | apply le_max_r ].
-  apply le_IZR; replace (IZR 0) with 0; [ idtac | reflexivity ]; left;
+  apply le_IZR; left;
     apply Rlt_trans with (/ eps);
       [ apply Rinv_0_lt_compat; assumption | assumption ].
   assert (H0 := archimed (/ eps)).
@@ -194,30 +194,27 @@ Proof.
   elim H1; intros; assumption.
   apply lt_le_trans with (S n).
   unfold ge in H2; apply le_lt_n_Sm; assumption.
-  replace (2 * n + 1)%nat with (S (2 * n)); [ idtac | ring ].
+  replace (2 * n + 1)%nat with (S (2 * n)) by ring.
   apply le_n_S; apply le_n_2n.
   apply Rmult_lt_reg_l with (INR (2 * S n)).
   apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n))).
   apply lt_O_Sn.
-  replace (S n) with (n + 1)%nat; [ idtac | ring ].
+  replace (S n) with (n + 1)%nat by ring.
   ring.
   rewrite <- Rinv_r_sym.
-  rewrite Rmult_1_r; replace 1 with (INR 1); [ apply lt_INR | reflexivity ].
+  rewrite Rmult_1_r.
+  apply (lt_INR 1).
   replace (2 * S n)%nat with (S (S (2 * n))).
   apply lt_n_S; apply lt_O_Sn.
-  replace (S n) with (n + 1)%nat; [ ring | ring ].
+  ring.
   apply not_O_INR; discriminate.
   apply not_O_INR; discriminate.
   replace (2 * n + 1)%nat with (S (2 * n));
   [ apply not_O_INR; discriminate | ring ].
   apply Rle_ge; left; apply Rinv_0_lt_compat.
   apply lt_INR_0.
-  replace (2 * S n * (2 * n + 1))%nat with (S (S (4 * (n * n) + 6 * n))).
+  replace (2 * S n * (2 * n + 1))%nat with (2 + (4 * (n * n) + 6 * n))%nat by ring.
   apply lt_O_Sn.
-  apply INR_eq.
-  repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR;
-    rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR;
-      replace (INR 0) with 0; [ ring | reflexivity ].
 Qed.
 
 Lemma cosn_no_R0 : forall n:nat, cos_n n <> 0.
@@ -318,28 +315,25 @@ Proof.
   elim H1; intros; assumption.
   apply lt_le_trans with (S n).
   unfold ge in H2; apply le_lt_n_Sm; assumption.
-  replace (2 * S n + 1)%nat with (S (2 * S n)); [ idtac | ring ].
+  replace (2 * S n + 1)%nat with (S (2 * S n)) by ring.
   apply le_S; apply le_n_2n.
   apply Rmult_lt_reg_l with (INR (2 * S n)).
   apply lt_INR_0; replace (2 * S n)%nat with (S (S (2 * n)));
-    [ apply lt_O_Sn | replace (S n) with (n + 1)%nat; [ idtac | ring ]; ring ].
+    [ apply lt_O_Sn | ring ].
   rewrite <- Rinv_r_sym.
-  rewrite Rmult_1_r; replace 1 with (INR 1); [ apply lt_INR | reflexivity ].
+  rewrite Rmult_1_r.
+  apply (lt_INR 1).
   replace (2 * S n)%nat with (S (S (2 * n))).
   apply lt_n_S; apply lt_O_Sn.
-  replace (S n) with (n + 1)%nat; [ ring | ring ].
+  ring.
   apply not_O_INR; discriminate.
   apply not_O_INR; discriminate.
   apply not_O_INR; discriminate.
-  left; change (0 < / INR ((2 * S n + 1) * (2 * S n)));
-    apply Rinv_0_lt_compat.
+  left; apply Rinv_0_lt_compat.
   apply lt_INR_0.
   replace ((2 * S n + 1) * (2 * S n))%nat with
-  (S (S (S (S (S (S (4 * (n * n) + 10 * n))))))).
+  (6 + (4 * (n * n) + 10 * n))%nat by ring.
   apply lt_O_Sn.
-  apply INR_eq; repeat rewrite S_INR; rewrite plus_INR; repeat rewrite mult_INR;
-    rewrite plus_INR; rewrite mult_INR; repeat rewrite S_INR;
-      replace (INR 0) with 0; [ ring | reflexivity ].
 Qed.
 
 Lemma sin_no_R0 : forall n:nat, sin_n n <> 0.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 5a2a07c42..3697999f7 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -1167,7 +1167,7 @@ Proof.
   assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros.
   rewrite H4 in H7; rewrite <- INR_IZR_INZ in H7.
   simpl in H7; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H2 H7)).
-  replace 1 with (INR 1); [ apply le_INR | reflexivity ]; apply le_n_S;
+  apply (le_INR 1); apply le_n_S;
     apply le_O_n.
   apply le_IZR; simpl; left; apply Rlt_trans with (Rabs x).
   assumption.