Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

1 files changed, 523 insertions, 396 deletions

diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 090680cf1..c12aea9df 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -8,469 +8,596 @@
  
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
-Require Rseries.
-Require Rcomplete.
-Require Max.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import Rseries.
+Require Import Rcomplete.
+Require Import Max.
 Open Local Scope R_scope.
 
-Lemma tech1 : (An:nat->R;N:nat) ((n:nat)``(le n N)``->``0<(An n)``) -> ``0 < (sum_f_R0 An N)``.
-Intros; Induction N.
-Simpl; Apply H; Apply le_n.
-Simpl; Apply gt0_plus_gt0_is_gt0.
-Apply HrecN; Intros; Apply H; Apply le_S; Assumption.
-Apply H; Apply le_n.
+Lemma tech1 :
+ forall (An:nat -> R) (N:nat),
+   (forall n:nat, (n <= N)%nat -> 0 < An n) -> 0 < sum_f_R0 An N.
+intros; induction  N as [| N HrecN].
+simpl in |- *; apply H; apply le_n.
+simpl in |- *; apply Rplus_lt_0_compat.
+apply HrecN; intros; apply H; apply le_S; assumption.
+apply H; apply le_n.
 Qed.
 
 (* Chasles' relation *)
-Lemma tech2 : (An:nat->R;m,n:nat) (lt m n) -> (sum_f_R0 An n) == (Rplus (sum_f_R0 An m) (sum_f_R0 [i:nat]``(An (plus (S m) i))`` (minus n (S m)))). 
-Intros; Induction n.
-Elim (lt_n_O ? H).
-Cut (lt m n)\/m=n.
-Intro; Elim H0; Intro.
-Replace (sum_f_R0 An (S n)) with ``(sum_f_R0 An n)+(An (S n))``; [Idtac | Reflexivity].
-Replace (minus (S n) (S m)) with (S (minus n (S m))).
-Replace (sum_f_R0 [i:nat](An (plus (S m) i)) (S (minus n (S m)))) with (Rplus (sum_f_R0 [i:nat](An (plus (S m) i)) (minus n (S m))) (An (plus (S m) (S (minus n (S m)))))); [Idtac | Reflexivity].
-Replace (plus (S m) (S (minus n (S m)))) with (S n).
-Rewrite (Hrecn H1).
-Ring.
-Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Do 2 Rewrite S_INR; Rewrite minus_INR.
-Rewrite S_INR; Ring.
-Apply lt_le_S; Assumption.
-Apply INR_eq; Rewrite S_INR; Repeat Rewrite minus_INR.
-Repeat Rewrite S_INR; Ring.
-Apply le_n_S; Apply lt_le_weak; Assumption.
-Apply lt_le_S; Assumption.
-Rewrite H1; Rewrite <- minus_n_n; Simpl.
-Replace (plus n O) with n; [Reflexivity | Ring].
-Inversion H.
-Right; Reflexivity.
-Left; Apply lt_le_trans with (S m); [Apply lt_n_Sn | Assumption].
+Lemma tech2 :
+ forall (An:nat -> R) (m n:nat),
+   (m < n)%nat ->
+   sum_f_R0 An n =
+   sum_f_R0 An m + sum_f_R0 (fun i:nat => An (S m + i)%nat) (n - S m). 
+intros; induction  n as [| n Hrecn].
+elim (lt_n_O _ H).
+cut ((m < n)%nat \/ m = n).
+intro; elim H0; intro.
+replace (sum_f_R0 An (S n)) with (sum_f_R0 An n + An (S n));
+ [ idtac | reflexivity ].
+replace (S n - S m)%nat with (S (n - S m)).
+replace (sum_f_R0 (fun i:nat => An (S m + i)%nat) (S (n - S m))) with
+ (sum_f_R0 (fun i:nat => An (S m + i)%nat) (n - S m) +
+  An (S m + S (n - S m))%nat); [ idtac | reflexivity ].
+replace (S m + S (n - S m))%nat with (S n).
+rewrite (Hrecn H1).
+ring.
+apply INR_eq; rewrite S_INR; rewrite plus_INR; do 2 rewrite S_INR;
+ rewrite minus_INR.
+rewrite S_INR; ring.
+apply lt_le_S; assumption.
+apply INR_eq; rewrite S_INR; repeat rewrite minus_INR.
+repeat rewrite S_INR; ring.
+apply le_n_S; apply lt_le_weak; assumption.
+apply lt_le_S; assumption.
+rewrite H1; rewrite <- minus_n_n; simpl in |- *.
+replace (n + 0)%nat with n; [ reflexivity | ring ].
+inversion H.
+right; reflexivity.
+left; apply lt_le_trans with (S m); [ apply lt_n_Sn | assumption ].
 Qed.
 
 (* Sum of geometric sequences *)
-Lemma tech3 : (k:R;N:nat) ``k<>1`` -> (sum_f_R0 [i:nat](pow k i) N)==``(1-(pow k (S N)))/(1-k)``.
-Intros; Cut ``1-k<>0``.
-Intro; Induction N.
-Simpl; Rewrite Rmult_1r; Unfold Rdiv; Rewrite <- Rinv_r_sym.
-Reflexivity.
-Apply H0.
-Replace (sum_f_R0 ([i:nat](pow k i)) (S N)) with (Rplus (sum_f_R0 [i:nat](pow k i) N) (pow k (S N))); [Idtac | Reflexivity]; Rewrite HrecN; Replace ``(1-(pow k (S N)))/(1-k)+(pow k (S N))`` with ``((1-(pow k (S N)))+(1-k)*(pow k (S N)))/(1-k)``.
-Apply r_Rmult_mult with ``1-k``.
-Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(1-k)``); Repeat Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [ Do 2 Rewrite Rmult_1l; Simpl; Ring | Apply H0].
-Apply H0.
-Unfold Rdiv; Rewrite Rmult_Rplus_distrl; Rewrite (Rmult_sym ``1-k``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1r; Reflexivity.
-Apply H0.
-Apply Rminus_eq_contra; Red; Intro; Elim H; Symmetry; Assumption.
+Lemma tech3 :
+ forall (k:R) (N:nat),
+   k <> 1 -> sum_f_R0 (fun i:nat => k ^ i) N = (1 - k ^ S N) / (1 - k).
+intros; cut (1 - k <> 0).
+intro; induction  N as [| N HrecN].
+simpl in |- *; rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rinv_r_sym.
+reflexivity.
+apply H0.
+replace (sum_f_R0 (fun i:nat => k ^ i) (S N)) with
+ (sum_f_R0 (fun i:nat => k ^ i) N + k ^ S N); [ idtac | reflexivity ];
+ rewrite HrecN;
+ replace ((1 - k ^ S N) / (1 - k) + k ^ S N) with
+  ((1 - k ^ S N + (1 - k) * k ^ S N) / (1 - k)).
+apply Rmult_eq_reg_l with (1 - k).
+unfold Rdiv in |- *; do 2 rewrite <- (Rmult_comm (/ (1 - k)));
+ repeat rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym;
+ [ do 2 rewrite Rmult_1_l; simpl in |- *; ring | apply H0 ].
+apply H0.
+unfold Rdiv in |- *; rewrite Rmult_plus_distr_r; rewrite (Rmult_comm (1 - k));
+ repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
+rewrite Rmult_1_r; reflexivity.
+apply H0.
+apply Rminus_eq_contra; red in |- *; intro; elim H; symmetry  in |- *;
+ assumption.
 Qed.
 
-Lemma tech4 : (An:nat->R;k:R;N:nat) ``0<=k`` -> ((i:nat)``(An (S i))<k*(An i)``) -> ``(An N)<=(An O)*(pow k N)``.
-Intros; Induction N.
-Simpl; Right; Ring.
-Apply Rle_trans with ``k*(An N)``.
-Left; Apply (H0 N).
-Replace (S N) with (plus N (1)); [Idtac | Ring].
-Rewrite pow_add; Simpl; Rewrite Rmult_1r; Replace ``(An O)*((pow k N)*k)`` with ``k*((An O)*(pow k N))``; [Idtac | Ring]; Apply Rle_monotony.
-Assumption.
-Apply HrecN.
+Lemma tech4 :
+ forall (An:nat -> R) (k:R) (N:nat),
+   0 <= k -> (forall i:nat, An (S i) < k * An i) -> An N <= An 0%nat * k ^ N.
+intros; induction  N as [| N HrecN].
+simpl in |- *; right; ring.
+apply Rle_trans with (k * An N).
+left; apply (H0 N).
+replace (S N) with (N + 1)%nat; [ idtac | ring ].
+rewrite pow_add; simpl in |- *; rewrite Rmult_1_r;
+ replace (An 0%nat * (k ^ N * k)) with (k * (An 0%nat * k ^ N));
+ [ idtac | ring ]; apply Rmult_le_compat_l.
+assumption.
+apply HrecN.
 Qed.
 
-Lemma tech5 : (An:nat->R;N:nat) (sum_f_R0 An (S N))==``(sum_f_R0 An N)+(An (S N))``.
-Intros; Reflexivity.
+Lemma tech5 :
+ forall (An:nat -> R) (N:nat), sum_f_R0 An (S N) = sum_f_R0 An N + An (S N).
+intros; reflexivity.
 Qed.
 
-Lemma tech6 : (An:nat->R;k:R;N:nat) ``0<=k`` -> ((i:nat)``(An (S i))<k*(An i)``) -> (Rle (sum_f_R0 An N) (Rmult (An O) (sum_f_R0 [i:nat](pow k i) N))).
-Intros; Induction N.
-Simpl; Right; Ring.
-Apply Rle_trans with (Rplus (Rmult (An O) (sum_f_R0 [i:nat](pow k i) N)) (An (S N))).
-Rewrite tech5; Do 2 Rewrite <- (Rplus_sym (An (S N))); Apply Rle_compatibility.
-Apply HrecN.
-Rewrite tech5 ; Rewrite Rmult_Rplus_distr; Apply Rle_compatibility.
-Apply tech4; Assumption.
+Lemma tech6 :
+ forall (An:nat -> R) (k:R) (N:nat),
+   0 <= k ->
+   (forall i:nat, An (S i) < k * An i) ->
+   sum_f_R0 An N <= An 0%nat * sum_f_R0 (fun i:nat => k ^ i) N.
+intros; induction  N as [| N HrecN].
+simpl in |- *; right; ring.
+apply Rle_trans with (An 0%nat * sum_f_R0 (fun i:nat => k ^ i) N + An (S N)).
+rewrite tech5; do 2 rewrite <- (Rplus_comm (An (S N)));
+ apply Rplus_le_compat_l.
+apply HrecN.
+rewrite tech5; rewrite Rmult_plus_distr_l; apply Rplus_le_compat_l.
+apply tech4; assumption.
 Qed.
 
-Lemma tech7 : (r1,r2:R) ``r1<>0`` -> ``r2<>0`` -> ``r1<>r2`` -> ``/r1<>/r2``.
-Intros; Red; Intro.
-Assert H3 := (Rmult_mult_r r1 ? ? H2).
-Rewrite <- Rinv_r_sym in H3; [Idtac | Assumption].
-Assert H4 := (Rmult_mult_r r2 ? ? H3).
-Rewrite Rmult_1r in H4; Rewrite <- Rmult_assoc in H4.
-Rewrite Rinv_r_simpl_m in H4; [Idtac | Assumption].
-Elim H1; Symmetry; Assumption.
+Lemma tech7 : forall r1 r2:R, r1 <> 0 -> r2 <> 0 -> r1 <> r2 -> / r1 <> / r2.
+intros; red in |- *; intro.
+assert (H3 := Rmult_eq_compat_l r1 _ _ H2).
+rewrite <- Rinv_r_sym in H3; [ idtac | assumption ].
+assert (H4 := Rmult_eq_compat_l r2 _ _ H3).
+rewrite Rmult_1_r in H4; rewrite <- Rmult_assoc in H4.
+rewrite Rinv_r_simpl_m in H4; [ idtac | assumption ].
+elim H1; symmetry  in |- *; assumption.
 Qed.
 
-Lemma tech11 : (An,Bn,Cn:nat->R;N:nat) ((i:nat) (An i)==``(Bn i)-(Cn i)``) -> (sum_f_R0 An N)==``(sum_f_R0 Bn N)-(sum_f_R0 Cn N)``.
-Intros; Induction N.
-Simpl; Apply H.
-Do 3 Rewrite tech5; Rewrite HrecN; Rewrite (H (S N)); Ring.
+Lemma tech11 :
+ forall (An Bn Cn:nat -> R) (N:nat),
+   (forall i:nat, An i = Bn i - Cn i) ->
+   sum_f_R0 An N = sum_f_R0 Bn N - sum_f_R0 Cn N.
+intros; induction  N as [| N HrecN].
+simpl in |- *; apply H.
+do 3 rewrite tech5; rewrite HrecN; rewrite (H (S N)); ring.
 Qed.
 
-Lemma tech12 : (An:nat->R;x:R;l:R) (Un_cv [N:nat](sum_f_R0 [i:nat]``(An i)*(pow x i)`` N) l) -> (Pser An x l).
-Intros; Unfold Pser; Unfold infinit_sum; Unfold Un_cv in H; Assumption.
+Lemma tech12 :
+ forall (An:nat -> R) (x l:R),
+   Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l ->
+   Pser An x l.
+intros; unfold Pser in |- *; unfold infinit_sum in |- *; unfold Un_cv in H;
+ assumption.
 Qed. 
 
-Lemma scal_sum : (An:nat->R;N:nat;x:R) (Rmult x (sum_f_R0 An N))==(sum_f_R0 [i:nat]``(An i)*x`` N).
-Intros; Induction N.
-Simpl; Ring.
-Do 2 Rewrite tech5.
-Rewrite Rmult_Rplus_distr; Rewrite <- HrecN; Ring.
+Lemma scal_sum :
+ forall (An:nat -> R) (N:nat) (x:R),
+   x * sum_f_R0 An N = sum_f_R0 (fun i:nat => An i * x) N.
+intros; induction  N as [| N HrecN].
+simpl in |- *; ring.
+do 2 rewrite tech5.
+rewrite Rmult_plus_distr_l; rewrite <- HrecN; ring.
 Qed.
 
-Lemma decomp_sum : (An:nat->R;N:nat) (lt O N) -> (sum_f_R0 An N)==(Rplus (An O) (sum_f_R0 [i:nat](An (S i)) (pred N))).
-Intros; Induction N.
-Elim (lt_n_n ? H).
-Cut (lt O N)\/N=O.
-Intro; Elim H0; Intro.
-Cut (S (pred N))=(pred (S N)).
-Intro; Rewrite <- H2.
-Do 2 Rewrite tech5.
-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.
-Simpl; Reflexivity.
-Rewrite <- b in H1; Elim (lt_n_n ? H1).
-Rewrite H1; Simpl; Reflexivity.
-Inversion H.
-Right; Reflexivity.
-Left; Apply lt_le_trans with (1); [Apply lt_O_Sn | Assumption].
+Lemma decomp_sum :
+ forall (An:nat -> R) (N:nat),
+   (0 < N)%nat ->
+   sum_f_R0 An N = An 0%nat + sum_f_R0 (fun i:nat => An (S i)) (pred N).
+intros; induction  N as [| N HrecN].
+elim (lt_irrefl _ H).
+cut ((0 < N)%nat \/ N = 0%nat).
+intro; elim H0; intro.
+cut (S (pred N) = pred (S N)).
+intro; rewrite <- H2.
+do 2 rewrite tech5.
+replace (S (S (pred N))) with (S N).
+rewrite (HrecN H1); ring.
+rewrite H2; simpl in |- *; reflexivity.
+assert (H2 := O_or_S N).
+elim H2; intros.
+elim a; intros.
+rewrite <- p.
+simpl in |- *; reflexivity.
+rewrite <- b in H1; elim (lt_irrefl _ H1).
+rewrite H1; simpl in |- *; reflexivity.
+inversion H.
+right; reflexivity.
+left; apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ].
 Qed.
 
-Lemma plus_sum : (An,Bn:nat->R;N:nat) (sum_f_R0 [i:nat]``(An i)+(Bn i)`` N)==``(sum_f_R0 An N)+(sum_f_R0 Bn N)``.
-Intros; Induction N.
-Simpl; Ring.
-Do 3 Rewrite tech5; Rewrite HrecN; Ring.
+Lemma plus_sum :
+ forall (An Bn:nat -> R) (N:nat),
+   sum_f_R0 (fun i:nat => An i + Bn i) N = sum_f_R0 An N + sum_f_R0 Bn N.
+intros; induction  N as [| N HrecN].
+simpl in |- *; ring.
+do 3 rewrite tech5; rewrite HrecN; ring.
 Qed.
 
-Lemma sum_eq : (An,Bn:nat->R;N:nat) ((i:nat)(le i N)->(An i)==(Bn i)) -> (sum_f_R0 An N)==(sum_f_R0 Bn N).
-Intros; Induction N.
-Simpl; Apply H; Apply le_n.
-Do 2 Rewrite tech5; Rewrite HrecN.
-Rewrite (H (S N)); [Reflexivity | Apply le_n].
-Intros; Apply H; Apply le_trans with N; [Assumption | Apply le_n_Sn].
+Lemma sum_eq :
+ forall (An Bn:nat -> R) (N:nat),
+   (forall i:nat, (i <= N)%nat -> An i = Bn i) ->
+   sum_f_R0 An N = sum_f_R0 Bn N.
+intros; induction  N as [| N HrecN].
+simpl in |- *; apply H; apply le_n.
+do 2 rewrite tech5; rewrite HrecN.
+rewrite (H (S N)); [ reflexivity | apply le_n ].
+intros; apply H; apply le_trans with N; [ assumption | apply le_n_Sn ].
 Qed.
 
 (* Unicity of the limit defined by convergent series *)
-Lemma unicity_sum : (An:nat->R;l1,l2:R) (infinit_sum An l1) -> (infinit_sum An l2) -> l1 == l2.
-Unfold infinit_sum; Intros.
-Case (Req_EM l1 l2); Intro.
-Assumption.
-Cut ``0<(Rabsolu ((l1-l2)/2))``; [Intro | Apply Rabsolu_pos_lt].
-Elim (H ``(Rabsolu ((l1-l2)/2))`` H2); Intros.
-Elim (H0 ``(Rabsolu ((l1-l2)/2))`` H2); Intros.
-Pose N := (max x0 x); Cut (ge N x0).
-Cut (ge N x).
-Intros; Assert H7 := (H3 N H5); Assert H8 := (H4 N H6).
-Cut ``(Rabsolu (l1-l2)) <= (R_dist (sum_f_R0 An N) l1) + (R_dist (sum_f_R0 An N) l2)``.
-Intro; Assert H10 := (Rplus_lt ? ? ? ? H7 H8); Assert H11 := (Rle_lt_trans ? ? ? H9 H10); Unfold Rdiv in H11; Rewrite Rabsolu_mult in H11.
-Cut ``(Rabsolu (/2))==/2``.
-Intro; Rewrite H12 in H11; Assert H13 := double_var; Unfold Rdiv in H13; Rewrite <- H13 in H11.
-Elim (Rlt_antirefl ? H11).
-Apply Rabsolu_right; Left; Change ``0</2``; Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H20; Generalize (lt_INR_0 (2) (neq_O_lt (2) H20)); Unfold INR; Intro; Assumption | Discriminate].
-Unfold R_dist; Rewrite <- (Rabsolu_Ropp ``(sum_f_R0 An N)-l1``); Rewrite Ropp_distr3.
-Replace ``l1-l2`` with ``((l1-(sum_f_R0 An N)))+((sum_f_R0 An N)-l2)``; [Idtac | Ring].
-Apply Rabsolu_triang.
-Unfold ge; Unfold N; Apply le_max_r.
-Unfold ge; Unfold N; Apply le_max_l.
-Unfold Rdiv; Apply prod_neq_R0.
-Apply Rminus_eq_contra; Assumption.
-Apply Rinv_neq_R0; DiscrR.
+Lemma uniqueness_sum :
+ forall (An:nat -> R) (l1 l2:R),
+   infinit_sum An l1 -> infinit_sum An l2 -> l1 = l2.
+unfold infinit_sum in |- *; intros.
+case (Req_dec l1 l2); intro.
+assumption.
+cut (0 < Rabs ((l1 - l2) / 2)); [ intro | apply Rabs_pos_lt ].
+elim (H (Rabs ((l1 - l2) / 2)) H2); intros.
+elim (H0 (Rabs ((l1 - l2) / 2)) H2); intros.
+pose (N := max x0 x); cut (N >= x0)%nat.
+cut (N >= x)%nat.
+intros; assert (H7 := H3 N H5); assert (H8 := H4 N H6).
+cut (Rabs (l1 - l2) <= R_dist (sum_f_R0 An N) l1 + R_dist (sum_f_R0 An N) l2).
+intro; assert (H10 := Rplus_lt_compat _ _ _ _ H7 H8);
+ assert (H11 := Rle_lt_trans _ _ _ H9 H10); unfold Rdiv in H11;
+ rewrite Rabs_mult in H11.
+cut (Rabs (/ 2) = / 2).
+intro; rewrite H12 in H11; assert (H13 := double_var); unfold Rdiv in H13;
+ rewrite <- H13 in H11.
+elim (Rlt_irrefl _ H11).
+apply Rabs_right; left; change (0 < / 2) in |- *; apply Rinv_0_lt_compat;
+ cut (0%nat <> 2%nat);
+ [ intro H20; generalize (lt_INR_0 2 (neq_O_lt 2 H20)); unfold INR in |- *;
+    intro; assumption
+ | discriminate ].
+unfold R_dist in |- *; rewrite <- (Rabs_Ropp (sum_f_R0 An N - l1));
+ rewrite Ropp_minus_distr'.
+replace (l1 - l2) with (l1 - sum_f_R0 An N + (sum_f_R0 An N - l2));
+ [ idtac | ring ].
+apply Rabs_triang.
+unfold ge in |- *; unfold N in |- *; apply le_max_r.
+unfold ge in |- *; unfold N in |- *; apply le_max_l.
+unfold Rdiv in |- *; apply prod_neq_R0.
+apply Rminus_eq_contra; assumption.
+apply Rinv_neq_0_compat; discrR.
 Qed.
 
-Lemma minus_sum : (An,Bn:nat->R;N:nat) (sum_f_R0 [i:nat]``(An i)-(Bn i)`` N)==``(sum_f_R0 An N)-(sum_f_R0 Bn N)``. 
-Intros; Induction N. 
-Simpl; Ring. 
-Do 3 Rewrite tech5; Rewrite HrecN; Ring. 
+Lemma minus_sum :
+ forall (An Bn:nat -> R) (N:nat),
+   sum_f_R0 (fun i:nat => An i - Bn i) N = sum_f_R0 An N - sum_f_R0 Bn N. 
+intros; induction  N as [| N HrecN]. 
+simpl in |- *; ring. 
+do 3 rewrite tech5; rewrite HrecN; ring. 
 Qed. 
 
-Lemma sum_decomposition : (An:nat->R;N:nat) (Rplus (sum_f_R0 [l:nat](An (mult (2) l)) (S N)) (sum_f_R0 [l:nat](An (S (mult (2) l))) N))==(sum_f_R0 An (mult (2) (S N))).
-Intros.
-Induction N.
-Simpl; Ring.
-Rewrite tech5.
-Rewrite (tech5 [l:nat](An (S (mult (2) l))) N).
-Replace (mult (2) (S (S N))) with (S (S (mult (2) (S N)))).
-Rewrite (tech5 An (S (mult (2) (S N)))).
-Rewrite (tech5 An (mult (2) (S N))).
-Rewrite <- HrecN.
-Ring.
-Apply INR_eq; Do 2 Rewrite S_INR; Do 2 Rewrite mult_INR;Repeat Rewrite S_INR.
-Ring.
+Lemma sum_decomposition :
+ forall (An:nat -> R) (N:nat),
+   sum_f_R0 (fun l:nat => An (2 * l)%nat) (S N) +
+   sum_f_R0 (fun l:nat => An (S (2 * l))) N = sum_f_R0 An (2 * S N).
+intros.
+induction  N as [| N HrecN].
+simpl in |- *; ring.
+rewrite tech5.
+rewrite (tech5 (fun l:nat => An (S (2 * l))) N).
+replace (2 * S (S N))%nat with (S (S (2 * S N))).
+rewrite (tech5 An (S (2 * S N))).
+rewrite (tech5 An (2 * S N)).
+rewrite <- HrecN.
+ring.
+apply INR_eq; do 2 rewrite S_INR; do 2 rewrite mult_INR; repeat rewrite S_INR.
+ring.
 Qed.
 
-Lemma sum_Rle : (An,Bn:nat->R;N:nat) ((n:nat)(le n N)->``(An n)<=(Bn n)``) -> ``(sum_f_R0 An N)<=(sum_f_R0 Bn N)``.
-Intros.
-Induction N.
-Simpl; Apply H.
-Apply le_n.
-Do 2 Rewrite tech5.
-Apply Rle_trans with ``(sum_f_R0 An N)+(Bn (S N))``.
-Apply Rle_compatibility.
-Apply H.
-Apply le_n.
-Do 2 Rewrite <- (Rplus_sym ``(Bn (S N))``).
-Apply Rle_compatibility.
-Apply HrecN.
-Intros; Apply H.
-Apply le_trans with N; [Assumption | Apply le_n_Sn].
+Lemma sum_Rle :
+ forall (An Bn:nat -> R) (N:nat),
+   (forall n:nat, (n <= N)%nat -> An n <= Bn n) ->
+   sum_f_R0 An N <= sum_f_R0 Bn N.
+intros.
+induction  N as [| N HrecN].
+simpl in |- *; apply H.
+apply le_n.
+do 2 rewrite tech5.
+apply Rle_trans with (sum_f_R0 An N + Bn (S N)).
+apply Rplus_le_compat_l.
+apply H.
+apply le_n.
+do 2 rewrite <- (Rplus_comm (Bn (S N))).
+apply Rplus_le_compat_l.
+apply HrecN.
+intros; apply H.
+apply le_trans with N; [ assumption | apply le_n_Sn ].
 Qed.
 
-Lemma sum_Rabsolu : (An:nat->R;N:nat) (Rle (Rabsolu (sum_f_R0 An N)) (sum_f_R0 [l:nat](Rabsolu (An l)) N)).
-Intros.
-Induction N.
-Simpl.
-Right; Reflexivity.
-Do 2 Rewrite tech5.
-Apply Rle_trans with ``(Rabsolu (sum_f_R0 An N))+(Rabsolu (An (S N)))``.
-Apply Rabsolu_triang.
-Do 2 Rewrite <- (Rplus_sym (Rabsolu (An (S N)))).
-Apply Rle_compatibility.
-Apply HrecN.
+Lemma Rsum_abs :
+ forall (An:nat -> R) (N:nat),
+   Rabs (sum_f_R0 An N) <= sum_f_R0 (fun l:nat => Rabs (An l)) N.
+intros.
+induction  N as [| N HrecN].
+simpl in |- *.
+right; reflexivity.
+do 2 rewrite tech5.
+apply Rle_trans with (Rabs (sum_f_R0 An N) + Rabs (An (S N))).
+apply Rabs_triang.
+do 2 rewrite <- (Rplus_comm (Rabs (An (S N)))).
+apply Rplus_le_compat_l.
+apply HrecN.
 Qed.
 
-Lemma sum_cte : (x:R;N:nat) (sum_f_R0 [_:nat]x N) == ``x*(INR (S N))``.
-Intros.
-Induction N.
-Simpl; Ring.
-Rewrite tech5.
-Rewrite HrecN; Repeat Rewrite S_INR; Ring.
+Lemma sum_cte :
+ forall (x:R) (N:nat), sum_f_R0 (fun _:nat => x) N = x * INR (S N).
+intros.
+induction  N as [| N HrecN].
+simpl in |- *; ring.
+rewrite tech5.
+rewrite HrecN; repeat rewrite S_INR; ring.
 Qed.
 
 (**********)
-Lemma sum_growing : (An,Bn:nat->R;N:nat) ((n:nat)``(An n)<=(Bn n)``)->``(sum_f_R0 An N)<=(sum_f_R0 Bn N)``.
-Intros.
-Induction N.
-Simpl; Apply H.
-Do 2 Rewrite tech5.
-Apply Rle_trans with ``(sum_f_R0 An N)+(Bn (S N))``.
-Apply Rle_compatibility; Apply H.
-Do 2 Rewrite <- (Rplus_sym (Bn (S N))).
-Apply Rle_compatibility; Apply HrecN.
+Lemma sum_growing :
+ forall (An Bn:nat -> R) (N:nat),
+   (forall n:nat, An n <= Bn n) -> sum_f_R0 An N <= sum_f_R0 Bn N.
+intros.
+induction  N as [| N HrecN].
+simpl in |- *; apply H.
+do 2 rewrite tech5.
+apply Rle_trans with (sum_f_R0 An N + Bn (S N)).
+apply Rplus_le_compat_l; apply H.
+do 2 rewrite <- (Rplus_comm (Bn (S N))).
+apply Rplus_le_compat_l; apply HrecN.
 Qed.
 
 (**********)
-Lemma Rabsolu_triang_gen : (An:nat->R;N:nat) (Rle (Rabsolu (sum_f_R0 An N)) (sum_f_R0 [i:nat](Rabsolu (An i)) N)). 
-Intros.
-Induction N.
-Simpl.
-Right; Reflexivity.
-Do 2 Rewrite tech5.
-Apply Rle_trans with ``(Rabsolu ((sum_f_R0 An N)))+(Rabsolu (An (S N)))``.
-Apply Rabsolu_triang.
-Do 2 Rewrite <- (Rplus_sym (Rabsolu (An (S N)))).
-Apply Rle_compatibility; Apply HrecN.
+Lemma Rabs_triang_gen :
+ forall (An:nat -> R) (N:nat),
+   Rabs (sum_f_R0 An N) <= sum_f_R0 (fun i:nat => Rabs (An i)) N. 
+intros.
+induction  N as [| N HrecN].
+simpl in |- *.
+right; reflexivity.
+do 2 rewrite tech5.
+apply Rle_trans with (Rabs (sum_f_R0 An N) + Rabs (An (S N))).
+apply Rabs_triang.
+do 2 rewrite <- (Rplus_comm (Rabs (An (S N)))).
+apply Rplus_le_compat_l; apply HrecN.
 Qed.
 
 (**********)
-Lemma cond_pos_sum : (An:nat->R;N:nat) ((n:nat)``0<=(An n)``) -> ``0<=(sum_f_R0 An N)``.
-Intros.
-Induction N.
-Simpl; Apply H.
-Rewrite tech5.
-Apply ge0_plus_ge0_is_ge0.
-Apply HrecN.
-Apply H.
+Lemma cond_pos_sum :
+ forall (An:nat -> R) (N:nat),
+   (forall n:nat, 0 <= An n) -> 0 <= sum_f_R0 An N.
+intros.
+induction  N as [| N HrecN].
+simpl in |- *; apply H.
+rewrite tech5.
+apply Rplus_le_le_0_compat.
+apply HrecN.
+apply H.
 Qed.
 
 (* Cauchy's criterion for series *)
-Definition Cauchy_crit_series [An:nat->R] : Prop := (Cauchy_crit [N:nat](sum_f_R0 An N)).
+Definition Cauchy_crit_series (An:nat -> R) : Prop :=
+  Cauchy_crit (fun N:nat => sum_f_R0 An N).
 
 (* If (|An|) satisfies the Cauchy's criterion for series, then (An) too *)
-Lemma cauchy_abs : (An:nat->R) (Cauchy_crit_series [i:nat](Rabsolu (An i))) -> (Cauchy_crit_series An).
-Unfold Cauchy_crit_series; Unfold Cauchy_crit.
-Intros.
-Elim (H eps H0); Intros.
-Exists x.
-Intros.
-Cut (Rle (R_dist (sum_f_R0 An n) (sum_f_R0 An m)) (R_dist (sum_f_R0 [i:nat](Rabsolu (An i)) n) (sum_f_R0 [i:nat](Rabsolu (An i)) m))).
-Intro.
-Apply Rle_lt_trans with (R_dist (sum_f_R0 [i:nat](Rabsolu (An i)) n) (sum_f_R0 [i:nat](Rabsolu (An i)) m)).
-Assumption.
-Apply H1; Assumption.
-Assert H4 := (lt_eq_lt_dec n m).
-Elim H4; Intro.
-Elim a; Intro.
-Rewrite (tech2 An n m); [Idtac | Assumption].
-Rewrite (tech2 [i:nat](Rabsolu (An i)) n m); [Idtac | Assumption].
-Unfold R_dist.
-Unfold Rminus.
-Do 2 Rewrite Ropp_distr1.
-Do 2 Rewrite <- Rplus_assoc.
-Do 2 Rewrite Rplus_Ropp_r.
-Do 2 Rewrite Rplus_Ol.
-Do 2 Rewrite Rabsolu_Ropp.
-Rewrite (Rabsolu_right (sum_f_R0 [i:nat](Rabsolu (An (plus (S n) i))) (minus m (S n)))).
-Pose Bn:=[i:nat](An (plus (S n) i)).
-Replace [i:nat](Rabsolu (An (plus (S n) i))) with [i:nat](Rabsolu (Bn i)).
-Apply Rabsolu_triang_gen.
-Unfold Bn; Reflexivity.
-Apply Rle_sym1.
-Apply cond_pos_sum.
-Intro; Apply Rabsolu_pos.
-Rewrite b.
-Unfold R_dist.
-Unfold Rminus; Do 2 Rewrite Rplus_Ropp_r.
-Rewrite Rabsolu_R0; Right; Reflexivity.
-Rewrite (tech2 An m n); [Idtac | Assumption].
-Rewrite (tech2 [i:nat](Rabsolu (An i)) m n); [Idtac | Assumption].
-Unfold R_dist.
-Unfold Rminus.
-Do 2 Rewrite Rplus_assoc.
-Rewrite (Rplus_sym (sum_f_R0 An m)).
-Rewrite (Rplus_sym (sum_f_R0 [i:nat](Rabsolu (An i)) m)).
-Do 2 Rewrite Rplus_assoc.
-Do 2 Rewrite Rplus_Ropp_l.
-Do 2 Rewrite Rplus_Or.
-Rewrite (Rabsolu_right (sum_f_R0 [i:nat](Rabsolu (An (plus (S m) i))) (minus n (S m)))).
-Pose Bn:=[i:nat](An (plus (S m) i)).
-Replace [i:nat](Rabsolu (An (plus (S m) i))) with [i:nat](Rabsolu (Bn i)).
-Apply Rabsolu_triang_gen.
-Unfold Bn; Reflexivity.
-Apply Rle_sym1.
-Apply cond_pos_sum.
-Intro; Apply Rabsolu_pos.
+Lemma cauchy_abs :
+ forall An:nat -> R,
+   Cauchy_crit_series (fun i:nat => Rabs (An i)) -> Cauchy_crit_series An.
+unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *.
+intros.
+elim (H eps H0); intros.
+exists x.
+intros.
+cut
+ (R_dist (sum_f_R0 An n) (sum_f_R0 An m) <=
+  R_dist (sum_f_R0 (fun i:nat => Rabs (An i)) n)
+    (sum_f_R0 (fun i:nat => Rabs (An i)) m)).
+intro.
+apply Rle_lt_trans with
+ (R_dist (sum_f_R0 (fun i:nat => Rabs (An i)) n)
+    (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.
+rewrite (tech2 An n m); [ idtac | assumption ].
+rewrite (tech2 (fun i:nat => Rabs (An i)) n m); [ idtac | assumption ].
+unfold R_dist in |- *.
+unfold Rminus in |- *.
+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.
+rewrite
+ (Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S n + i)%nat)) (m - S n)))
+ .
+pose (Bn := fun i:nat => An (S n + i)%nat).
+replace (fun i:nat => Rabs (An (S n + i)%nat)) with
+ (fun i:nat => Rabs (Bn i)).
+apply Rabs_triang_gen.
+unfold Bn in |- *; reflexivity.
+apply Rle_ge.
+apply cond_pos_sum.
+intro; apply Rabs_pos.
+rewrite b.
+unfold R_dist in |- *.
+unfold Rminus in |- *; do 2 rewrite Rplus_opp_r.
+rewrite Rabs_R0; right; reflexivity.
+rewrite (tech2 An m n); [ idtac | assumption ].
+rewrite (tech2 (fun i:nat => Rabs (An i)) m n); [ idtac | assumption ].
+unfold R_dist in |- *.
+unfold Rminus in |- *.
+do 2 rewrite Rplus_assoc.
+rewrite (Rplus_comm (sum_f_R0 An m)).
+rewrite (Rplus_comm (sum_f_R0 (fun i:nat => Rabs (An i)) m)).
+do 2 rewrite Rplus_assoc.
+do 2 rewrite Rplus_opp_l.
+do 2 rewrite Rplus_0_r.
+rewrite
+ (Rabs_right (sum_f_R0 (fun i:nat => Rabs (An (S m + i)%nat)) (n - S m)))
+ .
+pose (Bn := fun i:nat => An (S m + i)%nat).
+replace (fun i:nat => Rabs (An (S m + i)%nat)) with
+ (fun i:nat => Rabs (Bn i)).
+apply Rabs_triang_gen.
+unfold Bn in |- *; reflexivity.
+apply Rle_ge.
+apply cond_pos_sum.
+intro; apply Rabs_pos.
 Qed.
 
 (**********)
-Lemma cv_cauchy_1 : (An:nat->R) (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)) -> (Cauchy_crit_series An).
-Intros.
-Elim X; Intros.
-Unfold Un_cv in p.
-Unfold Cauchy_crit_series; Unfold Cauchy_crit.
-Intros.
-Cut ``0<eps/2``.
-Intro.
-Elim (p ``eps/2`` H0); Intros.
-Exists x0.
-Intros.
-Apply Rle_lt_trans with ``(R_dist (sum_f_R0 An n) x)+(R_dist (sum_f_R0 An m) x)``.
-Unfold R_dist.
-Replace ``(sum_f_R0 An n)-(sum_f_R0 An m)`` with ``((sum_f_R0 An n)-x)+ -((sum_f_R0 An m)-x)``; [Idtac | Ring].
-Rewrite <- (Rabsolu_Ropp ``(sum_f_R0 An m)-x``).
-Apply Rabsolu_triang.
-Apply Rlt_le_trans with ``eps/2+eps/2``.
-Apply Rplus_lt.
-Apply H1; Assumption.
-Apply H1; Assumption.
-Right; Symmetry; Apply double_var.
-Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0].
+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.
+elim X; intros.
+unfold Un_cv in p.
+unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *.
+intros.
+cut (0 < eps / 2).
+intro.
+elim (p (eps / 2) H0); intros.
+exists x0.
+intros.
+apply Rle_lt_trans with (R_dist (sum_f_R0 An n) x + R_dist (sum_f_R0 An m) x).
+unfold R_dist in |- *.
+replace (sum_f_R0 An n - sum_f_R0 An m) with
+ (sum_f_R0 An n - x + - (sum_f_R0 An m - x)); [ idtac | ring ].
+rewrite <- (Rabs_Ropp (sum_f_R0 An m - x)).
+apply Rabs_triang.
+apply Rlt_le_trans with (eps / 2 + eps / 2).
+apply Rplus_lt_compat.
+apply H1; assumption.
+apply H1; assumption.
+right; symmetry  in |- *; apply double_var.
+unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+ [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
 Qed.
 
-Lemma cv_cauchy_2 : (An:nat->R) (Cauchy_crit_series An) -> (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)).
-Intros.
-Apply R_complete.
-Unfold Cauchy_crit_series in H.
-Exact H.
+Lemma cv_cauchy_2 :
+ forall An:nat -> R,
+   Cauchy_crit_series An ->
+   sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l).
+intros.
+apply R_complete.
+unfold Cauchy_crit_series in H.
+exact H.
 Qed.
 
 (**********)
-Lemma sum_eq_R0 : (An:nat->R;N:nat) ((n:nat)(le n N)->``(An n)==0``) -> (sum_f_R0 An N)==R0.
-Intros; Induction N.
-Simpl; Apply H; Apply le_n.
-Rewrite tech5; Rewrite HrecN; [Rewrite Rplus_Ol; Apply H; Apply le_n | Intros; Apply H; Apply le_trans with N; [Assumption | Apply le_n_Sn]].
+Lemma sum_eq_R0 :
+ forall (An:nat -> R) (N:nat),
+   (forall n:nat, (n <= N)%nat -> An n = 0) -> sum_f_R0 An N = 0.
+intros; induction  N as [| N HrecN].
+simpl in |- *; apply H; apply le_n.
+rewrite tech5; rewrite HrecN;
+ [ rewrite Rplus_0_l; apply H; apply le_n
+ | intros; apply H; apply le_trans with N; [ assumption | apply le_n_Sn ] ].
 Qed.
 
-Definition SP [fn:nat->R->R;N:nat] : R->R := [x:R](sum_f_R0 [k:nat]``(fn k x)`` N).
+Definition SP (fn:nat -> R -> R) (N:nat) (x:R) : R :=
+  sum_f_R0 (fun k:nat => fn k x) N.
 
 (**********)
-Lemma sum_incr : (An:nat->R;N:nat;l:R) (Un_cv [n:nat](sum_f_R0 An n) l) -> ((n:nat)``0<=(An n)``) -> ``(sum_f_R0 An N)<=l``.
-Intros; Case (total_order_T (sum_f_R0 An N) l); Intro.
-Elim s; Intro.
-Left; Apply a.
-Right; Apply b.
-Cut (Un_growing [n:nat](sum_f_R0 An n)).
-Intro; Pose l1 := (sum_f_R0 An N).
-Fold l1 in r.
-Unfold Un_cv in H; Cut ``0<l1-l``.
-Intro; Elim (H ? H2); Intros.
-Pose N0 := (max x N); Cut (ge N0 x).
-Intro; Assert H5 := (H3 N0 H4).
-Cut ``l1<=(sum_f_R0 An N0)``.
-Intro; Unfold R_dist in H5; Rewrite Rabsolu_right in H5.
-Cut ``(sum_f_R0 An N0)<l1``.
-Intro; Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H7 H6)).
-Apply Rlt_anti_compatibility with ``-l``.
-Do 2 Rewrite (Rplus_sym ``-l``).
-Apply H5.
-Apply Rle_sym1; Apply Rle_anti_compatibility with l.
-Rewrite Rplus_Or; Replace ``l+((sum_f_R0 An N0)-l)`` with (sum_f_R0 An N0); [Idtac | Ring]; Apply Rle_trans with l1.
-Left; Apply r.
-Apply H6.
-Unfold l1; Apply Rle_sym2; Apply (growing_prop [k:nat](sum_f_R0 An k)).
-Apply H1.
-Unfold ge N0; Apply le_max_r.
-Unfold ge N0; Apply le_max_l.
-Apply Rlt_anti_compatibility with l; Rewrite Rplus_Or; Replace ``l+(l1-l)`` with l1; [Apply r | Ring].
-Unfold Un_growing; Intro; Simpl; Pattern 1 (sum_f_R0 An n); Rewrite <- Rplus_Or; Apply Rle_compatibility; Apply H0.
+Lemma sum_incr :
+ forall (An:nat -> R) (N:nat) (l:R),
+   Un_cv (fun n:nat => sum_f_R0 An n) l ->
+   (forall n:nat, 0 <= An n) -> sum_f_R0 An N <= l.
+intros; case (total_order_T (sum_f_R0 An N) l); intro.
+elim s; intro.
+left; apply a.
+right; apply b.
+cut (Un_growing (fun n:nat => sum_f_R0 An n)).
+intro; pose (l1 := sum_f_R0 An N).
+fold l1 in r.
+unfold Un_cv in H; cut (0 < l1 - l).
+intro; elim (H _ H2); intros.
+pose (N0 := max x N); cut (N0 >= x)%nat.
+intro; assert (H5 := H3 N0 H4).
+cut (l1 <= sum_f_R0 An N0).
+intro; unfold R_dist in H5; rewrite Rabs_right in H5.
+cut (sum_f_R0 An N0 < l1).
+intro; elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H7 H6)).
+apply Rplus_lt_reg_r with (- l).
+do 2 rewrite (Rplus_comm (- l)).
+apply H5.
+apply Rle_ge; apply Rplus_le_reg_l with l.
+rewrite Rplus_0_r; replace (l + (sum_f_R0 An N0 - l)) with (sum_f_R0 An N0);
+ [ idtac | ring ]; apply Rle_trans with l1.
+left; apply r.
+apply H6.
+unfold l1 in |- *; apply Rge_le;
+ apply (growing_prop (fun k:nat => sum_f_R0 An k)).
+apply H1.
+unfold ge, N0 in |- *; apply le_max_r.
+unfold ge, N0 in |- *; apply le_max_l.
+apply Rplus_lt_reg_r with l; rewrite Rplus_0_r;
+ replace (l + (l1 - l)) with l1; [ apply r | ring ].
+unfold Un_growing in |- *; intro; simpl in |- *;
+ pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r;
+ apply Rplus_le_compat_l; apply H0.
 Qed.
 
 (**********)
-Lemma sum_cv_maj : (An:nat->R;fn:nat->R->R;x,l1,l2:R) (Un_cv [n:nat](SP fn n x) l1) -> (Un_cv [n:nat](sum_f_R0 An n) l2) -> ((n:nat)``(Rabsolu (fn n x))<=(An n)``) -> ``(Rabsolu l1)<=l2``.
-Intros; Case (total_order_T (Rabsolu l1) l2); Intro.
-Elim s; Intro.
-Left; Apply a.
-Right; Apply b.
-Cut (n0:nat)``(Rabsolu (SP fn n0 x))<=(sum_f_R0 An n0)``.
-Intro; Cut ``0<((Rabsolu l1)-l2)/2``.
-Intro; Unfold Un_cv in H H0.
-Elim (H ? H3); Intros Na H4.
-Elim (H0 ? H3); Intros Nb H5.
-Pose N := (max Na Nb).
-Unfold R_dist in H4 H5.
-Cut ``(Rabsolu ((sum_f_R0 An N)-l2))<((Rabsolu l1)-l2)/2``.
-Intro; Cut ``(Rabsolu ((Rabsolu l1)-(Rabsolu (SP fn N x))))<((Rabsolu l1)-l2)/2``.
-Intro; Cut ``(sum_f_R0 An N)<((Rabsolu l1)+l2)/2``.
-Intro; Cut ``((Rabsolu l1)+l2)/2<(Rabsolu (SP fn N x))``.
-Intro; Cut ``(sum_f_R0 An N)<(Rabsolu (SP fn N x))``.
-Intro; Assert H11 := (H2 N).
-Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H11 H10)).
-Apply Rlt_trans with ``((Rabsolu l1)+l2)/2``; Assumption.
-Case (case_Rabsolu ``(Rabsolu l1)-(Rabsolu (SP fn N x))``); Intro.
-Apply Rlt_trans with (Rabsolu l1).
-Apply Rlt_monotony_contra with ``2``.
-Sup0.
-Unfold Rdiv; Rewrite (Rmult_sym ``2``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Rewrite double; Apply Rlt_compatibility; Apply r.
-DiscrR.
-Apply (Rminus_lt ? ? r0).
-Rewrite (Rabsolu_right ? r0) in H7.
-Apply Rlt_anti_compatibility with ``((Rabsolu l1)-l2)/2-(Rabsolu (SP fn N x))``.
-Replace ``((Rabsolu l1)-l2)/2-(Rabsolu (SP fn N x))+((Rabsolu l1)+l2)/2`` with ``(Rabsolu l1)-(Rabsolu (SP fn N x))``.
-Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply H7.
-Unfold Rdiv; Rewrite Rmult_Rplus_distrl; Rewrite <- (Rmult_sym ``/2``); Rewrite Rminus_distr; Repeat Rewrite (Rmult_sym ``/2``); Pattern 1 (Rabsolu l1); Rewrite double_var; Unfold Rdiv; Ring.
-Case (case_Rabsolu ``(sum_f_R0 An N)-l2``); Intro.
-Apply Rlt_trans with l2.
-Apply (Rminus_lt ? ? r0).
-Apply Rlt_monotony_contra with ``2``.
-Sup0.
-Rewrite (double l2); Unfold Rdiv; Rewrite (Rmult_sym ``2``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Rewrite (Rplus_sym (Rabsolu l1)); Apply Rlt_compatibility; Apply r.
-DiscrR.
-Rewrite (Rabsolu_right ? r0) in H6; Apply Rlt_anti_compatibility with ``-l2``.
-Replace ``-l2+((Rabsolu l1)+l2)/2`` with ``((Rabsolu l1)-l2)/2``.
-Rewrite Rplus_sym; Apply H6.
-Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite Rminus_distr; Rewrite Rmult_Rplus_distrl; Pattern 2 l2; Rewrite double_var; Repeat Rewrite (Rmult_sym ``/2``); Rewrite Ropp_distr1; Unfold Rdiv; Ring.
-Apply Rle_lt_trans with ``(Rabsolu ((SP fn N x)-l1))``.
-Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr3; Apply Rabsolu_triang_inv2.
-Apply H4; Unfold ge N; Apply le_max_l.
-Apply H5; Unfold ge N; Apply le_max_r.
-Unfold Rdiv; Apply Rmult_lt_pos.
-Apply Rlt_anti_compatibility with l2.
-Rewrite Rplus_Or; Replace ``l2+((Rabsolu l1)-l2)`` with (Rabsolu l1); [Apply r | Ring].
-Apply Rlt_Rinv; Sup0.
-Intros; Induction n0.
-Unfold SP; Simpl; Apply H1.
-Unfold SP; Simpl.
-Apply Rle_trans with (Rplus (Rabsolu (sum_f_R0 [k:nat](fn k x) n0)) (Rabsolu (fn (S n0) x))).
-Apply Rabsolu_triang.
-Apply Rle_trans with ``(sum_f_R0 An n0)+(Rabsolu (fn (S n0) x))``.
-Do 2 Rewrite <- (Rplus_sym (Rabsolu (fn (S n0) x))).
-Apply Rle_compatibility; Apply Hrecn0.
-Apply Rle_compatibility; Apply H1.
-Qed.
+Lemma sum_cv_maj :
+ forall (An:nat -> R) (fn:nat -> R -> R) (x l1 l2:R),
+   Un_cv (fun n:nat => SP fn n x) l1 ->
+   Un_cv (fun n:nat => sum_f_R0 An n) l2 ->
+   (forall n:nat, Rabs (fn n x) <= An n) -> Rabs l1 <= l2.
+intros; case (total_order_T (Rabs l1) l2); intro.
+elim s; intro.
+left; apply a.
+right; apply b.
+cut (forall n0:nat, Rabs (SP fn n0 x) <= sum_f_R0 An n0).
+intro; cut (0 < (Rabs l1 - l2) / 2).
+intro; unfold Un_cv in H, H0.
+elim (H _ H3); intros Na H4.
+elim (H0 _ H3); intros Nb H5.
+pose (N := max Na Nb).
+unfold R_dist in H4, H5.
+cut (Rabs (sum_f_R0 An N - l2) < (Rabs l1 - l2) / 2).
+intro; cut (Rabs (Rabs l1 - Rabs (SP fn N x)) < (Rabs l1 - l2) / 2).
+intro; cut (sum_f_R0 An N < (Rabs l1 + l2) / 2).
+intro; cut ((Rabs l1 + l2) / 2 < Rabs (SP fn N x)).
+intro; cut (sum_f_R0 An N < Rabs (SP fn N x)).
+intro; assert (H11 := H2 N).
+elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H10)).
+apply Rlt_trans with ((Rabs l1 + l2) / 2); assumption.
+case (Rcase_abs (Rabs l1 - Rabs (SP fn N x))); intro.
+apply Rlt_trans with (Rabs l1).
+apply Rmult_lt_reg_l with 2.
+prove_sup0.
+unfold Rdiv in |- *; rewrite (Rmult_comm 2); rewrite Rmult_assoc;
+ rewrite <- Rinv_l_sym.
+rewrite Rmult_1_r; rewrite double; apply Rplus_lt_compat_l; apply r.
+discrR.
+apply (Rminus_lt _ _ r0).
+rewrite (Rabs_right _ r0) in H7.
+apply Rplus_lt_reg_r with ((Rabs l1 - l2) / 2 - Rabs (SP fn N x)).
+replace ((Rabs l1 - l2) / 2 - Rabs (SP fn N x) + (Rabs l1 + l2) / 2) with
+ (Rabs l1 - Rabs (SP fn N x)).
+unfold Rminus in |- *; rewrite Rplus_assoc; rewrite Rplus_opp_l;
+ rewrite Rplus_0_r; apply H7.
+unfold Rdiv in |- *; rewrite Rmult_plus_distr_r;
+ rewrite <- (Rmult_comm (/ 2)); rewrite Rmult_minus_distr_l;
+ repeat rewrite (Rmult_comm (/ 2)); pattern (Rabs l1) at 1 in |- *;
+ rewrite double_var; unfold Rdiv in |- *; ring.
+case (Rcase_abs (sum_f_R0 An N - l2)); intro.
+apply Rlt_trans with l2.
+apply (Rminus_lt _ _ r0).
+apply Rmult_lt_reg_l with 2.
+prove_sup0.
+rewrite (double l2); unfold Rdiv in |- *; rewrite (Rmult_comm 2);
+ rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
+rewrite Rmult_1_r; rewrite (Rplus_comm (Rabs l1)); apply Rplus_lt_compat_l;
+ apply r.
+discrR.
+rewrite (Rabs_right _ r0) in H6; apply Rplus_lt_reg_r with (- l2).
+replace (- l2 + (Rabs l1 + l2) / 2) with ((Rabs l1 - l2) / 2).
+rewrite Rplus_comm; apply H6.
+unfold Rdiv in |- *; rewrite <- (Rmult_comm (/ 2));
+ rewrite Rmult_minus_distr_l; rewrite Rmult_plus_distr_r;
+ pattern l2 at 2 in |- *; rewrite double_var;
+ repeat rewrite (Rmult_comm (/ 2)); rewrite Ropp_plus_distr;
+ unfold Rdiv in |- *; ring.
+apply Rle_lt_trans with (Rabs (SP fn N x - l1)).
+rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr'; apply Rabs_triang_inv2.
+apply H4; unfold ge, N in |- *; apply le_max_l.
+apply H5; unfold ge, N in |- *; apply le_max_r.
+unfold Rdiv in |- *; apply Rmult_lt_0_compat.
+apply Rplus_lt_reg_r with l2.
+rewrite Rplus_0_r; replace (l2 + (Rabs l1 - l2)) with (Rabs l1);
+ [ apply r | ring ].
+apply Rinv_0_lt_compat; prove_sup0.
+intros; induction  n0 as [| n0 Hrecn0].
+unfold SP in |- *; simpl in |- *; apply H1.
+unfold SP in |- *; simpl in |- *.
+apply Rle_trans with
+ (Rabs (sum_f_R0 (fun k:nat => fn k x) n0) + Rabs (fn (S n0) x)).
+apply Rabs_triang.
+apply Rle_trans with (sum_f_R0 An n0 + Rabs (fn (S n0) x)).
+do 2 rewrite <- (Rplus_comm (Rabs (fn (S n0) x))).
+apply Rplus_le_compat_l; apply Hrecn0.
+apply Rplus_le_compat_l; apply H1.
+Qed.
\ No newline at end of file