Simplify some proofs using ring and field.

10 files changed, 99 insertions, 394 deletions

diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 379fee6f4..07bcd9836 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -2017,42 +2017,18 @@ Qed.
 Lemma le_epsilon :
   forall r1 r2, (forall eps:R, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2.
 Proof.
-  intros x y; intros; elim (Rtotal_order x y); intro.
-  left; assumption.
-  elim H0; intro.
-  right; assumption.
-  clear H0; generalize (Rgt_minus x y H1); intro H2; change (0 < x - y) in H2.
-  cut (0 < 2).
-  intro.
-  generalize (Rmult_lt_0_compat (x - y) (/ 2) H2 (Rinv_0_lt_compat 2 H0));
-    intro H3; generalize (H ((x - y) * / 2) H3);
-      replace (y + (x - y) * / 2) with ((y + x) * / 2).
-  intro H4;
-    generalize (Rmult_le_compat_l 2 x ((y + x) * / 2) (Rlt_le 0 2 H0) H4);
-      rewrite <- (Rmult_comm ((y + x) * / 2)); rewrite Rmult_assoc;
-        rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r; replace (2 * x) with (x + x).
-  rewrite (Rplus_comm y); intro H5; apply Rplus_le_reg_l with x; assumption.
-  ring.
-  replace 2 with (INR 2); [ apply not_0_INR; discriminate | reflexivity ].
-  pattern y at 2; replace y with (y / 2 + y / 2).
-  unfold Rminus, Rdiv.
-  repeat rewrite Rmult_plus_distr_r.
-  ring.
-  cut (forall z:R, 2 * z = z + z).
-  intro.
-  rewrite <- (H4 (y / 2)).
-  unfold Rdiv.
-  rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
-  replace 2 with (INR 2).
-  apply not_0_INR.
-  discriminate.
-  unfold INR; reflexivity.
-  intro; ring.
-  cut (0%nat <> 2%nat);
-    [ intro H0; generalize (lt_0_INR 2 (neq_O_lt 2 H0)); unfold INR;
-      intro; assumption
-      | discriminate ].
+  intros x y H.
+  destruct (Rle_or_lt x y) as [H1|H1].
+  exact H1.
+  apply Rplus_le_reg_r with x.
+  replace (y + x) with (2 * (y + (x - y) * / 2)) by field.
+  replace (x + x) with (2 * x) by ring.
+  apply Rmult_le_compat_l.
+  now apply (IZR_le 0 2).
+  apply H.
+  apply Rmult_lt_0_compat.
+  now apply Rgt_minus.
+  apply Rinv_0_lt_compat, Rlt_0_2.
 Qed.
 
 (**********)
diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index 445ffcb21..a8937e36f 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -296,56 +296,9 @@ Lemma canonical_Rsqr :
     a * Rsqr (x + b / (2 * a)) + (4 * a * c - Rsqr b) / (4 * a).
 Proof.
   intros.
-  rewrite Rsqr_plus.
-  repeat rewrite Rmult_plus_distr_l.
-  repeat rewrite Rplus_assoc.
-  apply Rplus_eq_compat_l.
-  unfold Rdiv, Rminus.
-  replace (2 * 1 + 2 * 1) with 4; [ idtac | ring ].
-  rewrite (Rmult_plus_distr_r (4 * a * c) (- Rsqr b) (/ (4 * a))).
-  rewrite Rsqr_mult.
-  repeat rewrite Rinv_mult_distr.
-  repeat rewrite (Rmult_comm a).
-  repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r.
-  rewrite (Rmult_comm 2).
-  repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r.
-  rewrite (Rmult_comm (/ 2)).
-  rewrite (Rmult_comm 2).
-  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r.
-  rewrite (Rmult_comm a).
-  repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r.
-  rewrite (Rmult_comm 2).
-  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r.
-  repeat rewrite Rplus_assoc.
-  rewrite (Rplus_comm (Rsqr b * (Rsqr (/ a * / 2) * a))).
-  repeat rewrite Rplus_assoc.
-  rewrite (Rmult_comm x).
-  apply Rplus_eq_compat_l.
-  rewrite (Rmult_comm (/ a)).
-  unfold Rsqr; repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r.
-  ring.
-  apply (cond_nonzero a).
-  discrR.
-  apply (cond_nonzero a).
-  discrR.
-  discrR.
-  apply (cond_nonzero a).
-  discrR.
-  discrR.
-  discrR.
-  apply (cond_nonzero a).
-  discrR.
-  apply (cond_nonzero a).
+  unfold Rsqr.
+  field.
+  apply a.
 Qed.
 
 Lemma Rsqr_eq : forall x y:R, Rsqr x = Rsqr y -> x = y \/ x = - y.
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index a6b1a26e0..5c975c3f5 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -359,107 +359,22 @@ Lemma Rsqr_sol_eq_0_1 :
     x = sol_x1 a b c \/ x = sol_x2 a b c -> a * Rsqr x + b * x + c = 0.
 Proof.
   intros; elim H0; intro.
-  unfold sol_x1 in H1; unfold Delta in H1; rewrite H1; unfold Rdiv;
-    repeat rewrite Rsqr_mult; rewrite Rsqr_plus; rewrite <- Rsqr_neg;
-      rewrite Rsqr_sqrt.
-  rewrite Rsqr_inv.
-  unfold Rsqr; repeat rewrite Rinv_mult_distr.
-  repeat rewrite Rmult_assoc; rewrite (Rmult_comm a).
-  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r; rewrite Rmult_plus_distr_r.
-  repeat rewrite Rmult_assoc.
-  pattern 2 at 2; rewrite (Rmult_comm 2).
-  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r.
-  rewrite
-    (Rmult_plus_distr_r (- b) (sqrt (b * b - 2 * (2 * (a * c)))) (/ 2 * / a))
-    .
-  rewrite Rmult_plus_distr_l; repeat rewrite Rplus_assoc.
-  replace
-  (- b * (sqrt (b * b - 2 * (2 * (a * c))) * (/ 2 * / a)) +
-    (b * (- b * (/ 2 * / a)) +
-      (b * (sqrt (b * b - 2 * (2 * (a * c))) * (/ 2 * / a)) + c))) with
-  (b * (- b * (/ 2 * / a)) + c).
-  unfold Rminus; repeat rewrite <- Rplus_assoc.
-  replace (b * b + b * b) with (2 * (b * b)).
-  rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc.
-  rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r.
-  rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc;
-    rewrite (Rmult_comm 2).
-  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r; rewrite (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc;
-    rewrite (Rmult_comm 2).
-  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r; repeat rewrite Rmult_assoc.
-  rewrite (Rmult_comm a); rewrite Rmult_assoc.
-  rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r; rewrite <- Rmult_opp_opp.
-  ring.
-  apply (cond_nonzero a).
-  discrR.
-  discrR.
-  discrR.
-  ring.
-  ring.
-  discrR.
-  apply (cond_nonzero a).
-  discrR.
-  apply (cond_nonzero a).
-  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
-  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
-  apply prod_neq_R0; [ discrR | apply (cond_nonzero a) ].
-  assumption.
-  unfold sol_x2 in H1; unfold Delta in H1; rewrite H1; unfold Rdiv;
-    repeat rewrite Rsqr_mult; rewrite Rsqr_minus; rewrite <- Rsqr_neg;
-      rewrite Rsqr_sqrt.
-  rewrite Rsqr_inv.
-  unfold Rsqr; repeat rewrite Rinv_mult_distr;
-    repeat rewrite Rmult_assoc.
-  rewrite (Rmult_comm a); repeat rewrite Rmult_assoc.
-  rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r; unfold Rminus; rewrite Rmult_plus_distr_r.
-  rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc;
-    pattern 2 at 2; rewrite (Rmult_comm 2).
-  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r;
-    rewrite
-      (Rmult_plus_distr_r (- b) (- sqrt (b * b + - (2 * (2 * (a * c)))))
-        (/ 2 * / a)).
-  rewrite Rmult_plus_distr_l; repeat rewrite Rplus_assoc.
-  rewrite Ropp_mult_distr_l_reverse; rewrite Ropp_involutive.
-  replace
-  (b * (sqrt (b * b + - (2 * (2 * (a * c)))) * (/ 2 * / a)) +
-    (b * (- b * (/ 2 * / a)) +
-      (b * (- sqrt (b * b + - (2 * (2 * (a * c)))) * (/ 2 * / a)) + c))) with
-  (b * (- b * (/ 2 * / a)) + c).
-  repeat rewrite <- Rplus_assoc; replace (b * b + b * b) with (2 * (b * b)).
-  rewrite Rmult_plus_distr_r; repeat rewrite Rmult_assoc;
-    rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc;
-      rewrite <- Rinv_l_sym.
-  rewrite Ropp_mult_distr_l_reverse; repeat rewrite Rmult_assoc.
-  rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r; rewrite (Rmult_comm (/ 2)); repeat rewrite Rmult_assoc.
-  rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r; repeat rewrite Rmult_assoc; rewrite (Rmult_comm a);
-    rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
-  rewrite Rmult_1_r; rewrite <- Rmult_opp_opp; ring.
-  apply (cond_nonzero a).
-  discrR.
-  discrR.
-  discrR.
-  ring.
-  ring.
-  discrR.
-  apply (cond_nonzero a).
-  discrR.
-  discrR.
-  apply (cond_nonzero a).
-  apply prod_neq_R0; discrR || apply (cond_nonzero a).
-  apply prod_neq_R0; discrR || apply (cond_nonzero a).
-  apply prod_neq_R0; discrR || apply (cond_nonzero a).
-  assumption.
+  rewrite H1.
+  unfold sol_x1, Delta, Rsqr.
+  field_simplify.
+  rewrite <- (Rsqr_pow2 (sqrt _)), Rsqr_sqrt.
+  field.
+  apply a.
+  apply H.
+  apply a.
+  rewrite H1.
+  unfold sol_x2, Delta, Rsqr.
+  field_simplify.
+  rewrite <- (Rsqr_pow2 (sqrt _)), Rsqr_sqrt.
+  field.
+  apply a.
+  apply H.
+  apply a.
 Qed.
 
 Lemma Rsqr_sol_eq_0_0 :
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index 661bc8c76..23daedb8b 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -130,15 +130,8 @@ Proof.
   intro; exists (mkposreal (- x) H1); intros.
   rewrite (Rabs_left x).
   rewrite (Rabs_left (x + h)).
-  rewrite Rplus_comm.
-  rewrite Ropp_plus_distr.
-  unfold Rminus; rewrite Ropp_involutive; rewrite Rplus_assoc;
-    rewrite Rplus_opp_l.
-  rewrite Rplus_0_r; unfold Rdiv.
-  rewrite Ropp_mult_distr_l_reverse.
-  rewrite <- Rinv_r_sym.
-  rewrite Ropp_involutive; rewrite Rplus_opp_l; rewrite Rabs_R0; apply H0.
-  apply H2.
+  replace ((-(x + h) - - x) / h - -1) with 0 by now field.
+  rewrite Rabs_R0; apply H0.
   destruct (Rcase_abs h) as [Hlt|Hgt].
   apply Ropp_lt_cancel.
   rewrite Ropp_0; rewrite Ropp_plus_distr; apply Rplus_lt_0_compat.
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index bd330ac9b..5fb6bd2b7 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.v
@@ -296,14 +296,10 @@ Proof.
       intros; generalize (H0 eps H1); clear H0; intro; elim H0;
         clear H0; intros; elim H0; clear H0; simpl;
           intros; split with x; split; auto.
-  intros; generalize (H2 x1 H3); clear H2; intro;
-    rewrite Ropp_mult_distr_l_reverse in H2;
-      rewrite Ropp_mult_distr_l_reverse in H2;
-        rewrite Ropp_mult_distr_l_reverse in H2;
-          rewrite (let (H1, H2) := Rmult_ne (f x1) in H2) in H2;
-            rewrite (let (H1, H2) := Rmult_ne (f x0) in H2) in H2;
-              rewrite (let (H1, H2) := Rmult_ne (df x0) in H2) in H2;
-                assumption.
+  intros; generalize (H2 x1 H3); clear H2; intro.
+  replace (- f x1 - - f x0) with (-1 * f x1 - -1 * f x0) by ring.
+  replace (- df x0) with (-1 * df x0) by ring.
+  exact H2.
 Qed.
 
 (*********)
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index e424a732a..f07140752 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -407,8 +407,7 @@ Proof.
                       generalize
                         (Rplus_lt_compat (R_dist (f x2) l) eps (R_dist (f x2) l') eps H H0);
                         unfold R_dist; intros; rewrite (Rabs_minus_sym (f x2) l) in H1;
-                          rewrite (Rmult_comm 2 eps); rewrite (Rmult_plus_distr_l eps 1 1);
-                            elim (Rmult_ne eps); intros a b; rewrite a; clear a b;
+                          rewrite (Rmult_comm 2 eps); replace (eps *2) with (eps + eps) by ring;
                               generalize (R_dist_tri l l' (f x2)); unfold R_dist;
                                 intros;
                                   apply
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index b3ce6fa33..a053c349e 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -55,25 +55,8 @@ Proof.
     simpl in H0.
   replace (/ 3) with
   (1 * / 1 + -1 * 1 * / 1 + -1 * (-1 * 1) * / 2 +
-    -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)).
+    -1 * (-1 * (-1 * 1)) * / (2 + 1 + 1 + 1 + 1)) by field.
   apply H0.
-  repeat rewrite Rinv_1; repeat rewrite Rmult_1_r;
-    rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l;
-      rewrite Ropp_involutive; rewrite Rplus_opp_r; rewrite Rmult_1_r;
-        rewrite Rplus_0_l; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 6.
-  rewrite Rmult_plus_distr_l; replace (2 + 1 + 1 + 1 + 1) with 6.
-  rewrite <- (Rmult_comm (/ 6)); rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym.
-  rewrite Rmult_1_l; replace 6 with 6.
-  do 2 rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
-  rewrite Rmult_1_r; rewrite (Rmult_comm 3); rewrite <- Rmult_assoc;
-    rewrite <- Rinv_r_sym.
-  ring.
-  discrR.
-  discrR.
-  ring.
-  discrR.
-  ring.
-  discrR.
   apply H.
   unfold Un_decreasing; intros;
     apply Rmult_le_reg_l with (INR (fact n)).
diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v
index 4d2418639..5f2e0d5b5 100644
--- a/theories/Reals/Rtrigo1.v
+++ b/theories/Reals/Rtrigo1.v
@@ -1260,44 +1260,22 @@ Proof.
   intros x y H1 H2 H3 H4; rewrite <- (cos_neg x); rewrite <- (cos_neg y);
     rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1);
       unfold INR in |- *;
-        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; intro H5;
     generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI x H1);
       generalize (Rplus_le_compat_l (-3 * (PI / 2)) x (2 * PI) H2);
         generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI y H3);
           generalize (Rplus_le_compat_l (-3 * (PI / 2)) y (2 * PI) H4).
-  replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)).
-  replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)).
-  replace (-3 * (PI / 2) + 2 * PI) with (PI / 2).
-  replace (-3 * (PI / 2) + PI) with (- (PI / 2)).
+  replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring.
+  replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring.
+  replace (-3 * (PI / 2) + 2 * PI) with (PI / 2) by field.
+  replace (-3 * (PI / 2) + PI) with (- (PI / 2)) by field.
   clear H1 H2 H3 H4; intros H1 H2 H3 H4;
     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)).
+      replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring.
+  replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring.
   apply (sin_increasing_0 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H4 H3 H2 H1 H5).
-  unfold Rminus in |- *.
-  rewrite Ropp_mult_distr_l_reverse.
-  apply Rplus_comm.
-  unfold Rminus in |- *.
-  rewrite Ropp_mult_distr_l_reverse.
-  apply Rplus_comm.
-  pattern PI at 3 in |- *; rewrite double_var.
-  ring.
-  rewrite double; pattern PI at 3 4 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.
-  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.
 Qed.
 
 Lemma cos_increasing_1 :
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index 9ba14ee73..53056cabd 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -32,48 +32,22 @@ Proof.
 Qed.
 
 Lemma sin_cos_PI4 : sin (PI / 4) = cos (PI / 4).
-Proof with trivial.
-  rewrite cos_sin...
-  replace (PI / 2 + PI / 4) with (- (PI / 4) + PI)...
-  rewrite neg_sin; rewrite sin_neg; ring...
-  cut (PI = PI / 2 + PI / 2); [ intro | apply double_var ]...
-  pattern PI at 2 3; rewrite H; pattern PI at 2 3; rewrite H...
-  assert (H0 : 2 <> 0);
-    [ discrR | unfold Rdiv; rewrite Rinv_mult_distr; try ring ]...
+Proof.
+  rewrite cos_sin.
+  replace (PI / 2 + PI / 4) with (- (PI / 4) + PI) by field.
+  rewrite neg_sin, sin_neg; ring.
 Qed.
 
 Lemma sin_PI3_cos_PI6 : sin (PI / 3) = cos (PI / 6).
-Proof with trivial.
-  replace (PI / 6) with (PI / 2 - PI / 3)...
-  rewrite cos_shift...
-  assert (H0 : 6 <> 0); [ discrR | idtac ]...
-  assert (H1 : 3 <> 0); [ discrR | idtac ]...
-  assert (H2 : 2 <> 0); [ discrR | idtac ]...
-  apply Rmult_eq_reg_l with 6...
-  rewrite Rmult_minus_distr_l; repeat rewrite (Rmult_comm 6)...
-  unfold Rdiv; repeat rewrite Rmult_assoc...
-  rewrite <- Rinv_l_sym...
-  rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym...
-  rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r;
-    repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym...
-  ring...
+Proof.
+  replace (PI / 6) with (PI / 2 - PI / 3) by field.
+  now rewrite cos_shift.
 Qed.
 
 Lemma sin_PI6_cos_PI3 : cos (PI / 3) = sin (PI / 6).
-Proof with trivial.
-  replace (PI / 6) with (PI / 2 - PI / 3)...
-  rewrite sin_shift...
-  assert (H0 : 6 <> 0); [ discrR | idtac ]...
-  assert (H1 : 3 <> 0); [ discrR | idtac ]...
-  assert (H2 : 2 <> 0); [ discrR | idtac ]...
-  apply Rmult_eq_reg_l with 6...
-  rewrite Rmult_minus_distr_l; repeat rewrite (Rmult_comm 6)...
-  unfold Rdiv; repeat rewrite Rmult_assoc...
-  rewrite <- Rinv_l_sym...
-  rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym...
-  rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r;
-    repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym...
-  ring...
+Proof.
+  replace (PI / 6) with (PI / 2 - PI / 3) by field.
+  now rewrite sin_shift.
 Qed.
 
 Lemma PI6_RGT_0 : 0 < PI / 6.
@@ -90,29 +64,20 @@ Proof.
 Qed.
 
 Lemma sin_PI6 : sin (PI / 6) = 1 / 2.
-Proof with trivial.
-  assert (H : 2 <> 0); [ discrR | idtac ]...
-  apply Rmult_eq_reg_l with (2 * cos (PI / 6))...
+Proof.
+  apply Rmult_eq_reg_l with (2 * cos (PI / 6)).
   replace (2 * cos (PI / 6) * sin (PI / 6)) with
-  (2 * sin (PI / 6) * cos (PI / 6))...
-  rewrite <- sin_2a; replace (2 * (PI / 6)) with (PI / 3)...
-  rewrite sin_PI3_cos_PI6...
-  unfold Rdiv; rewrite Rmult_1_l; rewrite Rmult_assoc;
-    pattern 2 at 2; rewrite (Rmult_comm 2); rewrite Rmult_assoc;
-      rewrite <- Rinv_l_sym...
-  rewrite Rmult_1_r...
-  unfold Rdiv; rewrite Rinv_mult_distr...
-  rewrite (Rmult_comm (/ 2)); rewrite (Rmult_comm 2);
-    repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym...
-  rewrite Rmult_1_r...
-  discrR...
-  ring...
-  apply prod_neq_R0...
+  (2 * sin (PI / 6) * cos (PI / 6)) by ring.
+  rewrite <- sin_2a; replace (2 * (PI / 6)) with (PI / 3) by field.
+  rewrite sin_PI3_cos_PI6.
+  field.
+  apply prod_neq_R0.
+  discrR.
   cut (0 < cos (PI / 6));
     [ intro H1; auto with real
       | apply cos_gt_0;
         [ apply (Rlt_trans (- (PI / 2)) 0 (PI / 6) _PI2_RLT_0 PI6_RGT_0)
-          | apply PI6_RLT_PI2 ] ]...
+          | apply PI6_RLT_PI2 ] ].
 Qed.
 
 Lemma sqrt2_neq_0 : sqrt 2 <> 0.
@@ -188,20 +153,13 @@ Proof with trivial.
   apply Rinv_0_lt_compat; apply Rlt_sqrt2_0...
   rewrite Rsqr_div...
   rewrite Rsqr_1; rewrite Rsqr_sqrt...
-  assert (H : 2 <> 0); [ discrR | idtac ]...
   unfold Rsqr; pattern (cos (PI / 4)) at 1;
     rewrite <- sin_cos_PI4;
       replace (sin (PI / 4) * cos (PI / 4)) with
-      (1 / 2 * (2 * sin (PI / 4) * cos (PI / 4)))...
-  rewrite <- sin_2a; replace (2 * (PI / 4)) with (PI / 2)...
+      (1 / 2 * (2 * sin (PI / 4) * cos (PI / 4))) by field.
+  rewrite <- sin_2a; replace (2 * (PI / 4)) with (PI / 2) by field.
   rewrite sin_PI2...
-  apply Rmult_1_r...
-  unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rinv_mult_distr...
-  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym...
-  rewrite Rmult_1_r...
-  unfold Rdiv; rewrite Rmult_1_l; repeat rewrite <- Rmult_assoc...
-  rewrite <- Rinv_l_sym...
-  rewrite Rmult_1_l...
+  field.
   left; prove_sup...
   apply sqrt2_neq_0...
 Qed.
@@ -219,24 +177,17 @@ Proof.
 Qed.
 
 Lemma cos3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2.
-Proof with trivial.
-  replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4))...
-  rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4...
-  unfold Rdiv; rewrite Ropp_mult_distr_l_reverse...
-  unfold Rminus; rewrite Ropp_involutive; pattern PI at 1;
-    rewrite double_var; unfold Rdiv; rewrite Rmult_plus_distr_r;
-      repeat rewrite Rmult_assoc; rewrite <- Rinv_mult_distr;
-        [ ring | discrR | discrR ]...
+Proof.
+  replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field.
+  rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4.
+  unfold Rdiv.
+  ring.
 Qed.
 
 Lemma sin3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2.
-Proof with trivial.
-  replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4))...
-  rewrite sin_shift; rewrite cos_neg; rewrite cos_PI4...
-  unfold Rminus; rewrite Ropp_involutive; pattern PI at 1;
-    rewrite double_var; unfold Rdiv; rewrite Rmult_plus_distr_r;
-      repeat rewrite Rmult_assoc; rewrite <- Rinv_mult_distr;
-        [ ring | discrR | discrR ]...
+Proof.
+  replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field.
+  now rewrite sin_shift, cos_neg, cos_PI4.
 Qed.
 
 Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2.
@@ -248,19 +199,11 @@ Proof with trivial.
   left; apply (Rmult_lt_0_compat (sqrt 3) (/ 2))...
   apply Rlt_sqrt3_0...
   apply Rinv_0_lt_compat; prove_sup0...
-  assert (H : 2 <> 0); [ discrR | idtac ]...
-  assert (H1 : 4 <> 0); [ apply prod_neq_R0 | idtac ]...
   rewrite Rsqr_div...
   rewrite cos2; unfold Rsqr; rewrite sin_PI6; rewrite sqrt_def...
-  unfold Rdiv; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 4...
-  rewrite Rmult_minus_distr_l; rewrite (Rmult_comm 3);
-    repeat rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym...
-  rewrite Rmult_1_l; rewrite Rmult_1_r...
-  rewrite <- (Rmult_comm (/ 2)); repeat rewrite <- Rmult_assoc...
-  rewrite <- Rinv_l_sym...
-  rewrite Rmult_1_l; rewrite <- Rinv_r_sym...
-  ring...
-  left; prove_sup0...
+  field.
+  left ; prove_sup0.
+  discrR.
 Qed.
 
 Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3.
@@ -306,56 +249,32 @@ Proof.
 Qed.
 
 Lemma cos_2PI3 : cos (2 * (PI / 3)) = -1 / 2.
-Proof with trivial.
-  assert (H : 2 <> 0); [ discrR | idtac ]...
-  assert (H0 : 4 <> 0); [ apply prod_neq_R0 | idtac ]...
-  rewrite double; rewrite cos_plus; rewrite sin_PI3; rewrite cos_PI3;
-    unfold Rdiv; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 4...
-  rewrite Rmult_minus_distr_l; repeat rewrite Rmult_assoc;
-    rewrite (Rmult_comm 2)...
-  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym...
-  rewrite Rmult_1_r; rewrite <- Rinv_r_sym...
-  pattern 2 at 4; rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc;
-    rewrite <- Rinv_l_sym...
-  rewrite Rmult_1_r; rewrite Ropp_mult_distr_r_reverse; rewrite Rmult_1_r...
-  rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym...
-  rewrite Rmult_1_r; rewrite (Rmult_comm 2); rewrite (Rmult_comm (/ 2))...
-  repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym...
-  rewrite Rmult_1_r; rewrite sqrt_def...
-  ring...
-  left; prove_sup...
+Proof.
+  rewrite cos_2a, sin_PI3, cos_PI3.
+  replace (sqrt 3 / 2 * (sqrt 3 / 2)) with ((sqrt 3 * sqrt 3) / 4) by field.
+  rewrite sqrt_sqrt.
+  field.
+  left ; prove_sup0.
 Qed.
 
 Lemma tan_2PI3 : tan (2 * (PI / 3)) = - sqrt 3.
-Proof with trivial.
-  assert (H : 2 <> 0); [ discrR | idtac ]...
-  unfold tan; rewrite sin_2PI3; rewrite cos_2PI3; unfold Rdiv;
-    rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l;
-      rewrite <- Ropp_inv_permute...
-  rewrite Rinv_involutive...
-  rewrite Rmult_assoc; rewrite Ropp_mult_distr_r_reverse; rewrite <- Rinv_l_sym...
-  ring...
-  apply Rinv_neq_0_compat...
+Proof.
+  unfold tan; rewrite sin_2PI3, cos_2PI3.
+  field.
 Qed.
 
 Lemma cos_5PI4 : cos (5 * (PI / 4)) = -1 / sqrt 2.
-Proof with trivial.
-  replace (5 * (PI / 4)) with (PI / 4 + PI)...
-  rewrite neg_cos; rewrite cos_PI4; unfold Rdiv;
-    rewrite Ropp_mult_distr_l_reverse...
-  pattern PI at 2; rewrite double_var; pattern PI at 2 3;
-    rewrite double_var; assert (H : 2 <> 0);
-      [ discrR | unfold Rdiv; repeat rewrite Rinv_mult_distr; try ring ]...
+Proof.
+  replace (5 * (PI / 4)) with (PI / 4 + PI) by field.
+  rewrite neg_cos; rewrite cos_PI4; unfold Rdiv.
+  ring.
 Qed.
 
 Lemma sin_5PI4 : sin (5 * (PI / 4)) = -1 / sqrt 2.
-Proof with trivial.
-  replace (5 * (PI / 4)) with (PI / 4 + PI)...
-  rewrite neg_sin; rewrite sin_PI4; unfold Rdiv;
-    rewrite Ropp_mult_distr_l_reverse...
-  pattern PI at 2; rewrite double_var; pattern PI at 2 3;
-    rewrite double_var; assert (H : 2 <> 0);
-      [ discrR | unfold Rdiv; repeat rewrite Rinv_mult_distr; try ring ]...
+Proof.
+  replace (5 * (PI / 4)) with (PI / 4 + PI) by field.
+  rewrite neg_sin; rewrite sin_PI4; unfold Rdiv.
+  ring.
 Qed.
 
 Lemma sin_cos5PI4 : cos (5 * (PI / 4)) = sin (5 * (PI / 4)).
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index eed612d94..4a1e3179c 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -395,15 +395,8 @@ Proof.
   apply Rlt_le_trans with alp.
   apply H7.
   unfold alp; apply Rmin_l.
-  rewrite sin_plus; unfold Rminus, Rdiv;
-    repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l;
-      repeat rewrite Rmult_assoc; repeat rewrite Rplus_assoc;
-        apply Rplus_eq_compat_l.
-  rewrite (Rplus_comm (sin x * (-1 * / h))); repeat rewrite Rplus_assoc;
-    apply Rplus_eq_compat_l.
-  rewrite Ropp_mult_distr_r_reverse; rewrite Ropp_mult_distr_l_reverse;
-    rewrite Rmult_1_r; rewrite Rmult_1_l; rewrite Ropp_mult_distr_r_reverse;
-      rewrite <- Ropp_mult_distr_l_reverse; apply Rplus_comm.
+  rewrite sin_plus.
+  now field.
   unfold alp; unfold Rmin; case (Rle_dec alp1 alp2); intro.
   apply (cond_pos alp1).
   apply (cond_pos alp2).