diff options
Diffstat (limited to 'theories/Reals/AltSeries.v')
-rw-r--r-- | theories/Reals/AltSeries.v | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index 6d54b791..3e99c989 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.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 *) @@ -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)). @@ -442,7 +438,7 @@ Proof. unfold Rdiv in H; apply Rlt_le_trans with (sum_f_R0 (tg_alt PI_tg) (S (2 * 0))). simpl; unfold tg_alt; simpl; rewrite Rmult_1_l; - rewrite Rmult_1_r; apply Rplus_lt_reg_r with (PI_tg 1). + rewrite Rmult_1_r; apply Rplus_lt_reg_l with (PI_tg 1). rewrite Rplus_0_r; replace (PI_tg 1 + (PI_tg 0 + -1 * PI_tg 1)) with (PI_tg 0); [ unfold PI_tg | ring ]. |