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/Rlimit.v | |
| parent | d2061bd8cd2d809d6e5a849dd150e9e0d74331fc (diff) | |
Simplify some proofs using ring and field.
Diffstat (limited to 'theories/Reals/Rlimit.v')
| -rw-r--r-- | theories/Reals/Rlimit.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index e424a732a..f07140752 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -407,8 +407,7 @@ Proof. generalize (Rplus_lt_compat (R_dist (f x2) l) eps (R_dist (f x2) l') eps H H0); unfold R_dist; intros; rewrite (Rabs_minus_sym (f x2) l) in H1; - rewrite (Rmult_comm 2 eps); rewrite (Rmult_plus_distr_l eps 1 1); - elim (Rmult_ne eps); intros a b; rewrite a; clear a b; + rewrite (Rmult_comm 2 eps); replace (eps *2) with (eps + eps) by ring; generalize (R_dist_tri l l' (f x2)); unfold R_dist; intros; apply |