diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/Reals/Rderiv.v | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/Reals/Rderiv.v')
| -rw-r--r-- | theories/Reals/Rderiv.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 64b1b0d4..3a332d21 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -162,9 +162,9 @@ Proof. (Rplus_lt_compat (Rabs (d x0 * (x1 - x0))) (eps * / 2) (Rabs (x1 - x0) * eps) (eps * / 2) H5 H3); intro; rewrite eps2 in H10; assumption. - unfold Rabs; case (Rcase_abs 2); auto. - intro; cut (0 < 2). - intro ; elim (Rlt_asym 0 2 H7 r). + unfold Rabs; destruct (Rcase_abs 2) as [Hlt|Hge]; auto. + cut (0 < 2). + intro H7; elim (Rlt_asym 0 2 H7 Hlt). fourier. apply Rabs_no_R0. discrR. @@ -193,11 +193,11 @@ Proof. unfold limit_in; intros; simpl; split with eps; split; auto. intros; elim H0; clear H0; intros; unfold D_x in H0; elim H0; intros; - rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (not_eq_sym H3))); - unfold R_dist; rewrite (Rminus_diag_eq 1 1 (eq_refl 1)); - unfold Rabs; case (Rcase_abs 0); intro. + rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (sym_not_eq H3))); + unfold R_dist; rewrite (Rminus_diag_eq 1 1 (refl_equal 1)); + unfold Rabs; case (Rcase_abs 0) as [Hlt|Hge]. absurd (0 < 0); auto. - red; intro; apply (Rlt_irrefl 0 r). + red in |- *; intro; apply (Rlt_irrefl 0 Hlt). unfold Rgt in H; assumption. Qed. |