Quelques améliorations

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

1 files changed, 103 insertions, 282 deletions

diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index 004cbda0c..4e9244dd3 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -15,15 +15,13 @@ Require Rtrigo.
 Require R_sqrt.
 
 Lemma tan_PI : ``(tan PI)==0``.
-Unfold tan; Rewrite -> sin_PI; Rewrite -> cos_PI.
-Unfold Rdiv; Apply Rmult_Ol. 
+Unfold tan; Rewrite sin_PI; Rewrite cos_PI; Unfold Rdiv; Apply Rmult_Ol. 
 Qed.
 
 Lemma sin_3PI2 : ``(sin (3*(PI/2)))==(-1)``.
 Replace ``3*(PI/2)`` with ``PI+(PI/2)``.
-Rewrite -> sin_plus; Rewrite -> sin_PI; Rewrite -> cos_PI; Rewrite -> sin_PI2; Ring.
-Pattern 1 PI; Rewrite (double_var PI).
-Ring.
+Rewrite sin_plus; Rewrite sin_PI; Rewrite cos_PI; Rewrite sin_PI2; Ring.
+Pattern 1 PI; Rewrite (double_var PI); Ring.
 Qed.
 
 Lemma tan_2PI : ``(tan (2*PI))==0``.
@@ -31,80 +29,45 @@ Unfold tan; Rewrite sin_2PI; Unfold Rdiv; Apply Rmult_Ol.
 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 2 3 PI; Rewrite H.
-Pattern 2 3 PI; Rewrite H.
-Unfold Rdiv.
-Repeat Rewrite Rinv_Rmult.
-Ring.
-DiscrR.
-DiscrR.
+Pattern 2 3 PI; Rewrite H; Pattern 2 3 PI; Rewrite H.
+Assert H0 : ``2<>0``; [DiscrR | Unfold Rdiv; Rewrite Rinv_Rmult; Try 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; Reflexivity.
-Pattern 2 PI; Rewrite double_var.
-Cut ``PI == 3*(PI/3)``.
-Intro.
-Pattern 1 PI; Rewrite H.
-Unfold Rdiv.
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Unfold Rminus.
-Rewrite (Rmult_Rplus_distrl ``PI*/2`` ``PI*/2`` ``/3``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Rewrite (Rmult_sym ``2``).
-Replace ``3*2`` with ``6``.
-Rewrite Ropp_distr1.
-Ring.
-Ring.
-DiscrR.
-DiscrR.
-DiscrR.
-DiscrR.
-Unfold Rdiv.
-Rewrite (Rmult_sym ``3``).
-Rewrite Rmult_assoc.
+Rewrite cos_shift.
+Assert H0 : ``6<>0``; [DiscrR | Idtac].
+Assert H1 : ``3<>0``; [DiscrR | Idtac].
+Assert H2 : ``2<>0``; [DiscrR | Idtac].
+Apply r_Rmult_mult with ``6``.
+Rewrite Rminus_distr; Repeat Rewrite (Rmult_sym ``6``).
+Unfold Rdiv; Repeat Rewrite Rmult_assoc.
 Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Reflexivity.
-DiscrR.
+Rewrite (Rmult_sym ``/3``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
+Pattern 2 PI; Rewrite (Rmult_sym PI); Repeat Rewrite Rmult_1r; Repeat Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
+Ring.
 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; Reflexivity.
-Pattern 2 PI; Rewrite double_var.
-Cut ``PI == 3*(PI/3)``.
-Intro.
-Pattern 1 PI; Rewrite H.
-Unfold Rdiv.
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Unfold Rminus.
-Rewrite (Rmult_Rplus_distrl ``PI*/2`` ``PI*/2`` ``/3``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Rewrite (Rmult_sym ``2``).
-Replace ``3*2`` with ``6``.
-Rewrite Ropp_distr1.
-Ring.
-Ring.
-DiscrR.
-DiscrR.
-DiscrR.
-DiscrR.
-Unfold Rdiv.
-Rewrite (Rmult_sym ``3``).
-Rewrite Rmult_assoc.
+Rewrite sin_shift.
+Assert H0 : ``6<>0``; [DiscrR | Idtac].
+Assert H1 : ``3<>0``; [DiscrR | Idtac].
+Assert H2 : ``2<>0``; [DiscrR | Idtac].
+Apply r_Rmult_mult with ``6``.
+Rewrite Rminus_distr; Repeat Rewrite (Rmult_sym ``6``).
+Unfold Rdiv; Repeat Rewrite Rmult_assoc.
 Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Reflexivity.
-DiscrR.
+Rewrite (Rmult_sym ``/3``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
+Pattern 2 PI; Rewrite (Rmult_sym PI); Repeat Rewrite Rmult_1r; Repeat Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
+Ring.
 Qed.
 
 Lemma PI6_RGT_0 : ``0<PI/6``.
@@ -114,40 +77,25 @@ Qed.
 Lemma PI6_RLT_PI2 : ``PI/6<PI/2``.
 Unfold Rdiv; Apply Rlt_monotony.
 Apply PI_RGT_0.
-Apply Rinv_lt.
-Apply Rmult_lt_pos; Sup0.
-Pattern 1 ``2``; Rewrite <- Rplus_Or.
-Replace ``6`` with ``2+4``; [Apply Rlt_compatibility; Sup0 | Ring].
+Apply Rinv_lt; Sup.
 Qed.
 
 Lemma sin_PI6 : ``(sin (PI/6))==1/2``.
+Proof with Trivial.
+Assert H : ``2<>0``; [DiscrR | Idtac].
 Apply r_Rmult_mult 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_1l.
-Rewrite Rmult_assoc.
-Pattern 2 ``2``; Rewrite (Rmult_sym ``2``).
-Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Reflexivity.
-DiscrR.
-Replace ``6`` with ``2*3``.
-Unfold Rdiv.
-Rewrite Rinv_Rmult.
-Rewrite (Rmult_sym ``/2``).
-Rewrite (Rmult_sym ``2``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
+Unfold Rdiv; Rewrite Rmult_1l; Rewrite Rmult_assoc; Pattern 2 ``2``; Rewrite (Rmult_sym ``2``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r.
+Unfold Rdiv; Rewrite Rinv_Rmult.
+Rewrite (Rmult_sym ``/2``); Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
 Rewrite Rmult_1r.
-Reflexivity.
-DiscrR.
-DiscrR.
 DiscrR.
 Ring.
-Ring.
-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 prod_neq_R0.
+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]].
 Qed.
 
 Lemma sqrt2_neq_0 : ~``(sqrt 2)==0``.
@@ -175,40 +123,28 @@ Unfold Rdiv; Apply Rmult_lt_pos; [Apply PI_RGT_0 | Apply Rlt_Rinv; Sup0].
 Qed.
 
 Lemma cos_PI4 : ``(cos (PI/4))==1/(sqrt 2)``.
+Proof with Trivial.
 Apply Rsqr_inj.
 Apply cos_ge_0.
 Left; Apply (Rlt_trans ``-(PI/2)`` R0 ``PI/4`` _PI2_RLT_0 PI4_RGT_0).
 Left; Apply PI4_RLT_PI2.
 Left; Apply (Rmult_lt_pos R1 ``(Rinv (sqrt 2))``).
-Apply Rlt_R0_R1.
-Apply Rlt_Rinv.
-Apply Rlt_sqrt2_0.
+Sup.
+Apply Rlt_Rinv; Apply Rlt_sqrt2_0.
 Rewrite Rsqr_div.
 Rewrite Rsqr_1; Rewrite Rsqr_sqrt.
+Assert H : ``2<>0``; [DiscrR | Idtac].
 Unfold Rsqr; Pattern 1 ``(cos (PI/4))``; 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``.
 Rewrite sin_PI2.
 Apply Rmult_1r.
-Unfold Rdiv.
-Rewrite (Rmult_sym ``2``).
-Replace ``4`` with ``2*2``.
-Rewrite Rinv_Rmult.
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
+Unfold Rdiv; Rewrite (Rmult_sym ``2``); Rewrite Rinv_Rmult.
+Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
 Rewrite Rmult_1r.
-Reflexivity.
-DiscrR.
-DiscrR.
-DiscrR.
-Reflexivity.
-Unfold Rdiv.
-Rewrite Rmult_1l.
-Repeat Rewrite <- Rmult_assoc.
+Unfold Rdiv; Rewrite Rmult_1l; Repeat Rewrite <- Rmult_assoc.
 Rewrite <- Rinv_l_sym.
 Rewrite Rmult_1l.
-Reflexivity.
-DiscrR.
-Left; Sup0.
+Left; Sup.
 Apply sqrt2_neq_0.
 Qed.
 
@@ -218,51 +154,27 @@ Qed.
 
 Lemma tan_PI4 : ``(tan (PI/4))==1``.
 Unfold tan; Rewrite sin_cos_PI4.
-Unfold Rdiv. 
-Apply Rinv_r.
-Replace ``PI*/4`` with ``PI/4``.
-Rewrite cos_PI4; Apply R1_sqrt2_neq_0.
-Unfold Rdiv; Reflexivity.
+Unfold Rdiv; Apply Rinv_r.
+Change ``(cos (PI/4))<>0``; Rewrite cos_PI4; Apply R1_sqrt2_neq_0.
 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_mul1.
-Reflexivity.
-Unfold Rminus.
-Rewrite Ropp_Ropp.
-Pattern 1 PI; Rewrite double_var.
-Unfold Rdiv.
-Rewrite Rmult_Rplus_distrl.
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Replace ``2*2`` with ``4``.
-Ring.
-Ring.
-DiscrR.
-DiscrR.
+Unfold Rdiv; Rewrite Ropp_mul1.
+Unfold Rminus; Rewrite Ropp_Ropp; Pattern 1 PI; Rewrite double_var; Unfold Rdiv; Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_Rmult; [Ring | DiscrR | DiscrR].
 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; Reflexivity.
-Unfold Rminus.
-Rewrite Ropp_Ropp.
-Pattern 1 PI; Rewrite double_var.
-Unfold Rdiv.
-Rewrite Rmult_Rplus_distrl.
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Replace ``2*2`` with ``4``.
-Ring.
-Ring.
-DiscrR.
-DiscrR.
+Rewrite sin_shift; Rewrite cos_neg; Rewrite cos_PI4.
+Unfold Rminus; Rewrite Ropp_Ropp; Pattern 1 PI; Rewrite double_var; Unfold Rdiv; Rewrite Rmult_Rplus_distrl; Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_Rmult; [Ring | DiscrR | DiscrR].
 Qed.
 
 Lemma cos_PI6 : ``(cos (PI/6))==(sqrt 3)/2``.
+Proof with Trivial.
 Apply Rsqr_inj.
 Apply cos_ge_0.
 Left; Apply (Rlt_trans ``-(PI/2)`` R0 ``PI/6`` _PI2_RLT_0 PI6_RGT_0).
@@ -270,50 +182,29 @@ Left; Apply PI6_RLT_PI2.
 Left; Apply (Rmult_lt_pos ``(sqrt 3)`` ``(Rinv 2)``).
 Apply Rlt_sqrt3_0.
 Apply Rlt_Rinv; 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_1l.
-Rewrite <- Rinv_Rmult.
-Replace ``2*2`` with ``4``.
-Apply r_Rmult_mult with ``4``.
-Unfold Rminus.
-Rewrite Rmult_Rplus_distr.
-Rewrite Rmult_1r.
-Rewrite Ropp_mul3.
-Rewrite <- Rinv_r_sym.
-Rewrite (Rmult_sym ``3``).
-Rewrite <- Rmult_assoc.
-Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1l.
-Ring.
-DiscrR.
-DiscrR.
-DiscrR.
+Unfold Rdiv; Rewrite Rmult_1l; Apply r_Rmult_mult with ``4``.
+Rewrite Rminus_distr; Rewrite (Rmult_sym ``3``); Repeat Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1l; Rewrite Rmult_1r.
+Rewrite <- (Rmult_sym ``/2``); Repeat Rewrite <- Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1l; Rewrite <- Rinv_r_sym.
 Ring.
-DiscrR.
-DiscrR.
 Left; Sup0.
-DiscrR.
 Qed.
 
 Lemma tan_PI6 : ``(tan (PI/6))==1/(sqrt 3)``.
-Unfold tan; Rewrite sin_PI6; Rewrite cos_PI6.
-Unfold Rdiv.
-Repeat Rewrite Rmult_1l.
-Rewrite Rinv_Rmult.
+Unfold tan; Rewrite sin_PI6; Rewrite cos_PI6; Unfold Rdiv; Repeat Rewrite Rmult_1l; Rewrite Rinv_Rmult.
 Rewrite Rinv_Rinv.
-Rewrite (Rmult_sym ``/2``).
-Rewrite Rmult_assoc.
-Rewrite <- Rinv_r_sym.
+Rewrite (Rmult_sym ``/2``); Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
 Apply Rmult_1r.
 DiscrR.
 DiscrR.
-Red; Intro.
-Assert H1 := Rlt_sqrt3_0.
-Rewrite H in H1; Elim (Rlt_antirefl ``0`` H1).
-Apply Rinv_neq_R0.
-DiscrR.
+Red; Intro; Assert H1 := Rlt_sqrt3_0; Rewrite H in H1; Elim (Rlt_antirefl ``0`` H1).
+Apply Rinv_neq_R0; DiscrR.
 Qed.
 
 Lemma sin_PI3 : ``(sin (PI/3))==(sqrt 3)/2``.
@@ -325,121 +216,57 @@ Rewrite sin_PI6_cos_PI3; Apply sin_PI6.
 Qed.
 
 Lemma tan_PI3 : ``(tan (PI/3))==(sqrt 3)``.
-Unfold tan; Rewrite sin_PI3; Rewrite cos_PI3.
-Unfold Rdiv.
-Rewrite Rmult_1l.
-Rewrite Rinv_Rinv.
-Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
+Unfold tan; Rewrite sin_PI3; Rewrite cos_PI3; Unfold Rdiv; Rewrite Rmult_1l; Rewrite Rinv_Rinv.
+Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
 Apply Rmult_1r.
 DiscrR.
 DiscrR.
 Qed.
 
 Lemma sin_2PI3 : ``(sin (2*(PI/3)))==(sqrt 3)/2``.
-Rewrite double.
-Rewrite sin_plus; Rewrite sin_PI3; Rewrite cos_PI3.
-Unfold Rdiv.
-Repeat Rewrite Rmult_1l.
-Rewrite (Rmult_sym ``/2``).
-Pattern 3 ``(sqrt 3)``; Rewrite double_var.
-Rewrite Rmult_Rplus_distrl.
-Unfold Rdiv.
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Replace ``2*2`` with ``4``.
-Reflexivity.
-Ring.
-DiscrR.
-DiscrR.
+Rewrite double; Rewrite sin_plus; Rewrite sin_PI3; Rewrite cos_PI3; Unfold Rdiv; Repeat Rewrite Rmult_1l; Rewrite (Rmult_sym ``/2``); Repeat Rewrite <- Rmult_assoc; Rewrite double_var; Reflexivity.
 Qed.
 
 Lemma cos_2PI3 : ``(cos (2*(PI/3)))==-1/2``.
-Rewrite double.
-Rewrite cos_plus; Rewrite sin_PI3; Rewrite cos_PI3.
-Unfold Rdiv.
-Rewrite Rmult_1l.
-Apply r_Rmult_mult with ``2*2``.
-Rewrite Rminus_distr.
-Repeat Rewrite Rmult_assoc.
-Rewrite (Rmult_sym ``2``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- (Rinv_l_sym).
-Rewrite Rmult_1r.
-Rewrite <- Rinv_r_sym.
-Pattern 4 ``2``; Rewrite (Rmult_sym ``2``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r.
-Rewrite Ropp_mul3.
-Rewrite Rmult_1r.
-Rewrite (Rmult_sym ``2``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r.
-Rewrite (Rmult_sym ``2``).
-Rewrite (Rmult_sym ``/2``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r.
-Rewrite sqrt_def.
+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_1l; Apply r_Rmult_mult with ``4``.
+Rewrite Rminus_distr; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``2``).
+Repeat Rewrite Rmult_assoc; Rewrite <- (Rinv_l_sym).
+Rewrite Rmult_1r; Rewrite <- Rinv_r_sym.
+Pattern 4 ``2``; Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite Ropp_mul3; Rewrite Rmult_1r.
+Rewrite (Rmult_sym ``2``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite (Rmult_sym ``2``); Rewrite (Rmult_sym ``/2``).
+Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Rewrite sqrt_def.
 Ring.
-Replace ``3`` with ``(INR (S (S (S O))))`` .
-Apply pos_INR.
-Unfold INR; Rewrite Rplus_sym; Reflexivity.
-DiscrR.
-DiscrR.
-DiscrR.
-DiscrR.
-DiscrR.
-Apply prod_neq_R0; DiscrR.
+Left; Sup.
 Qed.
 
 Lemma tan_2PI3 : ``(tan (2*(PI/3)))==-(sqrt 3)``.
-Unfold tan; Rewrite sin_2PI3; Rewrite cos_2PI3.
-Unfold Rdiv.
-Rewrite Rinv_Rmult.
+Proof with Trivial.
+Assert H : ``2<>0``; [DiscrR | Idtac].
+Unfold tan; Rewrite sin_2PI3; Rewrite cos_2PI3; Unfold Rdiv; Rewrite Ropp_mul1; Rewrite Rmult_1l; Rewrite <- Ropp_Rinv.
 Rewrite Rinv_Rinv.
-Repeat Rewrite Rmult_assoc.
-Rewrite (Rmult_sym ``/2``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1r.
-Rewrite <- Ropp_Rinv.
-Rewrite Ropp_mul3.
-Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity.
-DiscrR.
-DiscrR.
-DiscrR.
-DiscrR.
-Apply Rinv_neq_R0; DiscrR.
+Rewrite Rmult_assoc; Rewrite Ropp_mul3; Rewrite <- Rinv_l_sym.
+Ring.
+Apply Rinv_neq_R0.
 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.
-Symmetry; Apply Ropp_mul1.
-Pattern 2 PI; Rewrite double_var.
-Pattern 2 3 PI; Rewrite double_var.
-Unfold Rdiv.
-Repeat Rewrite Rinv_Rmult.
-Ring.
-DiscrR.
-DiscrR.
+Rewrite neg_cos; Rewrite cos_PI4; Unfold Rdiv; Rewrite Ropp_mul1.
+Pattern 2 PI; Rewrite double_var; Pattern 2 3 PI; Rewrite double_var; Assert H : ``2<>0``; [DiscrR | Unfold Rdiv; Repeat Rewrite Rinv_Rmult; Try 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; Symmetry; Apply Ropp_mul1.
-Pattern 2 PI; Rewrite double_var.
-Pattern 2 3 PI; Rewrite double_var.
-Unfold Rdiv.
-Repeat Rewrite Rinv_Rmult.
-Ring.
-DiscrR.
-DiscrR.
+Rewrite neg_sin; Rewrite sin_PI4; Unfold Rdiv; Rewrite Ropp_mul1.
+Pattern 2 PI; Rewrite double_var; Pattern 2 3 PI; Rewrite double_var; Assert H : ``2<>0``; [DiscrR | Unfold Rdiv; Repeat Rewrite Rinv_Rmult; Try Ring].
 Qed.
 
 Lemma sin_cos5PI4 : ``(cos (5*(PI/4)))==(sin (5*(PI/4)))``.
@@ -475,14 +302,9 @@ Definition toRad [x:R] : R := ``x*PI*/plat``.
 Definition toDeg [x:R] : R := ``x*plat*/PI``.
 
 Lemma rad_deg : (x:R) (toRad (toDeg x))==x.
-Intro x; Unfold toRad toDeg.
-Rewrite <- (Rmult_sym plat).
-Repeat Rewrite Rmult_assoc.
-Rewrite (Rmult_sym plat).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym. 
-Rewrite Rmult_1r; Rewrite <- Rinv_l_sym. 
-Apply Rmult_1r.
+Intro; Unfold toRad toDeg; Replace ``x*plat*/PI*PI*/plat`` with ``x*(plat*/plat)*(PI*/PI)``; [Idtac | Ring].
+Repeat Rewrite <- Rinv_r_sym.
+Ring.
 Apply PI_neq0.
 Unfold plat; DiscrR.
 Qed.
@@ -492,8 +314,7 @@ Intros; Unfold toRad in H; Apply r_Rmult_mult with PI.
 Rewrite <- (Rmult_sym x); Rewrite <- (Rmult_sym y).
 Apply r_Rmult_mult with ``/plat``.
 Rewrite <- (Rmult_sym ``x*PI``); Rewrite <- (Rmult_sym ``y*PI``); Assumption.
-Apply Rinv_neq_R0.
-Unfold plat; DiscrR.
+Apply Rinv_neq_R0; Unfold plat; DiscrR.
 Apply PI_neq0.
 Qed.
 
@@ -519,9 +340,9 @@ Left; Apply sin_lb_gt_0; Assumption.
 Elim H1; Intro.
 Rewrite <- H2; Unfold sin_lb; Unfold sin_approx; Unfold sum_f_R0; Unfold sin_term; Repeat Rewrite pow_ne_zero.
 Unfold Rdiv; Repeat Rewrite Rmult_Ol; Repeat Rewrite Rmult_Or; Repeat Rewrite Rplus_Or; Right; Reflexivity.
-Simpl; Discriminate.
-Simpl; Discriminate.
-Simpl; Discriminate.
-Simpl; Discriminate.
+Discriminate.
+Discriminate.
+Discriminate.
+Discriminate.
 Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` a ``0`` H H2)).
 Qed.