Nommage explicite de certains "intro" pour préserver la compatibilité

en préparation du passage à des inductifs à polymorphisme de sorte
("sigT R" va devenir de type le type de R, càd Set)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8670 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 253 insertions, 252 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 3a67fff821..188d7ad3ca 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -30,7 +30,7 @@ intros An H H0.
 cut
  (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) ->
   sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)).
-intro; apply X.
+intro X; apply X.
 apply completeness.
 unfold Un_cv in H0; unfold bound in |- *; cut (0 < / 2);
  [ intro | apply Rinv_0_lt_compat; prove_sup0 ].
@@ -107,7 +107,7 @@ red in |- *; intro; assert (H8 := H n); rewrite H7 in H8;
 replace (S x + 0)%nat with (S x); [ reflexivity | ring ].
 symmetry  in |- *; apply tech2; assumption.
 exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity.
-intro; elim X; intros.
+intro X; elim X; intros.
 apply existT with x; apply tech10;
  [ unfold Un_growing in |- *; intro; rewrite tech5;
     pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r;
@@ -418,7 +418,7 @@ intros An k Hyp H H0.
 cut
  (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) ->
   sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)).
-intro; apply X.
+intro X; apply X.
 apply completeness.
 assert (H1 := tech13 _ _ Hyp H0).
 elim H1; intros.
@@ -517,7 +517,7 @@ rewrite H10 in H11; elim (Rlt_irrefl _ H11).
 replace (S x0 + 0)%nat with (S x0); [ reflexivity | ring ].
 symmetry  in |- *; apply tech2; assumption.
 exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity.
-intro; elim X; intros.
+intro X; elim X; intros.
 apply existT with x; apply tech10;
  [ unfold Un_growing in |- *; intro; rewrite tech5;
     pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r;
@@ -559,11 +559,11 @@ rewrite <- Rabs_mult.
 rewrite Rabs_Rabsolu.
 unfold Rdiv in H3; apply H3; assumption.
 apply H0.
-intro.
+intro X.
 elim X; intros.
 apply existT with x.
 assumption.
-intro.
+intro X.
 elim X; intros.
 apply existT with x.
 assumption.
@@ -581,7 +581,7 @@ intros.
 cut
  (sigT
     (fun l:R => Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l)).
-intro.
+intro X.
 elim X; intros.
 apply existT with x0.
 apply tech12; assumption.
@@ -723,4 +723,4 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat.
 assumption.
 apply Rinv_0_lt_compat; apply Rabs_pos_lt.
 red in |- *; intro H7; rewrite H7 in r; elim (Rlt_irrefl _ r).
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index c8fa2b0cf9..b0849be4ac 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -895,7 +895,7 @@ cut
        Un_cv
          (fun n:nat =>
             sum_f_R0 (fun k:nat => Rabs (r ^ k / INR (fact (S k)))) n) l)).
-intro.
+intro X.
 elim X; intros.
 exists x; intros.
 split.
diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v
index bbd18250f4..0b066da34a 100644
--- a/theories/Reals/MVT.v
+++ b/theories/Reals/MVT.v
@@ -27,7 +27,7 @@ Theorem MVT :
 intros; assert (H2 := Rlt_le _ _ H).
 set (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y).
 cut (forall c:R, a < c < b -> derivable_pt h c).
-intro; cut (forall c:R, a <= c <= b -> continuity_pt h c).
+intro X; cut (forall c:R, a <= c <= b -> continuity_pt h c).
 intro; assert (H4 := continuity_ab_maj h a b H2 H3).
 assert (H5 := continuity_ab_min h a b H2 H3).
 elim H4; intros Mx H6.
@@ -142,9 +142,9 @@ Lemma MVT_cor1 :
    a < b ->
     exists c : R, f b - f a = derive_pt f c (pr c) * (b - a) /\ a < c < b.
 intros f a b pr H; cut (forall c:R, a < c < b -> derivable_pt f c);
- [ intro | intros; apply pr ].
+ [ intro X | intros; apply pr ].
 cut (forall c:R, a < c < b -> derivable_pt id c);
- [ intro | intros; apply derivable_pt_id ].
+ [ intro X0 | intros; apply derivable_pt_id ].
 cut (forall c:R, a <= c <= b -> continuity_pt f c);
  [ intro | intros; apply derivable_continuous_pt; apply pr ].
 cut (forall c:R, a <= c <= b -> continuity_pt id c);
@@ -166,11 +166,11 @@ Theorem MVT_cor2 :
    (forall c:R, a <= c <= b -> derivable_pt_lim f c (f' c)) ->
     exists c : R, f b - f a = f' c * (b - a) /\ a < c < b.
 intros f f' a b H H0; cut (forall c:R, a <= c <= b -> derivable_pt f c).
-intro; cut (forall c:R, a < c < b -> derivable_pt f c).
-intro; cut (forall c:R, a <= c <= b -> continuity_pt f c).
+intro X; cut (forall c:R, a < c < b -> derivable_pt f c).
+intro X0; cut (forall c:R, a <= c <= b -> continuity_pt f c).
 intro; cut (forall c:R, a <= c <= b -> derivable_pt id c).
-intro; cut (forall c:R, a < c < b -> derivable_pt id c).
-intro; cut (forall c:R, a <= c <= b -> continuity_pt id c).
+intro X1; cut (forall c:R, a < c < b -> derivable_pt id c).
+intro X2; cut (forall c:R, a <= c <= b -> continuity_pt id c).
 intro; elim (MVT f id a b X0 X2 H H1 H2); intros; elim H3; clear H3; intros;
  exists x; split.
 cut (derive_pt id x (X2 x x0) = 1).
@@ -595,7 +595,7 @@ Lemma IAF_var :
    g b - g a <= f b - f a.
 intros.
 cut (derivable (g - f)).
-intro.
+intro X.
 cut (forall c:R, a <= c <= b -> derive_pt (g - f) c (X c) <= 0).
 intro. 
 assert (H2 := IAF (g - f)%F a b 0 X H H1).
diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v
index 3fa2aece3b..cd2dbc193b 100644
--- a/theories/Reals/NewtonInt.v
+++ b/theories/Reals/NewtonInt.v
@@ -128,7 +128,8 @@ Lemma NewtonInt_P5 :
    Newton_integrable f a b ->
    Newton_integrable g a b ->
    Newton_integrable (fun x:R => l * f x + g x) a b.
-unfold Newton_integrable in |- *; intros; elim X; intros; elim X0; intros;
+unfold Newton_integrable in |- *; intros f g l a b X X0;
+ elim X; intros; elim X0; intros;
  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 3e121ecf68..9fe077a4ed 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -430,7 +430,7 @@ Lemma cv_cauchy_1 :
  forall An:nat -> R,
    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l) ->
    Cauchy_crit_series An.
-intros.
+intros An X.
 elim X; intros.
 unfold Un_cv in p.
 unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *.
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index fce508f18e..5751f843c9 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -453,7 +453,7 @@ Qed.
 
 Theorem derivable_continuous_pt :
  forall f (x:R), derivable_pt f x -> continuity_pt f x.
-intros.
+intros f x X.
 generalize (derivable_derive f x X); intro.
 elim H; intros l H1.
 cut (l = fct_cte l x).
@@ -468,7 +468,7 @@ unfold fct_cte in |- *; reflexivity.
 Qed.
 
 Theorem derivable_continuous : forall f, derivable f -> continuity f.
-unfold derivable, continuity in |- *; intros.
+unfold derivable, continuity in |- *; intros f X x.
 apply (derivable_continuous_pt f x (X x)).
 Qed.
 
@@ -661,7 +661,7 @@ Qed.
 Lemma derivable_pt_plus :
  forall f1 f2 (x:R),
    derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 + f2) x.
-unfold derivable_pt in |- *; intros.
+unfold derivable_pt in |- *; intros f1 f2 x X X0.
 elim X; intros.
 elim X0; intros.
 apply existT with (x0 + x1).
@@ -670,7 +670,7 @@ Qed.
 
 Lemma derivable_pt_opp :
  forall f (x:R), derivable_pt f x -> derivable_pt (- f) x.
-unfold derivable_pt in |- *; intros.
+unfold derivable_pt in |- *; intros f x X.
 elim X; intros.
 apply existT with (- x0).
 apply derivable_pt_lim_opp; assumption.
@@ -679,7 +679,7 @@ Qed.
 Lemma derivable_pt_minus :
  forall f1 f2 (x:R),
    derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 - f2) x.
-unfold derivable_pt in |- *; intros.
+unfold derivable_pt in |- *; intros f1 f2 x X X0.
 elim X; intros.
 elim X0; intros.
 apply existT with (x0 - x1).
@@ -689,7 +689,7 @@ Qed.
 Lemma derivable_pt_mult :
  forall f1 f2 (x:R),
    derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 * f2) x.
-unfold derivable_pt in |- *; intros.
+unfold derivable_pt in |- *; intros f1 f2 x X X0.
 elim X; intros.
 elim X0; intros.
 apply existT with (x0 * f2 x + f1 x * x1).
@@ -704,7 +704,7 @@ Qed.
 
 Lemma derivable_pt_scal :
  forall f (a x:R), derivable_pt f x -> derivable_pt (mult_real_fct a f) x.
-unfold derivable_pt in |- *; intros.
+unfold derivable_pt in |- *; intros f1 a x X.
 elim X; intros.
 apply existT with (a * x0).
 apply derivable_pt_lim_scal; assumption.
@@ -724,7 +724,7 @@ Qed.
 Lemma derivable_pt_comp :
  forall f1 f2 (x:R),
    derivable_pt f1 x -> derivable_pt f2 (f1 x) -> derivable_pt (f2 o f1) x.
-unfold derivable_pt in |- *; intros.
+unfold derivable_pt in |- *; intros f1 f2 x X X0.
 elim X; intros.
 elim X0; intros.
 apply existT with (x1 * x0).
@@ -733,24 +733,24 @@ Qed.
 
 Lemma derivable_plus :
  forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 + f2).
-unfold derivable in |- *; intros.
+unfold derivable in |- *; intros f1 f2 X X0 x.
 apply (derivable_pt_plus _ _ x (X _) (X0 _)).
 Qed.
 
 Lemma derivable_opp : forall f, derivable f -> derivable (- f).
-unfold derivable in |- *; intros.
+unfold derivable in |- *; intros f X x.
 apply (derivable_pt_opp _ x (X _)).
 Qed.
 
 Lemma derivable_minus :
  forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 - f2).
-unfold derivable in |- *; intros.
+unfold derivable in |- *; intros f1 f2 X X0 x.
 apply (derivable_pt_minus _ _ x (X _) (X0 _)).
 Qed.
 
 Lemma derivable_mult :
  forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 * f2).
-unfold derivable in |- *; intros.
+unfold derivable in |- *; intros f1 f2 X X0 x.
 apply (derivable_pt_mult _ _ x (X _) (X0 _)).
 Qed.
 
@@ -761,7 +761,7 @@ Qed.
 
 Lemma derivable_scal :
  forall f (a:R), derivable f -> derivable (mult_real_fct a f).
-unfold derivable in |- *; intros.
+unfold derivable in |- *; intros f a X x.
 apply (derivable_pt_scal _ a x (X _)).
 Qed.
 
@@ -775,7 +775,7 @@ Qed.
 
 Lemma derivable_comp :
  forall f1 f2, derivable f1 -> derivable f2 -> derivable (f2 o f1).
-unfold derivable in |- *; intros.
+unfold derivable in |- *; intros f1 f2 X X0 x.
 apply (derivable_pt_comp _ _ x (X _) (X0 _)).
 Qed.
 
diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index 9bcde49fda..7728effff4 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -20,9 +20,9 @@ Theorem derivable_pt_lim_div :
    derivable_pt_lim f2 x l2 ->
    f2 x <> 0 ->
    derivable_pt_lim (f1 / f2) x ((l1 * f2 x - l2 * f1 x) / Rsqr (f2 x)).
-intros.
+intros f1 f2 x l1 l2 H H0 H1.
 cut (derivable_pt f2 x);
- [ intro | unfold derivable_pt in |- *; apply existT with l2; exact H0 ].
+ [ intro X | unfold derivable_pt in |- *; apply existT with l2; exact H0 ].
 assert (H2 := continuous_neq_0 _ _ (derivable_continuous_pt _ _ X) H1).
 elim H2; clear H2; intros eps_f2 H2.
 unfold div_fct in |- *.
@@ -756,7 +756,7 @@ Lemma derivable_pt_div :
    derivable_pt f1 x ->
    derivable_pt f2 x -> f2 x <> 0 -> derivable_pt (f1 / f2) x.
 unfold derivable_pt in |- *.
-intros.
+intros f1 f2 x X X0 H.
 elim X; intros.
 elim X0; intros.
 apply existT with ((x0 * f2 x - x1 * f1 x) / Rsqr (f2 x)).
@@ -767,7 +767,7 @@ Lemma derivable_div :
  forall f1 f2:R -> R,
    derivable f1 ->
    derivable f2 -> (forall x:R, f2 x <> 0) -> derivable (f1 / f2).
-unfold derivable in |- *; intros.
+unfold derivable in |- *; intros f1 f2 X X0 H x.
 apply (derivable_pt_div _ _ _ (X x) (X0 x) (H x)).
 Qed.
 
@@ -790,4 +790,4 @@ unfold derive_pt in H; rewrite H in H3.
 assert (H4 := projT2 pr2).
 unfold derive_pt in H0; rewrite H0 in H4.
 apply derivable_pt_lim_div; assumption.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index 16f79fd1e9..0aeb5e1b77 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -20,13 +20,13 @@ Require Import Exp_prop. Open Local Scope R_scope.
 Lemma derivable_pt_inv :
  forall (f:R -> R) (x:R),
    f x <> 0 -> derivable_pt f x -> derivable_pt (/ f) x.
-intros; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x).
-intro; apply X0.
+intros f x H X; cut (derivable_pt (fct_cte 1 / f) x -> derivable_pt (/ f) x).
+intro X0; apply X0.
 apply derivable_pt_div.
 apply derivable_pt_const.
 assumption.
 assumption.
-unfold div_fct, inv_fct, fct_cte in |- *; intro; elim X0; intros;
+unfold div_fct, inv_fct, fct_cte in |- *; intro X0; elim X0; intros;
  unfold derivable_pt in |- *; apply existT with x0;
  unfold derivable_pt_abs in |- *; unfold derivable_pt_lim in |- *;
  unfold derivable_pt_abs in p; unfold derivable_pt_lim in p; 
@@ -76,8 +76,8 @@ Qed.
 (**********)
 Lemma derivable_inv :
  forall f:R -> R, (forall x:R, f x <> 0) -> derivable f -> derivable (/ f).
-intros.
-unfold derivable in |- *; intro.
+intros f H X.
+unfold derivable in |- *; intro x.
 apply derivable_pt_inv.
 apply (H x).
 apply (X x).
@@ -381,4 +381,4 @@ Lemma derive_pt_sinh :
  forall x:R, derive_pt sinh x (derivable_pt_sinh x) = cosh x.
 intro; apply derive_pt_eq_0.
 apply derivable_pt_lim_sinh.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index df750b9c68..629a2f003a 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -455,7 +455,7 @@ 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.
+intros X X0.
 elim X; intros.
 elim X0; intros.
 assert (H4 := cv_dicho _ _ _ _ _ H3 p0 p).
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 0fb8ee3875..d9e96b9c5d 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -32,7 +32,7 @@ cut
          (fun n:nat =>
             sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k)))
               n) l)).
-intro; elim X; intros.
+intro X; elim X; intros.
 apply existT with x.
 split.
 apply p.
@@ -206,7 +206,7 @@ cut
             sum_f_R0
               (fun k:nat => Rabs (/ INR (fact (2 * k + 1)) * r ^ (2 * k))) n)
          l)).
-intro; elim X; intros.
+intro X; elim X; intros.
 apply existT with x.
 split.
 apply p.
@@ -605,4 +605,4 @@ Lemma derive_pt_cos :
  forall x:R, derive_pt cos x (derivable_pt_cos _) = - sin x.
 intros; apply derive_pt_eq_0.
 apply derivable_pt_lim_cos.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 14ca8a1e98..484e0f2173 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
- 
+
 (*i $Id$ i*)
 
 Require Import Rbase.
@@ -48,7 +48,7 @@ cut (~ (forall N:nat, Un N <= x - eps)).
 intro H6; apply (not_all_not_ex nat (fun N:nat => x - eps < Un N)).
  intro H7; apply H6; intro N; apply Rnot_lt_le; apply H7.
 intro H7; generalize (Un_bound_imp Un (x - eps) H7); intro H8;
- unfold is_upper_bound in H8; generalize (H3 (x - eps) H8); 
+ unfold is_upper_bound in H8; generalize (H3 (x - eps) H8);
  apply Rlt_not_le; apply tech_Rgt_minus; exact H1.
 Qed.
 
@@ -66,12 +66,12 @@ Lemma decreasing_cv :
    Un_decreasing Un -> has_lb Un -> sigT (fun l:R => Un_cv Un l).
 intros.
 cut (sigT (fun l:R => Un_cv (opp_seq Un) l) -> sigT (fun l:R => Un_cv Un l)).
-intro.
+intro X.
 apply X.
 apply growing_cv.
 apply decreasing_growing; assumption.
 exact H0.
-intro.
+intro X.
 elim X; intros.
 apply existT with (- x).
 unfold Un_cv in p.
@@ -155,14 +155,14 @@ elim H1; intros.
 exists (k + x1)%nat; assumption.
 Qed.
 
-Definition sequence_majorant (Un:nat -> R) (pr:has_ub Un) 
+Definition sequence_majorant (Un:nat -> R) (pr:has_ub Un)
   (i:nat) : R := majorant (fun k:nat => Un (i + k)%nat) (maj_ss Un i pr).
 
-Definition sequence_minorant (Un:nat -> R) (pr:has_lb Un) 
+Definition sequence_minorant (Un:nat -> R) (pr:has_lb Un)
   (i:nat) : R := minorant (fun k:nat => Un (i + k)%nat) (min_ss Un i pr).
 
 Lemma Wn_decreasing :
- forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_majorant Un pr). 
+ forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_majorant Un pr).
 intros.
 unfold Un_decreasing in |- *.
 intro.
@@ -289,14 +289,14 @@ Qed.
 
 (**********)
 Lemma Vn_Un_Wn_order :
- forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un) 
-   (n:nat), sequence_minorant Un pr2 n <= Un n <= sequence_majorant Un pr1 n. 
+ forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un)
+   (n:nat), sequence_minorant Un pr2 n <= Un n <= sequence_majorant Un pr1 n.
 intros.
 split.
 unfold sequence_minorant in |- *.
 cut
  (sigT (fun l:R => is_lub (EUn (opp_seq (fun i:nat => Un (n + i)%nat))) l)).
-intro.
+intro X.
 elim X; intros.
 replace (minorant (fun k:nat => Un (n + k)%nat) (min_ss Un n pr2)) with (- x).
 unfold is_lub in p.
@@ -329,7 +329,7 @@ apply min_inf.
 apply min_ss; assumption.
 unfold sequence_majorant in |- *.
 cut (sigT (fun l:R => is_lub (EUn (fun i:nat => Un (n + i)%nat)) l)).
-intro.
+intro X.
 elim X; intros.
 replace (majorant (fun k:nat => Un (n + k)%nat) (maj_ss Un n pr1)) with x.
 unfold is_lub in p.
@@ -379,7 +379,7 @@ Qed.
 
 Lemma maj_min :
  forall (Un:nat -> R) (pr1:has_ub Un) (pr2:has_lb Un),
-   has_lb (sequence_majorant Un pr1). 
+   has_lb (sequence_majorant Un pr1).
 intros.
 assert (H := Vn_Un_Wn_order Un pr1 pr2).
 unfold has_lb in |- *.
@@ -486,7 +486,7 @@ Qed.
 Lemma not_Rlt : forall r1 r2:R, ~ r1 < r2 -> r1 >= r2.
 intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rge in |- *.
 tauto.
-Qed. 
+Qed.
 
 (**********)
 Lemma approx_maj :
@@ -628,234 +628,234 @@ assert (H2 := H1 n).
 apply not_Rlt; assumption.
 Qed.
 
-(* Unicity of limit for convergent sequences *) 
+(* Unicity of limit for convergent sequences *)
 Lemma UL_sequence :
- forall (Un:nat -> R) (l1 l2:R), Un_cv Un l1 -> Un_cv Un l2 -> l1 = l2. 
-intros Un l1 l2; unfold Un_cv in |- *; unfold R_dist in |- *; intros. 
-apply cond_eq. 
+ forall (Un:nat -> R) (l1 l2:R), Un_cv Un l1 -> Un_cv Un l2 -> l1 = l2.
+intros Un l1 l2; unfold Un_cv in |- *; unfold R_dist in |- *; intros.
+apply cond_eq.
 intros; cut (0 < eps / 2);
  [ intro
  | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
-    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. 
-elim (H (eps / 2) H2); intros. 
-elim (H0 (eps / 2) H2); intros. 
-set (N := max x x0). 
-apply Rle_lt_trans with (Rabs (l1 - Un N) + Rabs (Un N - l2)). 
+    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
+elim (H (eps / 2) H2); intros.
+elim (H0 (eps / 2) H2); intros.
+set (N := max x x0).
+apply Rle_lt_trans with (Rabs (l1 - Un N) + Rabs (Un N - l2)).
 replace (l1 - l2) with (l1 - Un N + (Un N - l2));
- [ apply Rabs_triang | ring ]. 
-rewrite (double_var eps); apply Rplus_lt_compat. 
+ [ apply Rabs_triang | ring ].
+rewrite (double_var eps); apply Rplus_lt_compat.
 rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H3;
- unfold ge, N in |- *; apply le_max_l. 
-apply H4; unfold ge, N in |- *; apply le_max_r. 
+ unfold ge, N in |- *; apply le_max_l.
+apply H4; unfold ge, N in |- *; apply le_max_r.
 Qed.
 
-(**********) 
+(**********)
 Lemma CV_plus :
  forall (An Bn:nat -> R) (l1 l2:R),
-   Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i + Bn i) (l1 + l2). 
-unfold Un_cv in |- *; unfold R_dist in |- *; intros. 
+   Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i + Bn i) (l1 + l2).
+unfold Un_cv in |- *; unfold R_dist in |- *; intros.
 cut (0 < eps / 2);
  [ intro
  | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
-    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. 
-elim (H (eps / 2) H2); intros. 
-elim (H0 (eps / 2) H2); intros. 
-set (N := max x x0). 
-exists N; intros. 
+    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
+elim (H (eps / 2) H2); intros.
+elim (H0 (eps / 2) H2); intros.
+set (N := max x x0).
+exists N; intros.
 replace (An n + Bn n - (l1 + l2)) with (An n - l1 + (Bn n - l2));
- [ idtac | ring ]. 
-apply Rle_lt_trans with (Rabs (An n - l1) + Rabs (Bn n - l2)). 
-apply Rabs_triang. 
-rewrite (double_var eps); apply Rplus_lt_compat. 
+ [ idtac | ring ].
+apply Rle_lt_trans with (Rabs (An n - l1) + Rabs (Bn n - l2)).
+apply Rabs_triang.
+rewrite (double_var eps); apply Rplus_lt_compat.
 apply H3; unfold ge in |- *; apply le_trans with N;
- [ unfold N in |- *; apply le_max_l | assumption ]. 
+ [ unfold N in |- *; apply le_max_l | assumption ].
 apply H4; unfold ge in |- *; apply le_trans with N;
- [ unfold N in |- *; apply le_max_r | assumption ]. 
+ [ unfold N in |- *; apply le_max_r | assumption ].
 Qed.
 
-(**********) 
+(**********)
 Lemma cv_cvabs :
  forall (Un:nat -> R) (l:R),
-   Un_cv Un l -> Un_cv (fun i:nat => Rabs (Un i)) (Rabs l). 
-unfold Un_cv in |- *; unfold R_dist in |- *; intros. 
-elim (H eps H0); intros. 
-exists x; intros. 
-apply Rle_lt_trans with (Rabs (Un n - l)). 
-apply Rabs_triang_inv2. 
-apply H1; assumption. 
-Qed. 
+   Un_cv Un l -> Un_cv (fun i:nat => Rabs (Un i)) (Rabs l).
+unfold Un_cv in |- *; unfold R_dist in |- *; intros.
+elim (H eps H0); intros.
+exists x; intros.
+apply Rle_lt_trans with (Rabs (Un n - l)).
+apply Rabs_triang_inv2.
+apply H1; assumption.
+Qed.
 
-(**********) 
+(**********)
 Lemma CV_Cauchy :
- forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> Cauchy_crit Un. 
-intros; elim X; intros. 
-unfold Cauchy_crit in |- *; intros. 
-unfold Un_cv in p; unfold R_dist in p. 
+ forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> Cauchy_crit Un.
+intros Un X; elim X; intros.
+unfold Cauchy_crit in |- *; intros.
+unfold Un_cv in p; unfold R_dist in p.
 cut (0 < eps / 2);
  [ intro
  | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
-    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. 
-elim (p (eps / 2) H0); intros. 
-exists x0; intros. 
+    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ].
+elim (p (eps / 2) H0); intros.
+exists x0; intros.
 unfold R_dist in |- *;
- apply Rle_lt_trans with (Rabs (Un n - x) + Rabs (x - Un m)). 
+ apply Rle_lt_trans with (Rabs (Un n - x) + Rabs (x - Un m)).
 replace (Un n - Un m) with (Un n - x + (x - Un m));
- [ apply Rabs_triang | ring ]. 
-rewrite (double_var eps); apply Rplus_lt_compat. 
-apply H1; assumption. 
-rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1; assumption. 
-Qed. 
+ [ apply Rabs_triang | ring ].
+rewrite (double_var eps); apply Rplus_lt_compat.
+apply H1; assumption.
+rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H1; assumption.
+Qed.
 
 (**********)
 Lemma maj_by_pos :
  forall Un:nat -> R,
    sigT (fun l:R => Un_cv Un l) ->
-    exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l). 
-intros; elim X; intros. 
-cut (sigT (fun l:R => Un_cv (fun k:nat => Rabs (Un k)) l)). 
-intro. 
-assert (H := CV_Cauchy (fun k:nat => Rabs (Un k)) X0). 
-assert (H0 := cauchy_bound (fun k:nat => Rabs (Un k)) H). 
-elim H0; intros. 
-exists (x0 + 1). 
-cut (0 <= x0). 
-intro. 
-split. 
-apply Rplus_le_lt_0_compat; [ assumption | apply Rlt_0_1 ]. 
-intros. 
-apply Rle_trans with x0. 
-unfold is_upper_bound in H1. 
-apply H1. 
-exists n; reflexivity. 
+    exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l).
+intros Un X; elim X; intros.
+cut (sigT (fun l:R => Un_cv (fun k:nat => Rabs (Un k)) l)).
+intro X0.
+assert (H := CV_Cauchy (fun k:nat => Rabs (Un k)) X0).
+assert (H0 := cauchy_bound (fun k:nat => Rabs (Un k)) H).
+elim H0; intros.
+exists (x0 + 1).
+cut (0 <= x0).
+intro.
+split.
+apply Rplus_le_lt_0_compat; [ assumption | apply Rlt_0_1 ].
+intros.
+apply Rle_trans with x0.
+unfold is_upper_bound in H1.
+apply H1.
+exists n; reflexivity.
 pattern x0 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
- apply Rlt_0_1. 
-apply Rle_trans with (Rabs (Un 0%nat)). 
-apply Rabs_pos. 
-unfold is_upper_bound in H1. 
-apply H1. 
-exists 0%nat; reflexivity. 
-apply existT with (Rabs x). 
-apply cv_cvabs; assumption. 
-Qed. 
- 
-(**********) 
+ apply Rlt_0_1.
+apply Rle_trans with (Rabs (Un 0%nat)).
+apply Rabs_pos.
+unfold is_upper_bound in H1.
+apply H1.
+exists 0%nat; reflexivity.
+apply existT with (Rabs x).
+apply cv_cvabs; assumption.
+Qed.
+
+(**********)
 Lemma CV_mult :
  forall (An Bn:nat -> R) (l1 l2:R),
-   Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i * Bn i) (l1 * l2). 
-intros. 
-cut (sigT (fun l:R => Un_cv An l)). 
-intro. 
-assert (H1 := maj_by_pos An X). 
-elim H1; intros M H2. 
-elim H2; intros. 
-unfold Un_cv in |- *; unfold R_dist in |- *; intros. 
-cut (0 < eps / (2 * M)). 
-intro. 
-case (Req_dec l2 0); intro. 
-unfold Un_cv in H0; unfold R_dist in H0. 
-elim (H0 (eps / (2 * M)) H6); intros. 
-exists x; intros. 
+   Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i * Bn i) (l1 * l2).
+intros.
+cut (sigT (fun l:R => Un_cv An l)).
+intro X.
+assert (H1 := maj_by_pos An X).
+elim H1; intros M H2.
+elim H2; intros.
+unfold Un_cv in |- *; unfold R_dist in |- *; intros.
+cut (0 < eps / (2 * M)).
+intro.
+case (Req_dec l2 0); intro.
+unfold Un_cv in H0; unfold R_dist in H0.
+elim (H0 (eps / (2 * M)) H6); intros.
+exists x; intros.
 apply Rle_lt_trans with
- (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). 
+ (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)).
 replace (An n * Bn n - l1 * l2) with
  (An n * Bn n - An n * l2 + (An n * l2 - l1 * l2));
- [ apply Rabs_triang | ring ]. 
+ [ apply Rabs_triang | ring ].
 replace (Rabs (An n * Bn n - An n * l2)) with
- (Rabs (An n) * Rabs (Bn n - l2)). 
-replace (Rabs (An n * l2 - l1 * l2)) with 0. 
-rewrite Rplus_0_r. 
-apply Rle_lt_trans with (M * Rabs (Bn n - l2)). 
-do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). 
-apply Rmult_le_compat_l. 
-apply Rabs_pos. 
-apply H4. 
-apply Rmult_lt_reg_l with (/ M). 
-apply Rinv_0_lt_compat; apply H3. 
-rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. 
-rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). 
-apply Rlt_trans with (eps / (2 * M)). 
-apply H8; assumption. 
-unfold Rdiv in |- *; rewrite Rinv_mult_distr. 
-apply Rmult_lt_reg_l with 2. 
+ (Rabs (An n) * Rabs (Bn n - l2)).
+replace (Rabs (An n * l2 - l1 * l2)) with 0.
+rewrite Rplus_0_r.
+apply Rle_lt_trans with (M * Rabs (Bn n - l2)).
+do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))).
+apply Rmult_le_compat_l.
+apply Rabs_pos.
+apply H4.
+apply Rmult_lt_reg_l with (/ M).
+apply Rinv_0_lt_compat; apply H3.
+rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
+rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)).
+apply Rlt_trans with (eps / (2 * M)).
+apply H8; assumption.
+unfold Rdiv in |- *; rewrite Rinv_mult_distr.
+apply Rmult_lt_reg_l with 2.
 prove_sup0.
 replace (2 * (eps * (/ 2 * / M))) with (2 * / 2 * (eps * / M));
- [ idtac | ring ]. 
-rewrite <- Rinv_r_sym. 
-rewrite Rmult_1_l; rewrite double. 
-pattern (eps * / M) at 1 in |- *; rewrite <- Rplus_0_r. 
+ [ idtac | ring ].
+rewrite <- Rinv_r_sym.
+rewrite Rmult_1_l; rewrite double.
+pattern (eps * / M) at 1 in |- *; rewrite <- Rplus_0_r.
 apply Rplus_lt_compat_l; apply Rmult_lt_0_compat;
- [ assumption | apply Rinv_0_lt_compat; assumption ]. 
-discrR. 
-discrR. 
-red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). 
-red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3). 
+ [ assumption | apply Rinv_0_lt_compat; assumption ].
+discrR.
+discrR.
+red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3).
+red in |- *; intro; rewrite H10 in H3; elim (Rlt_irrefl _ H3).
 rewrite H7; do 2 rewrite Rmult_0_r; unfold Rminus in |- *;
- rewrite Rplus_opp_r; rewrite Rabs_R0; reflexivity. 
-replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2)); [ idtac | ring ]. 
-symmetry  in |- *; apply Rabs_mult. 
-cut (0 < eps / (2 * Rabs l2)). 
-intro. 
+ rewrite Rplus_opp_r; rewrite Rabs_R0; reflexivity.
+replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2)); [ idtac | ring ].
+symmetry  in |- *; apply Rabs_mult.
+cut (0 < eps / (2 * Rabs l2)).
+intro.
 unfold Un_cv in H; unfold R_dist in H; unfold Un_cv in H0;
- unfold R_dist in H0. 
-elim (H (eps / (2 * Rabs l2)) H8); intros N1 H9. 
-elim (H0 (eps / (2 * M)) H6); intros N2 H10. 
-set (N := max N1 N2). 
-exists N; intros. 
+ unfold R_dist in H0.
+elim (H (eps / (2 * Rabs l2)) H8); intros N1 H9.
+elim (H0 (eps / (2 * M)) H6); intros N2 H10.
+set (N := max N1 N2).
+exists N; intros.
 apply Rle_lt_trans with
- (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)). 
+ (Rabs (An n * Bn n - An n * l2) + Rabs (An n * l2 - l1 * l2)).
 replace (An n * Bn n - l1 * l2) with
  (An n * Bn n - An n * l2 + (An n * l2 - l1 * l2));
- [ apply Rabs_triang | ring ]. 
+ [ apply Rabs_triang | ring ].
 replace (Rabs (An n * Bn n - An n * l2)) with
- (Rabs (An n) * Rabs (Bn n - l2)). 
-replace (Rabs (An n * l2 - l1 * l2)) with (Rabs l2 * Rabs (An n - l1)). 
-rewrite (double_var eps); apply Rplus_lt_compat. 
-apply Rle_lt_trans with (M * Rabs (Bn n - l2)). 
-do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))). 
-apply Rmult_le_compat_l. 
-apply Rabs_pos. 
-apply H4. 
-apply Rmult_lt_reg_l with (/ M). 
-apply Rinv_0_lt_compat; apply H3. 
-rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. 
-rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)). 
-apply Rlt_le_trans with (eps / (2 * M)). 
-apply H10. 
-unfold ge in |- *; apply le_trans with N. 
-unfold N in |- *; apply le_max_r. 
-assumption. 
-unfold Rdiv in |- *; rewrite Rinv_mult_distr. 
-right; ring. 
-discrR. 
-red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). 
-red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3). 
-apply Rmult_lt_reg_l with (/ Rabs l2). 
-apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. 
-rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. 
-rewrite Rmult_1_l; apply Rlt_le_trans with (eps / (2 * Rabs l2)). 
-apply H9. 
-unfold ge in |- *; apply le_trans with N. 
-unfold N in |- *; apply le_max_l. 
-assumption. 
-unfold Rdiv in |- *; right; rewrite Rinv_mult_distr. 
-ring. 
-discrR. 
-apply Rabs_no_R0; assumption. 
-apply Rabs_no_R0; assumption. 
+ (Rabs (An n) * Rabs (Bn n - l2)).
+replace (Rabs (An n * l2 - l1 * l2)) with (Rabs l2 * Rabs (An n - l1)).
+rewrite (double_var eps); apply Rplus_lt_compat.
+apply Rle_lt_trans with (M * Rabs (Bn n - l2)).
+do 2 rewrite <- (Rmult_comm (Rabs (Bn n - l2))).
+apply Rmult_le_compat_l.
+apply Rabs_pos.
+apply H4.
+apply Rmult_lt_reg_l with (/ M).
+apply Rinv_0_lt_compat; apply H3.
+rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
+rewrite Rmult_1_l; rewrite (Rmult_comm (/ M)).
+apply Rlt_le_trans with (eps / (2 * M)).
+apply H10.
+unfold ge in |- *; apply le_trans with N.
+unfold N in |- *; apply le_max_r.
+assumption.
+unfold Rdiv in |- *; rewrite Rinv_mult_distr.
+right; ring.
+discrR.
+red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3).
+red in |- *; intro; rewrite H12 in H3; elim (Rlt_irrefl _ H3).
+apply Rmult_lt_reg_l with (/ Rabs l2).
+apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption.
+rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym.
+rewrite Rmult_1_l; apply Rlt_le_trans with (eps / (2 * Rabs l2)).
+apply H9.
+unfold ge in |- *; apply le_trans with N.
+unfold N in |- *; apply le_max_l.
+assumption.
+unfold Rdiv in |- *; right; rewrite Rinv_mult_distr.
+ring.
+discrR.
+apply Rabs_no_R0; assumption.
+apply Rabs_no_R0; assumption.
 replace (An n * l2 - l1 * l2) with (l2 * (An n - l1));
- [ symmetry  in |- *; apply Rabs_mult | ring ]. 
+ [ symmetry  in |- *; apply Rabs_mult | ring ].
 replace (An n * Bn n - An n * l2) with (An n * (Bn n - l2));
- [ symmetry  in |- *; apply Rabs_mult | ring ]. 
-unfold Rdiv in |- *; apply Rmult_lt_0_compat. 
-assumption. 
+ [ symmetry  in |- *; apply Rabs_mult | ring ].
+unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+assumption.
 apply Rinv_0_lt_compat; apply Rmult_lt_0_compat;
- [ prove_sup0 | apply Rabs_pos_lt; assumption ]. 
+ [ prove_sup0 | apply Rabs_pos_lt; assumption ].
 unfold Rdiv in |- *; apply Rmult_lt_0_compat;
  [ assumption
  | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat;
-    [ prove_sup0 | assumption ] ]. 
-apply existT with l1; assumption. 
-Qed. 
+    [ prove_sup0 | assumption ] ].
+apply existT with l1; assumption.
+Qed.
 
 Lemma tech9 :
  forall Un:nat -> R,
@@ -905,13 +905,13 @@ rewrite b; assumption.
 cut (forall n:nat, Un n <= x0).
 intro; unfold is_lub in H0; unfold is_upper_bound in H0; elim H0; intros.
 cut (forall y:R, EUn Un y -> y <= x0).
-intro; assert (H8 := H6 _ H7). 
+intro; assert (H8 := H6 _ H7).
 elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H8 r)).
 unfold EUn in |- *; intros; elim H7; intros.
 rewrite H8; apply H4.
 intro; case (Rle_dec (Un n) x0); intro.
 assumption.
-cut (forall n0:nat, (n <= n0)%nat -> x0 < Un n0). 
+cut (forall n0:nat, (n <= n0)%nat -> x0 < Un n0).
 intro; unfold Un_cv in H3; cut (0 < Un n - x0).
 intro; elim (H3 (Un n - x0) H5); intros.
 cut (max n x1 >= x1)%nat.
@@ -931,7 +931,7 @@ left; assumption.
 unfold ge in |- *; apply le_max_r.
 apply Rplus_lt_reg_r with x0.
 rewrite Rplus_0_r; unfold Rminus in |- *; rewrite (Rplus_comm x0);
- rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; 
+ rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
  apply H4; apply le_n.
 intros; apply Rlt_le_trans with (Un n).
 case (Rlt_le_dec x0 (Un n)); intro.
@@ -977,7 +977,7 @@ unfold R_dist in H4; rewrite <- Rabs_Rabsolu;
 apply Rabs_triang.
 rewrite (Rabs_right k).
 apply Rplus_lt_reg_r with (- k); rewrite <- (Rplus_comm k);
- repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l; 
+ repeat rewrite <- Rplus_assoc; rewrite Rplus_opp_l;
  repeat rewrite Rplus_0_l; apply H4.
 apply Rle_ge; elim H; intros; assumption.
 unfold Rdiv in |- *; apply Rmult_lt_0_compat.
@@ -989,7 +989,7 @@ Qed.
 (**********)
 Lemma growing_ineq :
  forall (Un:nat -> R) (l:R),
-   Un_growing Un -> Un_cv Un l -> forall n:nat, Un n <= l. 
+   Un_growing Un -> Un_cv Un l -> forall n:nat, Un n <= l.
 intros; case (total_order_T (Un n) l); intro.
 elim s; intro.
 left; assumption.
@@ -1042,14 +1042,14 @@ Qed.
 (**********)
 Lemma CV_minus :
  forall (An Bn:nat -> R) (l1 l2:R),
-   Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i - Bn i) (l1 - l2). 
-intros. 
-replace (fun i:nat => An i - Bn i) with (fun i:nat => An i + opp_seq Bn i). 
-unfold Rminus in |- *; apply CV_plus. 
-assumption. 
-apply CV_opp; assumption. 
-unfold Rminus, opp_seq in |- *; reflexivity. 
-Qed. 
+   Un_cv An l1 -> Un_cv Bn l2 -> Un_cv (fun i:nat => An i - Bn i) (l1 - l2).
+intros.
+replace (fun i:nat => An i - Bn i) with (fun i:nat => An i + opp_seq Bn i).
+unfold Rminus in |- *; apply CV_plus.
+assumption.
+apply CV_opp; assumption.
+unfold Rminus, opp_seq in |- *; reflexivity.
+Qed.
 
 (* Un -> +oo *)
 Definition cv_infty (Un:nat -> R) : Prop :=
@@ -1265,7 +1265,7 @@ apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;
  assert (H8 := sym_eq H7); elim (fact_neq_0 _ H8).
 clear Un Vn; apply INR_le; simpl in |- *.
 induction  M_nat as [| M_nat HrecM_nat].
-assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros. 
+assert (H6 := archimed (Rabs x)); fold M in H6; elim H6; intros.
 rewrite H4 in H7; rewrite <- INR_IZR_INZ in H7.
 simpl in H7; elim (Rlt_irrefl _ (Rlt_trans _ _ _ H2 H7)).
 replace 1 with (INR 1); [ apply le_INR | reflexivity ]; apply le_n_S;
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 7a02b689df..f3762bd7ba 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -36,12 +36,12 @@ intros;
   (sigT
      (fun l:R =>
         Un_cv (fun n:nat => sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) l)).
-intro;
+intro X;
  cut
   (sigT
      (fun l:R =>
         Un_cv (fun n:nat => sum_f_R0 (fun l:nat => An (S N + l)%nat) n) l)).
-intro; elim X; intros l1N H2.
+intro X0; elim X; intros l1N H2.
 elim X0; intros l2N H3.
 cut (l1 - SP fn N x = l1N).
 intro; cut (l2 - sum_f_R0 An N = l2N).
@@ -217,7 +217,7 @@ Lemma Rseries_CV_comp :
    (forall n:nat, 0 <= An n <= Bn n) ->
    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 Bn N) l) ->
    sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l).
-intros; apply cv_cauchy_2.
+intros An Bn H X; apply cv_cauchy_2.
 assert (H0 := cv_cauchy_1 _ X).
 unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *.
 intros; elim (H0 eps H1); intros.