Make standard library independent of the names generated by

induction/elim over a dependent elimination principle for Prop
arguments.

20 files changed, 259 insertions, 324 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index a92b3584b..c4416e5d8 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -35,10 +35,8 @@ Proof.
     [ intro | apply Rinv_0_lt_compat; prove_sup0 ].
   elim (H0 (/ 2) H1); intros.
   exists (sum_f_R0 An x + 2 * An (S x)).
-  unfold is_upper_bound; intros; unfold EUn in H3; elim H3; intros.
-  rewrite H4; assert (H5 := lt_eq_lt_dec x1 x).
-  elim H5; intros.
-  elim a; intro.
+  unfold is_upper_bound; intros; unfold EUn in H3; destruct H3 as (x1,->).
+  destruct (lt_eq_lt_dec x1 x) as [[| -> ]|].
   replace (sum_f_R0 An x) with
     (sum_f_R0 An x1 + sum_f_R0 (fun i:nat => An (S x1 + i)%nat) (x - S x1)).
   pattern (sum_f_R0 An x1) at 1; rewrite <- Rplus_0_r;
@@ -47,7 +45,7 @@ Proof.
   apply tech1; intros; apply H.
   apply Rmult_lt_0_compat; [ prove_sup0 | apply H ].
   symmetry ; apply tech2; assumption.
-  rewrite b; pattern (sum_f_R0 An x) at 1; rewrite <- Rplus_0_r;
+  pattern (sum_f_R0 An x) at 1; rewrite <- Rplus_0_r;
     apply Rplus_le_compat_l.
   left; apply Rmult_lt_0_compat; [ prove_sup0 | apply H ].
   replace (sum_f_R0 An x1) with
@@ -86,8 +84,8 @@ Proof.
   apply (tech6 (fun i:nat => An (S x + i)%nat) (/ 2)).
   left; apply Rinv_0_lt_compat; prove_sup0.
   intro; cut (forall n:nat, (n >= x)%nat -> An (S n) < / 2 * An n).
-  intro; replace (S x + S i)%nat with (S (S x + i)).
-  apply H6; unfold ge; apply tech8.
+  intro H4; replace (S x + S i)%nat with (S (S x + i)).
+  apply H4; unfold ge; apply tech8.
   apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; do 2 rewrite S_INR; ring.
   intros; unfold R_dist in H2; apply Rmult_lt_reg_l with (/ An n).
   apply Rinv_0_lt_compat; apply H.
@@ -101,17 +99,17 @@ Proof.
   unfold Rdiv; reflexivity.
   left; unfold Rdiv; change (0 < An (S n) * / An n);
     apply Rmult_lt_0_compat; [ apply H | apply Rinv_0_lt_compat; apply H ].
-  red; intro; assert (H8 := H n); rewrite H7 in H8;
+  intro H5; assert (H8 := H n); rewrite H5 in H8;
     elim (Rlt_irrefl _ H8).
   replace (S x + 0)%nat with (S x); [ reflexivity | ring ].
   symmetry ; apply tech2; assumption.
   exists (sum_f_R0 An 0); unfold EUn; exists 0%nat; reflexivity.
-  intro X; elim X; intros.
+  intros (x,H1).
   exists x; apply Un_cv_crit_lub;
     [ unfold Un_growing; intro; rewrite tech5;
       pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r;
 	apply Rplus_le_compat_l; left; apply H
-      | apply p ].
+      | apply H1 ].
 Defined.
 
 Lemma Alembert_C2 :
@@ -127,14 +125,12 @@ Proof.
   intro; cut (forall n:nat, 0 < Wn n).
   intro; cut (Un_cv (fun n:nat => Rabs (Vn (S n) / Vn n)) 0).
   intro; cut (Un_cv (fun n:nat => Rabs (Wn (S n) / Wn n)) 0).
-  intro; assert (H5 := Alembert_C1 Vn H1 H3).
-  assert (H6 := Alembert_C1 Wn H2 H4).
-  elim H5; intros.
-  elim H6; intros.
+  intro; pose proof (Alembert_C1 Vn H1 H3) as (x,p).
+  pose proof (Alembert_C1 Wn H2 H4) as (x0,p0).
   exists (x - x0); unfold Un_cv; unfold Un_cv in p;
     unfold Un_cv in p0; intros; cut (0 < eps / 2).
-  intro; elim (p (eps / 2) H8); clear p; intros.
-  elim (p0 (eps / 2) H8); clear p0; intros.
+  intro H6; destruct (p (eps / 2) H6) as (x1,H8). clear p.
+  destruct (p0 (eps / 2) H6) as (x2,H9). clear p0.
   set (N := max x1 x2).
   exists N; intros;
     replace (sum_f_R0 An n) with (sum_f_R0 Vn n - sum_f_R0 Wn n).
@@ -146,9 +142,9 @@ Proof.
   apply Rabs_triang.
   rewrite Rabs_Ropp; apply Rlt_le_trans with (eps / 2 + eps / 2).
   apply Rplus_lt_compat.
-  unfold R_dist in H9; apply H9; unfold ge; apply le_trans with N;
+  unfold R_dist in H8; apply H8; unfold ge; apply le_trans with N;
     [ unfold N; apply le_max_l | assumption ].
-  unfold R_dist in H10; apply H10; unfold ge; apply le_trans with N;
+  unfold R_dist in H9; apply H9; unfold ge; apply le_trans with N;
     [ unfold N; apply le_max_r | assumption ].
   right; symmetry ; apply double_var.
   symmetry ; apply tech11; intro; unfold Vn, Wn;
@@ -344,9 +340,8 @@ Proof.
   intros; set (Bn := fun i:nat => An i * x ^ i).
   cut (forall n:nat, Bn n <> 0).
   intro; cut (Un_cv (fun n:nat => Rabs (Bn (S n) / Bn n)) 0).
-  intro; assert (H4 := Alembert_C2 Bn H2 H3).
-  elim H4; intros.
-  exists x0; unfold Bn in p; apply tech12; assumption.
+  intro; destruct (Alembert_C2 Bn H2 H3) as (x0,H4).
+  exists x0; unfold Bn in H4; apply tech12; assumption.
   unfold Un_cv; intros; unfold Un_cv in H1; cut (0 < eps / Rabs x).
   intro; elim (H1 (eps / Rabs x) H4); intros.
   exists x0; intros; unfold R_dist; unfold Rminus;
@@ -431,9 +426,7 @@ Proof.
   unfold is_upper_bound; intros; unfold EUn in H6.
   elim H6; intros.
   rewrite H7.
-  assert (H8 := lt_eq_lt_dec x2 x0).
-  elim H8; intros.
-  elim a; intro.
+  destruct (lt_eq_lt_dec x2 x0) as [[| -> ]|].
   replace (sum_f_R0 An x0) with
     (sum_f_R0 An x2 + sum_f_R0 (fun i:nat => An (S x2 + i)%nat) (x0 - S x2)).
   pattern (sum_f_R0 An x2) at 1; rewrite <- Rplus_0_r.
@@ -446,7 +439,7 @@ Proof.
     replace (x + (1 - x)) with 1; [ elim H3; intros; assumption | ring ].
   apply H.
   symmetry ; apply tech2; assumption.
-  rewrite b; pattern (sum_f_R0 An x0) at 1; rewrite <- Rplus_0_r;
+  pattern (sum_f_R0 An x0) at 1; rewrite <- Rplus_0_r;
     apply Rplus_le_compat_l.
   left; apply Rmult_lt_0_compat.
   apply Rinv_0_lt_compat; apply Rplus_lt_reg_l with x; rewrite Rplus_0_r;
@@ -520,12 +513,12 @@ Proof.
   replace (S x0 + 0)%nat with (S x0); [ reflexivity | ring ].
   symmetry ; apply tech2; assumption.
   exists (sum_f_R0 An 0); unfold EUn; exists 0%nat; reflexivity.
-  intro X; elim X; intros.
+  intros (x,H1).
   exists x; apply Un_cv_crit_lub;
     [ unfold Un_growing; intro; rewrite tech5;
       pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r;
 	apply Rplus_le_compat_l; left; apply H
-      | apply p ].
+      | apply H1].
 Qed.
 
 Lemma Alembert_C5 :
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)).
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 160f3d480..88c6f9c48 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -86,18 +86,17 @@ Qed.
 
 Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat.
 Proof.
-  intros; induction  N as [| N HrecN].
-  elim (lt_n_O _ H).
-  cut ((1 < N)%nat \/ N = 1%nat).
-  intro; elim H0; intro.
-  assert (H2 := even_odd_dec N).
-  elim H2; intro.
-  rewrite <- (even_div2 _ a); apply HrecN; assumption.
-  rewrite <- (odd_div2 _ b); apply lt_O_Sn.
-  rewrite H1; simpl; apply lt_O_Sn.
-  inversion H.
-  right; reflexivity.
-  left; apply lt_le_trans with 2%nat; [ apply lt_n_Sn | apply H1 ].
+  intros; induction N as [| N HrecN].
+  - elim (lt_n_O _ H).
+  - cut ((1 < N)%nat \/ N = 1%nat).
+    { intro; elim H0; intro.
+      + destruct (even_odd_dec N) as [Heq|Heq].
+        * rewrite <- (even_div2 _ Heq); apply HrecN; assumption.
+        * rewrite <- (odd_div2 _ Heq); apply lt_O_Sn.
+      + rewrite H1; simpl; apply lt_O_Sn. }
+    inversion H.
+    right; reflexivity.
+    left; apply lt_le_trans with 2%nat; [ apply lt_n_Sn | apply H1 ].
 Qed.
 
 Lemma Reste_E_maj :
@@ -857,8 +856,7 @@ Proof.
         Un_cv
         (fun n:nat =>
           sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l }.
-  intro X.
-  elim X; intros.
+  intros (x,p).
   exists x; intros.
   split.
   apply p.
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index 928422ed8..e0bb8ee2b 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -98,7 +98,7 @@ Lemma NewtonInt_P5 :
     Newton_integrable (fun x:R => l * f x + g x) a b.
 Proof.
   unfold Newton_integrable; intros f g l a b X X0;
-    elim X; intros; elim X0; intros;
+    elim X; intros x p; elim X0; intros x0 p0;
       exists (fun y:R => l * x y + x0 y).
   elim p; intro.
   elim p0; intro.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 10c3327f2..d559efbce 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -180,12 +180,9 @@ Proof.
   replace (S (S (pred N))) with (S N).
   rewrite (HrecN H1); ring.
   rewrite H2; simpl; reflexivity.
-  assert (H2 := O_or_S N).
-  elim H2; intros.
-  elim a; intros.
-  rewrite <- p.
+  destruct (O_or_S N) as [(m,<-)|<-].
   simpl; reflexivity.
-  rewrite <- b in H1; elim (lt_irrefl _ H1).
+  elim (lt_irrefl _ H1).
   rewrite H1; simpl; reflexivity.
   inversion H.
   right; reflexivity.
@@ -395,9 +392,7 @@ Proof.
       (sum_f_R0 (fun i:nat => Rabs (An i)) m)).
   assumption.
   apply H1; assumption.
-  assert (H4 := lt_eq_lt_dec n m).
-  elim H4; intro.
-  elim a; intro.
+  destruct (lt_eq_lt_dec n m) as [[ | -> ]|].
   rewrite (tech2 An n m); [ idtac | assumption ].
   rewrite (tech2 (fun i:nat => Rabs (An i)) n m); [ idtac | assumption ].
   unfold R_dist.
@@ -418,7 +413,6 @@ Proof.
   apply Rle_ge.
   apply cond_pos_sum.
   intro; apply Rabs_pos.
-  rewrite b.
   unfold R_dist.
   unfold Rminus; do 2 rewrite Rplus_opp_r.
   rewrite Rabs_R0; right; reflexivity.
@@ -451,8 +445,7 @@ Lemma cv_cauchy_1 :
     { l:R | Un_cv (fun N:nat => sum_f_R0 An N) l } ->
     Cauchy_crit_series An.
 Proof.
-  intros An X.
-  elim X; intros.
+  intros An (x,p).
   unfold Un_cv in p.
   unfold Cauchy_crit_series; unfold Cauchy_crit.
   intros.
diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index 6d42434a4..e75a4c17d 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.v
@@ -181,13 +181,13 @@ Proof.
   elim Hrecl; intros; assert (H3 := H1 H0); elim H3; intros; elim H4; intros;
     exists (S x0); split;
       [ simpl; apply lt_n_S; assumption | simpl; assumption ].
-  elim H; intros; elim H0; intros; elim (zerop x0); intro.
-  rewrite a in H2; simpl in H2; left; assumption.
-  right; elim Hrecl; intros; apply H4; assert (H5 : S (pred x0) = x0).
+  elim H; intros; elim H0; intros; destruct (zerop x0) as [->|].
+  simpl in H2; left; assumption.
+  right; elim Hrecl; intros H4 H5; apply H5; assert (H6 : S (pred x0) = x0).
   symmetry ; apply S_pred with 0%nat; assumption.
   exists (pred x0); split;
-    [ simpl in H1; apply lt_S_n; rewrite H5; assumption
-      | rewrite <- H5 in H2; simpl in H2; assumption ].
+    [ simpl in H1; apply lt_S_n; rewrite H6; assumption
+      | rewrite <- H6 in H2; simpl in H2; assumption ].
 Qed.
 
 Lemma Rlist_P1 :
@@ -208,11 +208,11 @@ Proof.
   assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0);
     intros; elim H5; clear H5; intros; split.
   simpl; rewrite H5; reflexivity.
-  intros; elim (zerop i); intro.
-  rewrite a; simpl; assumption.
-  assert (H8 : i = S (pred i)).
+  intros; destruct (zerop i) as [->|].
+  simpl; assumption.
+  assert (H9 : i = S (pred i)).
   apply S_pred with 0%nat; assumption.
-  rewrite H8; simpl; apply H6; simpl in H7; apply lt_S_n; rewrite <- H8;
+  rewrite H9; simpl; apply H6; simpl in H7; apply lt_S_n; rewrite <- H9;
     assumption.
 Qed.
 
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 0409c99e4..6afc20f5a 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -1066,15 +1066,8 @@ Lemma pr_nu :
   forall f (x:R) (pr1 pr2:derivable_pt f x),
     derive_pt f x pr1 = derive_pt f x pr2.
 Proof.
-  intros.
-  unfold derivable_pt in pr1.
-  unfold derivable_pt in pr2.
-  elim pr1; intros.
-  elim pr2; intros.
-  unfold derivable_pt_abs in p.
-  unfold derivable_pt_abs in p0.
-  simpl.
-  apply (uniqueness_limite f x x0 x1 p p0).
+  intros f x (x0,H0) (x1,H1).
+  apply (uniqueness_limite f x x0 x1 H0 H1).
 Qed.
 
 
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index 663f62f7a..dd8e0dd52 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -26,7 +26,7 @@ Proof.
   apply derivable_pt_const.
   assumption.
   assumption.
-  unfold div_fct, inv_fct, fct_cte; intro X0; elim X0; intros;
+  unfold div_fct, inv_fct, fct_cte; intros (x0,p);
     unfold derivable_pt; exists x0;
       unfold derivable_pt_abs; unfold derivable_pt_lim;
         unfold derivable_pt_abs in p; unfold derivable_pt_lim in p;
@@ -41,11 +41,7 @@ Lemma pr_nu_var :
   forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x),
     f = g -> derive_pt f x pr1 = derive_pt g x pr2.
 Proof.
-  unfold derivable_pt, derive_pt; intros.
-  elim pr1; intros.
-  elim pr2; intros.
-  simpl.
-  rewrite H in p.
+  unfold derivable_pt, derive_pt; intros f g x (x0,p0) (x1,p1) ->.
   apply uniqueness_limite with g x; assumption.
 Qed.
 
@@ -54,14 +50,11 @@ Lemma pr_nu_var2 :
   forall (f g:R -> R) (x:R) (pr1:derivable_pt f x) (pr2:derivable_pt g x),
     (forall h:R, f h = g h) -> derive_pt f x pr1 = derive_pt g x pr2.
 Proof.
-  unfold derivable_pt, derive_pt; intros.
-  elim pr1; intros.
-  elim pr2; intros.
-  simpl.
-  assert (H0 := uniqueness_step2 _ _ _ p).
-  assert (H1 := uniqueness_step2 _ _ _ p0).
+  unfold derivable_pt, derive_pt; intros f g x (x0,p0) (x1,p1) H.
+  assert (H0 := uniqueness_step2 _ _ _ p0).
+  assert (H1 := uniqueness_step2 _ _ _ p1).
   cut (limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) x1 0).
-  intro; assert (H3 := uniqueness_step1 _ _ _ _ H0 H2).
+  intro H2; assert (H3 := uniqueness_step1 _ _ _ _ H0 H2).
   assumption.
   unfold limit1_in; unfold limit_in; unfold dist;
     simpl; unfold R_dist; unfold limit1_in in H1;
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index 6f8dcdc71..f787aa630 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -165,8 +165,8 @@ assert (forall x l, lb < x < ub -> (derivable_pt_abs f x l <-> derivable_pt_abs
  apply Rlt_le_trans with (r2:=Rmin delta (Rmin (ub - a) (a - lb))) ; [| apply Rmin_r] ; assumption.
  unfold derivable_pt in Prf.
   unfold derivable_pt in Prg.
-  elim Prf; intros.
-  elim Prg; intros.
+  elim Prf; intros x0 p.
+  elim Prg; intros x1 p0.
   assert (Temp := p); rewrite H in Temp.
   unfold derivable_pt_abs in p.
   unfold derivable_pt_abs in p0.
@@ -295,8 +295,8 @@ intros. (* f x y f_cont_interv x_lt_y fx_neg fy_pos.*)
   generalize (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3). 
   generalize (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3). 
   intros X X0.
-  elim X; intros.
-  elim X0; intros.
+  elim X; intros x0 p.
+  elim X0; intros x1 p0.
   assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p).
   rewrite H4 in p0.
   exists x0.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index daf895fd2..c189b0333 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -276,9 +276,9 @@ Qed.
 (*********)
 Lemma Rcase_abs : forall r, {r < 0} + {r >= 0}.
 Proof.
-  intro; generalize (Rle_dec 0 r); intro X; elim X; intro; clear X.
-  right; apply (Rle_ge 0 r a).
-  left; fold (0 > r); apply (Rnot_le_lt 0 r b).
+  intro; generalize (Rle_dec 0 r); intro X; elim X; intro H; clear X.
+  right; apply (Rle_ge 0 r H).
+  left; fold (0 > r); apply (Rnot_le_lt 0 r H).
 Qed.
 
 (*********)
diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v
index 8e0e0692c..b9150c181 100644
--- a/theories/Reals/Rcomplete.v
+++ b/theories/Reals/Rcomplete.v
@@ -27,21 +27,19 @@ Proof.
   intros.
   set (Vn := sequence_minorant Un (cauchy_min Un H)).
   set (Wn := sequence_majorant Un (cauchy_maj Un H)).
-  assert (H0 := maj_cv Un H).
-  fold Wn in H0.
-  assert (H1 := min_cv Un H).
-  fold Vn in H1.
-  elim H0; intros.
-  elim H1; intros.
+  pose proof (maj_cv Un H) as (x,p).
+  fold Wn in p.
+  pose proof (min_cv Un H) as (x0,p0).
+  fold Vn in p0.
   cut (x = x0).
-  intros.
+  intros H2.
   exists x.
   rewrite <- H2 in p0.
   unfold Un_cv.
   intros.
   unfold Un_cv in p; unfold Un_cv in p0.
   cut (0 < eps / 3).
-  intro.
+  intro H4.
   elim (p (eps / 3) H4); intros.
   elim (p0 (eps / 3) H4); intros.
   exists (max x1 x2).
@@ -83,20 +81,20 @@ Proof.
   [ apply Rabs_triang | ring ].
   apply Rlt_le_trans with (eps / 3 + eps / 3 + eps / 3).
   repeat apply Rplus_lt_compat.
-  unfold R_dist in H5.
-  apply H5.
+  unfold R_dist in H1.
+  apply H1.
   unfold ge; apply le_trans with (max x1 x2).
   apply le_max_l.
   assumption.
   rewrite <- Rabs_Ropp.
   replace (- (x - Vn n)) with (Vn n - x); [ idtac | ring ].
-  unfold R_dist in H6.
-  apply H6.
+  unfold R_dist in H3.
+  apply H3.
   unfold ge; apply le_trans with (max x1 x2).
   apply le_max_r.
   assumption.
-  unfold R_dist in H6.
-  apply H6.
+  unfold R_dist in H3.
+  apply H3.
   unfold ge; apply le_trans with (max x1 x2).
   apply le_max_r.
   assumption.
@@ -112,11 +110,11 @@ Proof.
   intro.
   unfold Un_cv in p; unfold Un_cv in p0.
   unfold R_dist in p; unfold R_dist in p0.
-  elim (p (eps / 5) H3); intros N1 H4.
-  elim (p0 (eps / 5) H3); intros N2 H5.
+  elim (p (eps / 5) H1); intros N1 H4.
+  elim (p0 (eps / 5) H1); intros N2 H5.
   unfold Cauchy_crit in H.
   unfold R_dist in H.
-  elim (H (eps / 5) H3); intros N3 H6.
+  elim (H (eps / 5) H1); intros N3 H6.
   set (N := max (max N1 N2) N3).
   apply Rle_lt_trans with (Rabs (x - Wn N) + Rabs (Wn N - x0)).
   replace (x - x0) with (x - Wn N + (Wn N - x0)); [ apply Rabs_triang | ring ].
@@ -146,12 +144,11 @@ Proof.
   cut
     (Vn N =
       minorant (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))).
-  intros.
-  rewrite <- H9; rewrite <- H10.
-  rewrite <- H9 in H8.
-  rewrite <- H10 in H7.
-  elim (H7 (eps / 5) H3); intros k2 H11.
-  elim (H8 (eps / 5) H3); intros k1 H12.
+  intros H9 H10.
+  rewrite <- H9 in H8 |- *.
+  rewrite <- H10 in H7 |- *.
+  elim (H7 (eps / 5) H1); intros k2 H11.
+  elim (H8 (eps / 5) H1); intros k1 H12.
   apply Rle_lt_trans with
     (Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Vn N)).
   replace (Wn N - Vn N) with
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 1445e7dbe..0dc3329ee 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -49,8 +49,8 @@ Lemma RiemannInt_P1 :
   forall (f:R -> R) (a b:R),
     Riemann_integrable f a b -> Riemann_integrable f b a.
 Proof.
-  unfold Riemann_integrable; intros; elim (X eps); clear X; intros;
-    elim p; clear p; intros; exists (mkStepFun (StepFun_P6 (pre x)));
+  unfold Riemann_integrable; intros; elim (X eps); clear X; intros.
+  elim p; clear p; intros x0 p; exists (mkStepFun (StepFun_P6 (pre x)));
       exists (mkStepFun (StepFun_P6 (pre x0)));
         elim p; clear p; intros; split.
   intros; apply (H t); elim H1; clear H1; intros; split;
@@ -171,7 +171,7 @@ Proof.
   rewrite Rabs_Ropp; apply H4.
   rewrite Rabs_Ropp in H4; apply H4.
   apply H4.
-  assert (H3 := RiemannInt_P2 _ _ _ _ H H1 H2); elim H3; intros;
+  assert (H3 := RiemannInt_P2 _ _ _ _ H H1 H2); elim H3; intros x p;
     exists (- x); unfold Un_cv; unfold Un_cv in p;
       intros; elim (p _ H4); intros; exists x0; intros;
         generalize (H5 _ H6); unfold R_dist, RiemannInt_SF;
@@ -423,7 +423,7 @@ Proof.
   exists 0%nat; unfold I; rewrite Rmult_0_l; rewrite Rplus_0_r;
     assumption.
   cut (Nbound I).
-  intro; assert (H2 := Nzorn H0 H1); elim H2; intros; exists x; elim p; intros;
+  intro; assert (H2 := Nzorn H0 H1); elim H2; intros x p; exists x; elim p; intros;
     split.
   apply H3.
   destruct (total_order_T (a + INR (S x) * del) b) as [[Hlt|Heq]|Hgt].
@@ -497,7 +497,7 @@ Proof.
             | apply Rmin_r ]
           | intros; apply H3; try assumption; apply Rlt_le_trans with (Rmin x (b - a));
             [ assumption | apply Rmin_l ] ].
-  assert (H3 := completeness E H1 H2); elim H3; intros; cut (0 < x <= b - a).
+  assert (H3 := completeness E H1 H2); elim H3; intros x p; cut (0 < x <= b - a).
   intro; elim H4; clear H4; intros; exists (mkposreal _ H4); split.
   apply H5.
   unfold is_lub in p; elim p; intros; unfold is_upper_bound in H6;
@@ -535,7 +535,7 @@ Lemma Heine_cor2 :
           a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps }.
 Proof.
   intro f; intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt].
-  assert (H0 := Heine_cor1 Hlt H eps); elim H0; intros; exists x;
+  assert (H0 := Heine_cor1 Hlt H eps); elim H0; intros x p; exists x;
     elim p; intros; apply H2; assumption.
   exists (mkposreal _ Rlt_0_1); intros; assert (H3 : x = y);
     [ elim H0; elim H1; intros; rewrite Heq in H3, H5;
@@ -993,11 +993,10 @@ Qed.
 
 Lemma Req_EM_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.
 Proof.
-  intros; elim (total_order_T r1 r2); intros;
-    [ elim a; intro;
-      [ right; red; intro; rewrite H in a0; elim (Rlt_irrefl r2 a0)
-        | left; assumption ]
-      | right; red; intro; rewrite H in b; elim (Rlt_irrefl r2 b) ].
+  intros; destruct (total_order_T r1 r2) as [[H|]|H].
+  - right; red; intros ->; elim (Rlt_irrefl r2 H).
+  - left; assumption.
+  - right; red; intros ->; elim (Rlt_irrefl r2 H).
 Qed.
 
 (* L1([a,b]) is a vectorial space *)
@@ -1008,7 +1007,7 @@ Lemma RiemannInt_P10 :
     Riemann_integrable (fun x:R => f x + l * g x) a b.
 Proof.
   unfold Riemann_integrable; intros f g; intros; destruct (Req_EM_T l 0) as [Heq|Hneq].
-  elim (X eps); intros; split with x; elim p; intros; split with x0; elim p0;
+  elim (X eps); intros x p; split with x; elim p; intros x0 p0; split with x0; elim p0;
     intros; split; try assumption; rewrite Heq; intros;
       rewrite Rmult_0_l; rewrite Rplus_0_r; apply H; assumption.
   assert (H : 0 < eps / 2).
@@ -1019,9 +1018,9 @@ Proof.
     [ apply (cond_pos eps)
       | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat;
         [ prove_sup0 | apply Rabs_pos_lt; assumption ] ].
-  elim (X (mkposreal _ H)); intros; elim (X0 (mkposreal _ H0)); intros;
+  elim (X (mkposreal _ H)); intros x p; elim (X0 (mkposreal _ H0)); intros x0 p0;
     split with (mkStepFun (StepFun_P28 l x x0)); elim p0;
-      elim p; intros; split with (mkStepFun (StepFun_P28 (Rabs l) x1 x2));
+      elim p; intros x1 p1 x2 p2. split with (mkStepFun (StepFun_P28 (Rabs l) x1 x2));
         elim p1; elim p2; clear p1 p2 p0 p X X0; intros; split.
   intros; simpl;
     apply Rle_trans with (Rabs (f t - x t) + Rabs (l * (g t - x0 t))).
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 9466ed8e6..d2c04f556 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -40,26 +40,25 @@ Proof.
   assert (H2 :  exists x : R, E x).
   elim H; intros; exists (INR x); unfold E; exists x; split;
     [ assumption | reflexivity ].
-  assert (H3 := completeness E H1 H2); elim H3; intros; unfold is_lub in p;
-    elim p; clear p; intros; unfold is_upper_bound in H4, H5;
+  destruct (completeness E H1 H2) as (x,(H4,H5)); unfold is_upper_bound in H4, H5;
       assert (H6 : 0 <= x).
-  elim H2; intros; unfold E in H6; elim H6; intros; elim H7; intros;
+  destruct H2 as (x0,H6). remember H6 as H7. destruct H7 as (x1,(H8,H9)).
     apply Rle_trans with x0;
       [ rewrite <- H9; change (INR 0 <= INR x1); apply le_INR;
         apply le_O_n
         | apply H4; assumption ].
   assert (H7 := archimed x); elim H7; clear H7; intros;
     assert (H9 : x <= IZR (up x) - 1).
-  apply H5; intros; assert (H10 := H4 _ H9); unfold E in H9; elim H9; intros;
-    elim H11; intros; rewrite <- H13; apply Rplus_le_reg_l with 1;
+  apply H5; intros x0 H9. assert (H10 := H4 _ H9); unfold E in H9; elim H9; intros x1 (H12,<-).
+    apply Rplus_le_reg_l with 1;
       replace (1 + (IZR (up x) - 1)) with (IZR (up x));
       [ idtac | ring ]; replace (1 + INR x1) with (INR (S x1));
       [ idtac | rewrite S_INR; ring ].
   assert (H14 : (0 <= up x)%Z).
   apply le_IZR; apply Rle_trans with x; [ apply H6 | left; assumption ].
-  assert (H15 := IZN _ H14); elim H15; clear H15; intros; rewrite H15;
-    rewrite <- INR_IZR_INZ; apply le_INR; apply lt_le_S;
-      apply INR_lt; rewrite H13; apply Rle_lt_trans with x;
+  destruct (IZN _ H14) as (x2,H15).
+    rewrite H15, <- INR_IZR_INZ; apply le_INR; apply lt_le_S.
+      apply INR_lt; apply Rle_lt_trans with x;
         [ assumption | rewrite INR_IZR_INZ; rewrite <- H15; assumption ].
   assert (H10 : x = IZR (up x) - 1).
   apply Rle_antisym;
@@ -84,18 +83,18 @@ Proof.
   cut (x = INR (pred x0)).
   intro; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18;
     rewrite <- H19; assumption.
-  rewrite H10; rewrite p; rewrite <- INR_IZR_INZ; replace 1 with (INR 1);
+  rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; replace 1 with (INR 1);
     [ idtac | reflexivity ]; rewrite <- minus_INR.
   replace (x0 - 1)%nat with (pred x0);
   [ reflexivity
     | case x0; [ reflexivity | intro; simpl; apply minus_n_O ] ].
-  induction  x0 as [| x0 Hrecx0];
-    [ rewrite p in H7; rewrite <- INR_IZR_INZ in H7; simpl in H7;
-      elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H7))
-      | apply le_n_S; apply le_O_n ].
-  rewrite H15 in H13; elim H12; assumption.
+  induction x0 as [|x0 Hrecx0].
+    rewrite H8 in H3. rewrite <- INR_IZR_INZ in H3; simpl in H3.
+      elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H3)).
+    apply le_n_S; apply le_O_n.
+    rewrite H15 in H13; elim H12; assumption.
   split with (pred x0); unfold E in H13; elim H13; intros; elim H12; intros;
-    rewrite H10 in H15; rewrite p in H15; rewrite <- INR_IZR_INZ in H15;
+    rewrite H10 in H15; rewrite H8 in H15; rewrite <- INR_IZR_INZ in H15;
       assert (H16 : INR x0 = INR x1 + 1).
   rewrite H15; ring.
   rewrite <- S_INR in H16; assert (H17 := INR_eq _ _ H16); rewrite H17;
@@ -1202,13 +1201,13 @@ Proof.
   [ apply lt_n_S; assumption
     | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red;
       intro; rewrite <- H22 in H21; elim (lt_n_O _ H21) ].
-  elim (Rle_dec (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro.
+  elim (Rle_dec (pos_Rl lf (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro a0.
   assert (H23 : (S x0 <= x0)%nat).
   apply H20; unfold I; split; assumption.
   elim (le_Sn_n _ H23).
   assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lf (S x0)).
   auto with real.
-  clear b0; apply RList_P17; try assumption.
+  clear a0; apply RList_P17; try assumption.
   apply RList_P2; assumption.
   elim (RList_P9 lf lg (pos_Rl lf (S x0))); intros; apply H25; left;
     elim (RList_P3 lf (pos_Rl lf (S x0))); intros; apply H27;
@@ -1450,12 +1449,12 @@ Proof.
   apply lt_n_S; assumption.
   symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red;
     intro; rewrite <- H22 in H21; elim (lt_n_O _ H21).
-  elim (Rle_dec (pos_Rl lg (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro.
+  elim (Rle_dec (pos_Rl lg (S x0)) (pos_Rl (cons_ORlist lf lg) i)); intro a0.
   assert (H23 : (S x0 <= x0)%nat);
     [ apply H20; unfold I; split; assumption | elim (le_Sn_n _ H23) ].
   assert (H23 : pos_Rl (cons_ORlist lf lg) i < pos_Rl lg (S x0)).
   auto with real.
-  clear b0; apply RList_P17; try assumption;
+  clear a0; apply RList_P17; try assumption;
     [ apply RList_P2; assumption
       | elim (RList_P9 lf lg (pos_Rl lg (S x0))); intros; apply H25; right;
         elim (RList_P3 lg (pos_Rl lg (S x0))); intros;
@@ -2423,7 +2422,7 @@ Proof.
     discriminate.
   clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}).
   case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ].
-  elim H1; intro.
+  elim H1; intro a0.
   split with (cons r (cons c nil)); split with (cons r3 nil);
     unfold adapted_couple in H; decompose [and] H; clear H;
       assert (H6 : r = a).
@@ -2534,7 +2533,7 @@ Proof.
     discriminate.
   clear Hreclf1; assert (H1 : {c <= r1} + {r1 < c}).
   case (Rle_dec c r1); intro; [ left; assumption | right; auto with real ].
-  elim H1; intro.
+  elim H1; intro a0.
   split with (cons c (cons r1 r2)); split with (cons r3 lf1);
     unfold adapted_couple in H; decompose [and] H; clear H;
       unfold adapted_couple; repeat split.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index f9ad64b86..2e3d7f167 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -423,18 +423,15 @@ Lemma dicho_lb_car :
     P x = false -> P (dicho_lb x y P n) = false.
 Proof.
   intros.
-  induction  n as [| n Hrecn].
-  simpl.
-  assumption.
-  simpl.
-  assert
-    (X :=
-      sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))).
-  elim X; intro.
-  rewrite a.
-  unfold dicho_lb in Hrecn; assumption.
-  rewrite b.
-  assumption.
+  induction n as [| n Hrecn].
+  - assumption.
+  - simpl.
+    destruct
+        (sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))) as [Heq|Heq].
+    + rewrite Heq.
+      unfold dicho_lb in Hrecn; assumption.
+    + rewrite Heq.
+      assumption.
 Qed.
 
 Lemma dicho_up_car :
@@ -442,18 +439,15 @@ Lemma dicho_up_car :
     P y = true -> P (dicho_up x y P n) = true.
 Proof.
   intros.
-  induction  n as [| n Hrecn].
-  simpl.
-  assumption.
-  simpl.
-  assert
-    (X :=
-      sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))).
-  elim X; intro.
-  rewrite a.
-  unfold dicho_lb in Hrecn; assumption.
-  rewrite b.
-  assumption.
+  induction n as [| n Hrecn].
+  - assumption.
+  - simpl.
+    destruct
+      (sumbool_of_bool (P ((Dichotomy_lb x y P n + Dichotomy_ub x y P n) / 2))) as [Heq|Heq].
+    + rewrite Heq.
+      unfold dicho_lb in Hrecn; assumption.
+    + rewrite  Heq.
+      assumption.
 Qed.
 
 (** Intermediate Value Theorem *)
@@ -463,13 +457,9 @@ Lemma IVT :
     x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }.
 Proof.
   intros.
-  cut (x <= y).
-  intro.
-  generalize (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3).
-  generalize (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3).
-  intros X X0.
-  elim X; intros.
-  elim X0; intros.
+  assert (x <= y) by (left; assumption).
+  destruct (dicho_lb_cv x y (fun z:R => cond_positivity (f z)) H3) as (x1,p0).
+  destruct (dicho_up_cv x y (fun z:R => cond_positivity (f z)) H3) as (x0,p).
   assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p).
   rewrite H4 in p0.
   exists x0.
@@ -486,7 +476,6 @@ Proof.
   apply dicho_up_decreasing; assumption.
   assumption.
   right; reflexivity.
-  2: left; assumption.
   set (Vn := fun n:nat => dicho_lb x y (fun z:R => cond_positivity (f z)) n).
   set (Wn := fun n:nat => dicho_up x y (fun z:R => cond_positivity (f z)) n).
   cut ((forall n:nat, f (Vn n) <= 0) -> f x0 <= 0).
@@ -612,9 +601,8 @@ Proof.
   cut ((- f)%F x < 0).
   cut (0 < (- f)%F y).
   intros.
-  elim (H3 H5 H4); intros.
+  destruct (H3 H5 H4) as (x0,[]).
   exists x0.
-  elim p; intros.
   split.
   assumption.
   unfold opp_fct in H7.
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.
diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v
index e42610424..1f488aa9e 100644
--- a/theories/Reals/Rtrigo1.v
+++ b/theories/Reals/Rtrigo1.v
@@ -39,7 +39,7 @@ Proof.
         (fun n:nat =>
           sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k)))
           n) l }.
-  intro X; elim X; intros.
+  intros (x,p).
   exists x.
   split.
   apply p.
diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index b131b5107..cbba91f06 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -20,80 +20,79 @@ Local Open Scope R_scope.
 Lemma Alembert_exp :
   Un_cv (fun n:nat => Rabs (/ INR (fact (S n)) * / / INR (fact n))) 0.
 Proof.
-  unfold Un_cv; intros; elim (Rgt_dec eps 1); intro.
-  split with 0%nat; intros; rewrite (simpl_fact n); unfold R_dist;
-    rewrite (Rminus_0_r (Rabs (/ INR (S n))));
-      rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0).
-  intro; rewrite (Rabs_pos_eq (/ INR (S n))).
-  cut (/ eps - 1 < 0).
-  intro; generalize (Rlt_le_trans (/ eps - 1) 0 (INR n) H2 (pos_INR n));
-    clear H2; intro; unfold Rminus in H2;
-      generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H2);
-        replace (1 + (/ eps + -1)) with (/ eps); [ clear H2; intro | ring ].
-  rewrite (Rplus_comm 1 (INR n)) in H2; rewrite <- (S_INR n) in H2;
-    generalize (Rmult_gt_0_compat (/ INR (S n)) eps H1 H);
-      intro; unfold Rgt in H3;
-        generalize (Rmult_lt_compat_l (/ INR (S n) * eps) (/ eps) (INR (S n)) H3 H2);
-          intro; rewrite (Rmult_assoc (/ INR (S n)) eps (/ eps)) in H4;
-            rewrite (Rinv_r eps (Rlt_dichotomy_converse eps 0 (or_intror (eps < 0) H)))
-              in H4; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H4;
-                rewrite (Rmult_comm (/ INR (S n))) in H4;
-                  rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H4;
-                    rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (not_eq_sym (O_S n)))) in H4;
-                      rewrite (let (H1, H2) := Rmult_ne eps in H1) in H4;
-                        assumption.
-  apply Rlt_minus; unfold Rgt in a; rewrite <- Rinv_1;
-    apply (Rinv_lt_contravar 1 eps); auto;
-      rewrite (let (H1, H2) := Rmult_ne eps in H2); unfold Rgt in H;
-        assumption.
-  unfold Rgt in H1; apply Rlt_le; assumption.
-  unfold Rgt; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn.
-(**)
-  cut (0 <= up (/ eps - 1))%Z.
-  intro; elim (IZN (up (/ eps - 1)) H0); intros; split with x; intros;
-    rewrite (simpl_fact n); unfold R_dist;
+  unfold Un_cv; intros; destruct (Rgt_dec eps 1) as [Hgt|Hnotgt].
+  - split with 0%nat; intros; rewrite (simpl_fact n); unfold R_dist;
       rewrite (Rminus_0_r (Rabs (/ INR (S n))));
         rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0).
-  intro; rewrite (Rabs_pos_eq (/ INR (S n))).
-  cut (/ eps - 1 < INR x).
-  intro ;
-    generalize
-      (Rlt_le_trans (/ eps - 1) (INR x) (INR n) H4
-        (le_INR x n H2));
-      clear H4; intro; unfold Rminus in H4;
-        generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H4);
-          replace (1 + (/ eps + -1)) with (/ eps); [ clear H4; intro | ring ].
-  rewrite (Rplus_comm 1 (INR n)) in H4; rewrite <- (S_INR n) in H4;
-    generalize (Rmult_gt_0_compat (/ INR (S n)) eps H3 H);
-      intro; unfold Rgt in H5;
-        generalize (Rmult_lt_compat_l (/ INR (S n) * eps) (/ eps) (INR (S n)) H5 H4);
-          intro; rewrite (Rmult_assoc (/ INR (S n)) eps (/ eps)) in H6;
-            rewrite (Rinv_r eps (Rlt_dichotomy_converse eps 0 (or_intror (eps < 0) H)))
-              in H6; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H6;
-                rewrite (Rmult_comm (/ INR (S n))) in H6;
-                  rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H6;
-                    rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (not_eq_sym (O_S n)))) in H6;
-                      rewrite (let (H1, H2) := Rmult_ne eps in H1) in H6;
-                        assumption.
-  cut (IZR (up (/ eps - 1)) = IZR (Z.of_nat x));
-    [ intro | rewrite H1; trivial ].
-  elim (archimed (/ eps - 1)); intros; clear H6; unfold Rgt in H5;
-    rewrite H4 in H5; rewrite INR_IZR_INZ; assumption.
-  unfold Rgt in H1; apply Rlt_le; assumption.
-  unfold Rgt; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn.
-  apply (le_O_IZR (up (/ eps - 1)));
-    apply (Rle_trans 0 (/ eps - 1) (IZR (up (/ eps - 1)))).
-  generalize (Rnot_gt_le eps 1 b); clear b; unfold Rle; intro; elim H0;
-    clear H0; intro.
-  left; unfold Rgt in H;
-    generalize (Rmult_lt_compat_l (/ eps) eps 1 (Rinv_0_lt_compat eps H) H0);
-      rewrite
-        (Rinv_l eps
-          (not_eq_sym (Rlt_dichotomy_converse 0 eps (or_introl (0 > eps) H))))
-        ; rewrite (let (H1, H2) := Rmult_ne (/ eps) in H1);
-          intro; fold (/ eps - 1 > 0); apply Rgt_minus;
-            unfold Rgt; assumption.
-  right; rewrite H0; rewrite Rinv_1; symmetry; apply Rminus_diag_eq; auto.
-  elim (archimed (/ eps - 1)); intros; clear H1; unfold Rgt in H0; apply Rlt_le;
-    assumption.
+    intro; rewrite (Rabs_pos_eq (/ INR (S n))).
+    cut (/ eps - 1 < 0).
+    intro H2; generalize (Rlt_le_trans (/ eps - 1) 0 (INR n) H2 (pos_INR n));
+      clear H2; intro; unfold Rminus in H2;
+        generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H2);
+          replace (1 + (/ eps + -1)) with (/ eps); [ clear H2; intro | ring ].
+    rewrite (Rplus_comm 1 (INR n)) in H2; rewrite <- (S_INR n) in H2;
+      generalize (Rmult_gt_0_compat (/ INR (S n)) eps H1 H);
+        intro; unfold Rgt in H3;
+          generalize (Rmult_lt_compat_l (/ INR (S n) * eps) (/ eps) (INR (S n)) H3 H2);
+            intro; rewrite (Rmult_assoc (/ INR (S n)) eps (/ eps)) in H4;
+              rewrite (Rinv_r eps (Rlt_dichotomy_converse eps 0 (or_intror (eps < 0) H)))
+                in H4; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H4;
+                  rewrite (Rmult_comm (/ INR (S n))) in H4;
+                    rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H4;
+                      rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (not_eq_sym (O_S n)))) in H4;
+                        rewrite (let (H1, H2) := Rmult_ne eps in H1) in H4;
+                          assumption.
+    apply Rlt_minus; unfold Rgt in Hgt; rewrite <- Rinv_1;
+      apply (Rinv_lt_contravar 1 eps); auto;
+        rewrite (let (H1, H2) := Rmult_ne eps in H2); unfold Rgt in H;
+          assumption.
+    unfold Rgt in H1; apply Rlt_le; assumption.
+    unfold Rgt; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn.
+  - cut (0 <= up (/ eps - 1))%Z.
+    intro; elim (IZN (up (/ eps - 1)) H0); intros; split with x; intros;
+      rewrite (simpl_fact n); unfold R_dist;
+        rewrite (Rminus_0_r (Rabs (/ INR (S n))));
+          rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0).
+    intro; rewrite (Rabs_pos_eq (/ INR (S n))).
+    cut (/ eps - 1 < INR x).
+    intro ;
+      generalize
+        (Rlt_le_trans (/ eps - 1) (INR x) (INR n) H4
+          (le_INR x n H2));
+        clear H4; intro; unfold Rminus in H4;
+          generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H4);
+            replace (1 + (/ eps + -1)) with (/ eps); [ clear H4; intro | ring ].
+    rewrite (Rplus_comm 1 (INR n)) in H4; rewrite <- (S_INR n) in H4;
+      generalize (Rmult_gt_0_compat (/ INR (S n)) eps H3 H);
+        intro; unfold Rgt in H5;
+          generalize (Rmult_lt_compat_l (/ INR (S n) * eps) (/ eps) (INR (S n)) H5 H4);
+            intro; rewrite (Rmult_assoc (/ INR (S n)) eps (/ eps)) in H6;
+              rewrite (Rinv_r eps (Rlt_dichotomy_converse eps 0 (or_intror (eps < 0) H)))
+                in H6; rewrite (let (H1, H2) := Rmult_ne (/ INR (S n)) in H1) in H6;
+                  rewrite (Rmult_comm (/ INR (S n))) in H6;
+                    rewrite (Rmult_assoc eps (/ INR (S n)) (INR (S n))) in H6;
+                      rewrite (Rinv_l (INR (S n)) (not_O_INR (S n) (not_eq_sym (O_S n)))) in H6;
+                        rewrite (let (H1, H2) := Rmult_ne eps in H1) in H6;
+                          assumption.
+    cut (IZR (up (/ eps - 1)) = IZR (Z.of_nat x));
+      [ intro | rewrite H1; trivial ].
+    elim (archimed (/ eps - 1)); intros; clear H6; unfold Rgt in H5;
+      rewrite H4 in H5; rewrite INR_IZR_INZ; assumption.
+    unfold Rgt in H1; apply Rlt_le; assumption.
+    unfold Rgt; apply Rinv_0_lt_compat; apply lt_INR_0; apply lt_O_Sn.
+    apply (le_O_IZR (up (/ eps - 1)));
+      apply (Rle_trans 0 (/ eps - 1) (IZR (up (/ eps - 1)))).
+    generalize (Rnot_gt_le eps 1 Hnotgt); clear Hnotgt; unfold Rle; intro; elim H0;
+      clear H0; intro.
+    left; unfold Rgt in H;
+      generalize (Rmult_lt_compat_l (/ eps) eps 1 (Rinv_0_lt_compat eps H) H0);
+        rewrite
+          (Rinv_l eps
+            (not_eq_sym (Rlt_dichotomy_converse 0 eps (or_introl (0 > eps) H))))
+          ; rewrite (let (H1, H2) := Rmult_ne (/ eps) in H1);
+            intro; fold (/ eps - 1 > 0); apply Rgt_minus;
+              unfold Rgt; assumption.
+    right; rewrite H0; rewrite Rinv_1; symmetry; apply Rminus_diag_eq; auto.
+    elim (archimed (/ eps - 1)); intros; clear H1; unfold Rgt in H0; apply Rlt_le;
+      assumption.
 Qed.
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index aafa3357e..1394abd2a 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -59,7 +59,7 @@ Proof.
           sum_f_R0
           (fun k:nat => Rabs (/ INR (fact (2 * k + 1)) * r ^ (2 * k))) n)
         l }.
-  intro X; elim X; intros.
+  intros (x,p).
   exists x.
   split.
   apply p.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index d8f1cc6aa..1a5171c9b 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -53,8 +53,7 @@ Proof.
   apply growing_cv.
   apply decreasing_growing; assumption.
   exact H0.
-  intro X.
-  elim X; intros.
+  intros (x,p).
   exists (- x).
   unfold Un_cv in p.
   unfold R_dist in p.
@@ -151,7 +150,7 @@ Definition sequence_lb (Un:nat -> R) (pr:has_lb Un)
 (* Compatibility *)
 Notation sequence_majorant := sequence_ub (only parsing).
 Notation sequence_minorant := sequence_lb (only parsing).
-
+Unset Standard Proposition Elimination Names.
 Lemma Wn_decreasing :
   forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr).
 Proof.
@@ -159,21 +158,15 @@ Proof.
   unfold Un_decreasing.
   intro.
   unfold sequence_ub.
-  assert (H := ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)).
-  assert (H0 := ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)).
-  elim H; intros.
-  elim H0; intros.
+  pose proof (ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) as (x,(H1,H2)).
+  pose proof (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) as (x0,(H3,H4)).
   cut (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr) = x);
     [ intro Maj1; rewrite Maj1 | idtac ].
   cut (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr) = x0);
     [ intro Maj2; rewrite Maj2 | idtac ].
-  unfold is_lub in p.
-  unfold is_lub in p0.
-  elim p; intros.
   apply H2.
-  elim p0; intros.
   unfold is_upper_bound.
-  intros.
+  intros x1 H5.
   unfold is_upper_bound in H3.
   apply H3.
   elim H5; intros.
@@ -184,12 +177,10 @@ Proof.
   cut
     (is_lub (EUn (fun k:nat => Un (n + k)%nat))
       (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr))).
-  intro.
-  unfold is_lub in p0; unfold is_lub in H1.
-  elim p0; intros; elim H1; intros.
-  assert (H6 := H5 x0 H2).
+  intros (H5,H6).
+  assert (H7 := H6 x0 H3).
   assert
-    (H7 := H3 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H4).
+    (H8 := H4 (lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)) H5).
   apply Rle_antisym; assumption.
   unfold lub.
   case (ub_to_lub (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr)).
@@ -197,13 +188,11 @@ Proof.
   cut
     (is_lub (EUn (fun k:nat => Un (S n + k)%nat))
       (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr))).
-  intro.
-  unfold is_lub in p; unfold is_lub in H1.
-  elim p; intros; elim H1; intros.
-  assert (H6 := H5 x H2).
+  intros (H5,H6).
+  assert (H7 := H6 x H1).
   assert
-    (H7 :=
-      H3 (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H4).
+    (H8 :=
+      H2 (lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)) H5).
   apply Rle_antisym; assumption.
   unfold lub.
   case (ub_to_lub (fun k:nat => Un (S n + k)%nat) (maj_ss Un (S n) pr)).
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 462a94db1..fb0c171ad 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -222,39 +222,37 @@ Proof.
   intro; apply Rle_lt_trans with (R_dist (sum_f_R0 Bn n) (sum_f_R0 Bn m)).
   assumption.
   apply H2; assumption.
-  assert (H5 := lt_eq_lt_dec n m).
-  elim H5; intro.
-  elim a; intro.
-  rewrite (tech2 An n m); [ idtac | assumption ].
-  rewrite (tech2 Bn n m); [ idtac | assumption ].
-  unfold R_dist; unfold Rminus; do 2 rewrite Ropp_plus_distr;
-    do 2 rewrite <- Rplus_assoc; do 2 rewrite Rplus_opp_r;
-      do 2 rewrite Rplus_0_l; do 2 rewrite Rabs_Ropp; repeat rewrite Rabs_right.
-  apply sum_Rle; intros.
-  elim (H (S n + n0)%nat); intros.
-  apply H8.
-  apply Rle_ge; apply cond_pos_sum; intro.
-  elim (H (S n + n0)%nat); intros.
-  apply Rle_trans with (An (S n + n0)%nat); assumption.
-  apply Rle_ge; apply cond_pos_sum; intro.
-  elim (H (S n + n0)%nat); intros; assumption.
-  rewrite b; unfold R_dist; unfold Rminus;
+  destruct (lt_eq_lt_dec n m) as [[| -> ]|].
+  - rewrite (tech2 An n m); [ idtac | assumption ].
+    rewrite (tech2 Bn n m); [ idtac | assumption ].
+    unfold R_dist; unfold Rminus; do 2 rewrite Ropp_plus_distr;
+      do 2 rewrite <- Rplus_assoc; do 2 rewrite Rplus_opp_r;
+        do 2 rewrite Rplus_0_l; do 2 rewrite Rabs_Ropp; repeat rewrite Rabs_right.
+    apply sum_Rle; intros.
+    elim (H (S n + n0)%nat); intros.
+    apply H8.
+    apply Rle_ge; apply cond_pos_sum; intro.
+    elim (H (S n + n0)%nat); intros.
+    apply Rle_trans with (An (S n + n0)%nat); assumption.
+    apply Rle_ge; apply cond_pos_sum; intro.
+    elim (H (S n + n0)%nat); intros; assumption.
+  - unfold R_dist; unfold Rminus;
     do 2 rewrite Rplus_opp_r; rewrite Rabs_R0; right;
       reflexivity.
-  rewrite (tech2 An m n); [ idtac | assumption ].
-  rewrite (tech2 Bn m n); [ idtac | assumption ].
-  unfold R_dist; unfold Rminus; do 2 rewrite Rplus_assoc;
-    rewrite (Rplus_comm (sum_f_R0 An m)); rewrite (Rplus_comm (sum_f_R0 Bn m));
-      do 2 rewrite Rplus_assoc; do 2 rewrite Rplus_opp_l;
-        do 2 rewrite Rplus_0_r; repeat rewrite Rabs_right.
-  apply sum_Rle; intros.
-  elim (H (S m + n0)%nat); intros; apply H8.
-  apply Rle_ge; apply cond_pos_sum; intro.
-  elim (H (S m + n0)%nat); intros.
-  apply Rle_trans with (An (S m + n0)%nat); assumption.
-  apply Rle_ge.
-  apply cond_pos_sum; intro.
-  elim (H (S m + n0)%nat); intros; assumption.
+  - rewrite (tech2 An m n); [ idtac | assumption ].
+    rewrite (tech2 Bn m n); [ idtac | assumption ].
+    unfold R_dist; unfold Rminus; do 2 rewrite Rplus_assoc;
+      rewrite (Rplus_comm (sum_f_R0 An m)); rewrite (Rplus_comm (sum_f_R0 Bn m));
+        do 2 rewrite Rplus_assoc; do 2 rewrite Rplus_opp_l;
+          do 2 rewrite Rplus_0_r; repeat rewrite Rabs_right.
+    apply sum_Rle; intros.
+    elim (H (S m + n0)%nat); intros; apply H8.
+    apply Rle_ge; apply cond_pos_sum; intro.
+    elim (H (S m + n0)%nat); intros.
+    apply Rle_trans with (An (S m + n0)%nat); assumption.
+    apply Rle_ge.
+    apply cond_pos_sum; intro.
+    elim (H (S m + n0)%nat); intros; assumption.
 Qed.
 
 (** Cesaro's theorem *)