diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-05 19:58:44 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 16:42:00 +0100 |
commit | 46d79ebd74876f34242c8c5d9ab3dcedbadba7cc (patch) | |
tree | 262da87e5fca237320e75be293244dd19628ca3a /theories/Reals/Rtrigo_reg.v | |
parent | d2061bd8cd2d809d6e5a849dd150e9e0d74331fc (diff) |
Simplify some proofs using ring and field.
Diffstat (limited to 'theories/Reals/Rtrigo_reg.v')
-rw-r--r-- | theories/Reals/Rtrigo_reg.v | 11 |
1 files changed, 2 insertions, 9 deletions
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). |