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/AltSeries.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/AltSeries.v')
| -rw-r--r-- | theories/Reals/AltSeries.v | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index cb3c762cd..73d288aee 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -156,8 +156,7 @@ Proof. intros. assert (H2 := CV_ALT_step0 _ H). assert (H3 := CV_ALT_step4 _ H H0). - assert (X := growing_cv _ H2 H3). - elim X; intros. + destruct (growing_cv _ H2 H3) as (x,p). exists x. unfold Un_cv; unfold R_dist; unfold Un_cv in H1; unfold R_dist in H1; unfold Un_cv in p; unfold R_dist in p. @@ -388,16 +387,13 @@ Proof. apply Rle_ge; apply PI_tg_pos. apply lt_le_trans with N; assumption. elim H1; intros H5 _. - assert (H6 := lt_eq_lt_dec 0 N). - elim H6; intro. - elim a; intro. + destruct (lt_eq_lt_dec 0 N) as [[| <- ]|H6]. assumption. - rewrite <- b in H4. rewrite H4 in H5. simpl in H5. cut (0 < / (2 * eps)); [ intro | apply Rinv_0_lt_compat; assumption ]. - elim (Rlt_irrefl _ (Rlt_trans _ _ _ H7 H5)). - elim (lt_n_O _ b). + elim (Rlt_irrefl _ (Rlt_trans _ _ _ H6 H5)). + elim (lt_n_O _ H6). apply le_IZR. simpl. left; apply Rlt_trans with (/ (2 * eps)). |