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