diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 10:26:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 11:33:55 +0200 |
| commit | 76adb57c72fccb4f3e416bd7f3927f4fff72178b (patch) | |
| tree | f8d72073a2ea62d3e5c274c201ef06532ac57b61 /theories/Reals/Rderiv.v | |
| parent | be01deca2b8ff22505adaa66f55f005673bf2d85 (diff) | |
Making those proofs which depend on names generated for the arguments
in Prop of constructors of inductive types independent of these names.
Incidentally upgraded/simplified a couple of proofs, mainly in Reals.
This prepares to the next commit about using names based on H for such
hypotheses in Prop.
Diffstat (limited to 'theories/Reals/Rderiv.v')
| -rw-r--r-- | theories/Reals/Rderiv.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index e714f5f8c..69ef143e7 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -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. |