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/Rderiv.v | |
parent | d2061bd8cd2d809d6e5a849dd150e9e0d74331fc (diff) |
Simplify some proofs using ring and field.
Diffstat (limited to 'theories/Reals/Rderiv.v')
-rw-r--r-- | theories/Reals/Rderiv.v | 12 |
1 files changed, 4 insertions, 8 deletions
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. (*********) |