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 ].