diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-03 17:15:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-04 18:42:22 +0200 |
| commit | e1e0f4f7f3c549fd3d5677b67c6b13ed687e6f12 (patch) | |
| tree | 70d40db0a8bb6378bb97d9c7c72567045bd4bd78 /theories/Reals/Rtopology.v | |
| parent | 6c9e2ded8fc093e42902d008a883b6650533d47f (diff) | |
Make standard library independent of the names generated by
induction/elim over a dependent elimination principle for Prop
arguments.
Diffstat (limited to 'theories/Reals/Rtopology.v')
| -rw-r--r-- | theories/Reals/Rtopology.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 991a52409..ac15cf21e 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -1655,9 +1655,9 @@ Proof. apply H7; split. unfold D_x, no_cond; split; [ trivial | assumption ]. apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H8 | apply Rmin_l ]. - assert (H8 := completeness _ H6 H7); elim H8; clear H8; intros; + destruct (completeness _ H6 H7) as (x1,p). cut (0 < x1 <= M - m). - intro; elim H8; clear H8; intros; exists (mkposreal _ H8); split. + intros (H8,H9); exists (mkposreal _ H8); split. intros; cut (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp). intros; elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13; intros; apply H15. @@ -1811,7 +1811,7 @@ Proof. apply H14; split; [ unfold D_x, no_cond; split; [ trivial | assumption ] | apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H15 | apply Rmin_l ] ]. - assert (H13 := completeness _ H11 H12); elim H13; clear H13; intros; + destruct (completeness _ H11 H12) as (x0,p). cut (0 < x0 <= M - m). intro; elim H13; clear H13; intros; exists x0; split. assumption. |