diff options
Diffstat (limited to 'theories/Reals/Rtrigo_reg.v')
| -rw-r--r-- | theories/Reals/Rtrigo_reg.v | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index eed612d94..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. @@ -395,15 +396,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). |