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, 385 insertions, 275 deletions

diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 03963fc4d..ffac3df29 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -8,9 +8,9 @@
  
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
-Require Max.
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import Max.
 Require Export Rseries.
 Require Export SeqProp.
 Require Export Rcomplete.
@@ -21,287 +21,397 @@ Require Export Rsigma.
 Require Export Rprod.
 Require Export Cauchy_prod.
 Require Export Alembert.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
 Open Local Scope R_scope.
 
 (**********)
-Lemma sum_maj1 : (fn:nat->R->R;An:nat->R;x,l1,l2:R;N:nat) (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-(SP fn N x)))<=l2-(sum_f_R0 An N)``.
-Intros; Cut (sigTT R [l:R](Un_cv [n:nat](sum_f_R0 [l:nat](fn (plus (S N) l) x) n) l)).
-Intro; Cut (sigTT R [l:R](Un_cv [n:nat](sum_f_R0 [l:nat](An (plus (S N) l)) n) l)).
-Intro; 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``.
-Intro; Rewrite H4; Rewrite H5.
-Apply sum_cv_maj with [l:nat](An (plus (S N) l)) [l:nat][x:R](fn (plus (S N) l) x) x.
-Unfold SP; Apply H2.
-Apply H3.
-Intros; Apply H1.
-Symmetry; EApply UL_sequence.
-Apply H3.
-Unfold Un_cv in H0; Unfold Un_cv; Intros; Elim (H0 eps H5); Intros N0 H6.
-Unfold R_dist in H6; Exists N0; Intros.
-Unfold R_dist; Replace (Rminus (sum_f_R0 [l:nat](An (plus (S N) l)) n) (Rminus l2 (sum_f_R0 An N))) with (Rminus (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) l2); [Idtac | Ring].
-Replace (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) with (sum_f_R0 An (S (plus N n))).
-Apply H6; Unfold ge; Apply le_trans with n.
-Apply H7.
-Apply le_trans with (plus N n).
-Apply le_plus_r.
-Apply le_n_Sn.
-Cut (le O N).
-Cut (lt N (S (plus N n))).
-Intros; Assert H10 := (sigma_split An H9 H8).
-Unfold sigma in H10.
-Do 2 Rewrite <- minus_n_O in H10.
-Replace (sum_f_R0 An (S (plus N n))) with (sum_f_R0 [k:nat](An (plus (0) k)) (S (plus N n))).
-Replace (sum_f_R0 An N) with (sum_f_R0 [k:nat](An (plus (0) k)) N).
-Cut (minus (S (plus N n)) (S N))=n.
-Intro; Rewrite H11 in H10.
-Apply H10.
-Apply INR_eq; Rewrite minus_INR.
-Do 2 Rewrite S_INR; Rewrite plus_INR; Ring.
-Apply le_n_S; Apply le_plus_l.
-Apply sum_eq; Intros.
-Reflexivity.
-Apply sum_eq; Intros.
-Reflexivity.
-Apply le_lt_n_Sm; Apply le_plus_l.
-Apply le_O_n.
-Symmetry; EApply UL_sequence.
-Apply H2.
-Unfold Un_cv in H; Unfold Un_cv; Intros.
-Elim (H eps H4); Intros N0 H5.
-Unfold R_dist in H5; Exists N0; Intros.
-Unfold R_dist SP; Replace (Rminus (sum_f_R0 [l:nat](fn (plus (S N) l) x) n) (Rminus l1 (sum_f_R0 [k:nat](fn k x) N))) with (Rminus (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) l1); [Idtac | Ring].
-Replace (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) with (sum_f_R0 [k:nat](fn k x) (S (plus N n))).
-Unfold SP in H5; Apply H5; Unfold ge; Apply le_trans with n.
-Apply H6.
-Apply le_trans with (plus N n).
-Apply le_plus_r.
-Apply le_n_Sn.
-Cut (le O N).
-Cut (lt N (S (plus N n))).
-Intros; Assert H9 := (sigma_split [k:nat](fn k x) H8 H7).
-Unfold sigma in H9.
-Do 2 Rewrite <- minus_n_O in H9.
-Replace (sum_f_R0 [k:nat](fn k x) (S (plus N n))) with (sum_f_R0 [k:nat](fn (plus (0) k) x) (S (plus N n))).
-Replace (sum_f_R0 [k:nat](fn k x) N) with (sum_f_R0 [k:nat](fn (plus (0) k) x) N).
-Cut (minus (S (plus N n)) (S N))=n.
-Intro; Rewrite H10 in H9.
-Apply H9.
-Apply INR_eq; Rewrite minus_INR.
-Do 2 Rewrite S_INR; Rewrite plus_INR; Ring.
-Apply le_n_S; Apply le_plus_l.
-Apply sum_eq; Intros.
-Reflexivity.
-Apply sum_eq; Intros.
-Reflexivity.
-Apply le_lt_n_Sm.
-Apply le_plus_l.
-Apply le_O_n.
-Apply existTT with ``l2-(sum_f_R0 An N)``.
-Unfold Un_cv in H0; Unfold Un_cv; Intros.
-Elim (H0 eps H2); Intros N0 H3.
-Unfold R_dist in H3; Exists N0; Intros.
-Unfold R_dist; Replace (Rminus (sum_f_R0 [l:nat](An (plus (S N) l)) n) (Rminus l2 (sum_f_R0 An N))) with (Rminus (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) l2); [Idtac | Ring].
-Replace (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) with (sum_f_R0 An (S (plus N n))).
-Apply H3; Unfold ge; Apply le_trans with n.
-Apply H4.
-Apply le_trans with (plus N n).
-Apply le_plus_r.
-Apply le_n_Sn.
-Cut (le O N).
-Cut (lt N (S (plus N n))).
-Intros; Assert H7 := (sigma_split An H6 H5).
-Unfold sigma in H7.
-Do 2 Rewrite <- minus_n_O in H7.
-Replace (sum_f_R0 An (S (plus N n))) with (sum_f_R0 [k:nat](An (plus (0) k)) (S (plus N n))).
-Replace (sum_f_R0 An N) with (sum_f_R0 [k:nat](An (plus (0) k)) N).
-Cut (minus (S (plus N n)) (S N))=n.
-Intro; Rewrite H8 in H7.
-Apply H7.
-Apply INR_eq; Rewrite minus_INR.
-Do 2 Rewrite S_INR; Rewrite plus_INR; Ring.
-Apply le_n_S; Apply le_plus_l.
-Apply sum_eq; Intros.
-Reflexivity.
-Apply sum_eq; Intros.
-Reflexivity.
-Apply le_lt_n_Sm.
-Apply le_plus_l.
-Apply le_O_n.
-Apply existTT with ``l1-(SP fn N x)``.
-Unfold Un_cv in H; Unfold Un_cv; Intros.
-Elim (H eps H2); Intros N0 H3.
-Unfold R_dist in H3; Exists N0; Intros.
-Unfold R_dist SP.
-Replace (Rminus (sum_f_R0 [l:nat](fn (plus (S N) l) x) n) (Rminus l1 (sum_f_R0 [k:nat](fn k x) N))) with (Rminus (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) l1); [Idtac | Ring].
-Replace (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) with (sum_f_R0 [k:nat](fn k x) (S (plus N n))).
-Unfold SP in H3; Apply H3.
-Unfold ge; Apply le_trans with n.
-Apply H4.
-Apply le_trans with (plus N n).
-Apply le_plus_r.
-Apply le_n_Sn.
-Cut (le O N).
-Cut (lt N (S (plus N n))).
-Intros; Assert H7 := (sigma_split [k:nat](fn k x) H6 H5).
-Unfold sigma in H7.
-Do 2 Rewrite <- minus_n_O in H7.
-Replace (sum_f_R0 [k:nat](fn k x) (S (plus N n))) with (sum_f_R0 [k:nat](fn (plus (0) k) x) (S (plus N n))).
-Replace (sum_f_R0 [k:nat](fn k x) N) with (sum_f_R0 [k:nat](fn (plus (0) k) x) N).
-Cut (minus (S (plus N n)) (S N))=n.
-Intro; Rewrite H8 in H7.
-Apply H7.
-Apply INR_eq; Rewrite minus_INR.
-Do 2 Rewrite S_INR; Rewrite plus_INR; Ring.
-Apply le_n_S; Apply le_plus_l.
-Apply sum_eq; Intros.
-Reflexivity.
-Apply sum_eq; Intros.
-Reflexivity.
-Apply le_lt_n_Sm.
-Apply le_plus_l.
-Apply le_O_n.
+Lemma sum_maj1 :
+ forall (fn:nat -> R -> R) (An:nat -> R) (x l1 l2:R) 
+   (N:nat),
+   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 - SP fn N x) <= l2 - sum_f_R0 An N.
+intros;
+ cut
+  (sigT
+     (fun l:R =>
+        Un_cv (fun n:nat => sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) l)).
+intro;
+ 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.
+elim X0; intros l2N H3.
+cut (l1 - SP fn N x = l1N).
+intro; cut (l2 - sum_f_R0 An N = l2N).
+intro; rewrite H4; rewrite H5.
+apply sum_cv_maj with
+ (fun l:nat => An (S N + l)%nat) (fun (l:nat) (x:R) => fn (S N + l)%nat x) x.
+unfold SP in |- *; apply H2.
+apply H3.
+intros; apply H1.
+symmetry  in |- *; eapply UL_sequence.
+apply H3.
+unfold Un_cv in H0; unfold Un_cv in |- *; intros; elim (H0 eps H5);
+ intros N0 H6.
+unfold R_dist in H6; exists N0; intros.
+unfold R_dist in |- *;
+ replace (sum_f_R0 (fun l:nat => An (S N + l)%nat) n - (l2 - sum_f_R0 An N))
+  with (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n - l2);
+ [ idtac | ring ].
+replace (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n) with
+ (sum_f_R0 An (S (N + n))).
+apply H6; unfold ge in |- *; apply le_trans with n.
+apply H7.
+apply le_trans with (N + n)%nat.
+apply le_plus_r.
+apply le_n_Sn.
+cut (0 <= N)%nat.
+cut (N < S (N + n))%nat.
+intros; assert (H10 := sigma_split An H9 H8).
+unfold sigma in H10.
+do 2 rewrite <- minus_n_O in H10.
+replace (sum_f_R0 An (S (N + n))) with
+ (sum_f_R0 (fun k:nat => An (0 + k)%nat) (S (N + n))).
+replace (sum_f_R0 An N) with (sum_f_R0 (fun k:nat => An (0 + k)%nat) N).
+cut ((S (N + n) - S N)%nat = n).
+intro; rewrite H11 in H10.
+apply H10.
+apply INR_eq; rewrite minus_INR.
+do 2 rewrite S_INR; rewrite plus_INR; ring.
+apply le_n_S; apply le_plus_l.
+apply sum_eq; intros.
+reflexivity.
+apply sum_eq; intros.
+reflexivity.
+apply le_lt_n_Sm; apply le_plus_l.
+apply le_O_n.
+symmetry  in |- *; eapply UL_sequence.
+apply H2.
+unfold Un_cv in H; unfold Un_cv in |- *; intros.
+elim (H eps H4); intros N0 H5.
+unfold R_dist in H5; exists N0; intros.
+unfold R_dist, SP in |- *;
+ replace
+  (sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n -
+   (l1 - sum_f_R0 (fun k:nat => fn k x) N)) with
+  (sum_f_R0 (fun k:nat => fn k x) N +
+   sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n - l1); 
+ [ idtac | ring ].
+replace
+ (sum_f_R0 (fun k:nat => fn k x) N +
+  sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) with
+ (sum_f_R0 (fun k:nat => fn k x) (S (N + n))).
+unfold SP in H5; apply H5; unfold ge in |- *; apply le_trans with n.
+apply H6.
+apply le_trans with (N + n)%nat.
+apply le_plus_r.
+apply le_n_Sn.
+cut (0 <= N)%nat.
+cut (N < S (N + n))%nat.
+intros; assert (H9 := sigma_split (fun k:nat => fn k x) H8 H7).
+unfold sigma in H9.
+do 2 rewrite <- minus_n_O in H9.
+replace (sum_f_R0 (fun k:nat => fn k x) (S (N + n))) with
+ (sum_f_R0 (fun k:nat => fn (0 + k)%nat x) (S (N + n))).
+replace (sum_f_R0 (fun k:nat => fn k x) N) with
+ (sum_f_R0 (fun k:nat => fn (0 + k)%nat x) N).
+cut ((S (N + n) - S N)%nat = n).
+intro; rewrite H10 in H9.
+apply H9.
+apply INR_eq; rewrite minus_INR.
+do 2 rewrite S_INR; rewrite plus_INR; ring.
+apply le_n_S; apply le_plus_l.
+apply sum_eq; intros.
+reflexivity.
+apply sum_eq; intros.
+reflexivity.
+apply le_lt_n_Sm.
+apply le_plus_l.
+apply le_O_n.
+apply existT with (l2 - sum_f_R0 An N).
+unfold Un_cv in H0; unfold Un_cv in |- *; intros.
+elim (H0 eps H2); intros N0 H3.
+unfold R_dist in H3; exists N0; intros.
+unfold R_dist in |- *;
+ replace (sum_f_R0 (fun l:nat => An (S N + l)%nat) n - (l2 - sum_f_R0 An N))
+  with (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n - l2);
+ [ idtac | ring ].
+replace (sum_f_R0 An N + sum_f_R0 (fun l:nat => An (S N + l)%nat) n) with
+ (sum_f_R0 An (S (N + n))).
+apply H3; unfold ge in |- *; apply le_trans with n.
+apply H4.
+apply le_trans with (N + n)%nat.
+apply le_plus_r.
+apply le_n_Sn.
+cut (0 <= N)%nat.
+cut (N < S (N + n))%nat.
+intros; assert (H7 := sigma_split An H6 H5).
+unfold sigma in H7.
+do 2 rewrite <- minus_n_O in H7.
+replace (sum_f_R0 An (S (N + n))) with
+ (sum_f_R0 (fun k:nat => An (0 + k)%nat) (S (N + n))).
+replace (sum_f_R0 An N) with (sum_f_R0 (fun k:nat => An (0 + k)%nat) N).
+cut ((S (N + n) - S N)%nat = n).
+intro; rewrite H8 in H7.
+apply H7.
+apply INR_eq; rewrite minus_INR.
+do 2 rewrite S_INR; rewrite plus_INR; ring.
+apply le_n_S; apply le_plus_l.
+apply sum_eq; intros.
+reflexivity.
+apply sum_eq; intros.
+reflexivity.
+apply le_lt_n_Sm.
+apply le_plus_l.
+apply le_O_n.
+apply existT with (l1 - SP fn N x).
+unfold Un_cv in H; unfold Un_cv in |- *; intros.
+elim (H eps H2); intros N0 H3.
+unfold R_dist in H3; exists N0; intros.
+unfold R_dist, SP in |- *.
+replace
+ (sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n -
+  (l1 - sum_f_R0 (fun k:nat => fn k x) N)) with
+ (sum_f_R0 (fun k:nat => fn k x) N +
+  sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n - l1); 
+ [ idtac | ring ].
+replace
+ (sum_f_R0 (fun k:nat => fn k x) N +
+  sum_f_R0 (fun l:nat => fn (S N + l)%nat x) n) with
+ (sum_f_R0 (fun k:nat => fn k x) (S (N + n))).
+unfold SP in H3; apply H3.
+unfold ge in |- *; apply le_trans with n.
+apply H4.
+apply le_trans with (N + n)%nat.
+apply le_plus_r.
+apply le_n_Sn.
+cut (0 <= N)%nat.
+cut (N < S (N + n))%nat.
+intros; assert (H7 := sigma_split (fun k:nat => fn k x) H6 H5).
+unfold sigma in H7.
+do 2 rewrite <- minus_n_O in H7.
+replace (sum_f_R0 (fun k:nat => fn k x) (S (N + n))) with
+ (sum_f_R0 (fun k:nat => fn (0 + k)%nat x) (S (N + n))).
+replace (sum_f_R0 (fun k:nat => fn k x) N) with
+ (sum_f_R0 (fun k:nat => fn (0 + k)%nat x) N).
+cut ((S (N + n) - S N)%nat = n).
+intro; rewrite H8 in H7.
+apply H7.
+apply INR_eq; rewrite minus_INR.
+do 2 rewrite S_INR; rewrite plus_INR; ring.
+apply le_n_S; apply le_plus_l.
+apply sum_eq; intros.
+reflexivity.
+apply sum_eq; intros.
+reflexivity.
+apply le_lt_n_Sm.
+apply le_plus_l.
+apply le_O_n.
 Qed.
 
 (* Comparaison of convergence for series *)
-Lemma Rseries_CV_comp : (An,Bn:nat->R) ((n:nat)``0<=(An n)<=(Bn n)``) -> (sigTT ? [l:R](Un_cv [N:nat](sum_f_R0 Bn N) l)) -> (sigTT ? [l:R](Un_cv [N:nat](sum_f_R0 An N) l)).
-Intros; Apply cv_cauchy_2.
-Assert H0 := (cv_cauchy_1 ? X).
-Unfold Cauchy_crit_series; Unfold Cauchy_crit.
-Intros; Elim (H0 eps H1); Intros.
-Exists x; Intros.
-Cut (Rle (R_dist (sum_f_R0 An n) (sum_f_R0 An m)) (R_dist (sum_f_R0 Bn n) (sum_f_R0 Bn m))).
-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_distr1; Do 2 Rewrite <- Rplus_assoc; Do 2 Rewrite Rplus_Ropp_r; Do 2 Rewrite Rplus_Ol; Do 2 Rewrite Rabsolu_Ropp; Repeat Rewrite Rabsolu_right.
-Apply sum_Rle; Intros.
-Elim (H (plus (S n) n0)); Intros.
-Apply H8.
-Apply Rle_sym1; Apply cond_pos_sum; Intro.
-Elim (H (plus (S n) n0)); Intros.
-Apply Rle_trans with (An (plus (S n) n0)); Assumption.
-Apply Rle_sym1; Apply cond_pos_sum; Intro.
-Elim (H (plus (S n) n0)); Intros; Assumption.
-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 Bn 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 Bn m)); Do 2 Rewrite Rplus_assoc; Do 2 Rewrite Rplus_Ropp_l; Do 2 Rewrite Rplus_Or; Repeat Rewrite Rabsolu_right.
-Apply sum_Rle; Intros.
-Elim (H (plus (S m) n0)); Intros; Apply H8.
-Apply Rle_sym1; Apply cond_pos_sum; Intro.
-Elim (H (plus (S m) n0)); Intros.
-Apply Rle_trans with (An (plus (S m) n0)); Assumption.
-Apply Rle_sym1.
-Apply cond_pos_sum; Intro.
-Elim (H (plus (S m) n0)); Intros; Assumption.
+Lemma Rseries_CV_comp :
+ forall An Bn:nat -> R,
+   (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.
+assert (H0 := cv_cauchy_1 _ X).
+unfold Cauchy_crit_series in |- *; unfold Cauchy_crit in |- *.
+intros; elim (H0 eps H1); intros.
+exists x; intros.
+cut
+ (R_dist (sum_f_R0 An n) (sum_f_R0 An m) <=
+  R_dist (sum_f_R0 Bn n) (sum_f_R0 Bn m)).
+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 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; 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 in |- *; unfold Rminus in |- *;
+ 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 in |- *; unfold Rminus in |- *; 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 *)
-Lemma Cesaro : (An,Bn:nat->R;l:R) (Un_cv Bn l) -> ((n:nat)``0<(An n)``) -> (cv_infty [n:nat](sum_f_R0 An n)) -> (Un_cv [n:nat](Rdiv (sum_f_R0 [k:nat]``(An k)*(Bn k)`` n) (sum_f_R0 An n)) l).
-Proof with Trivial.
-Unfold Un_cv; Intros; Assert H3 : (n:nat)``0<(sum_f_R0 An n)``.
-Intro; Apply tech1.
-Assert H4 : (n:nat) ``(sum_f_R0 An n)<>0``.
-Intro; Red; Intro; Assert H5 := (H3 n); Rewrite H4 in H5; Elim (Rlt_antirefl ? H5).
-Assert H5 := (cv_infty_cv_R0 ? H4 H1); Assert H6 : ``0<eps/2``.
-Unfold Rdiv; Apply Rmult_lt_pos.
-Apply Rlt_Rinv; Sup.
-Elim (H ? H6); Clear H; Intros N1 H; Pose C := (Rabsolu (sum_f_R0 [k:nat]``(An k)*((Bn k)-l)`` N1)); Assert H7 : (EX N:nat | (n:nat) (le N n) -> ``C/(sum_f_R0 An n)<eps/2``).
-Case (Req_EM C R0); Intro.
-Exists O; Intros.
-Rewrite H7; Unfold Rdiv; Rewrite Rmult_Ol; Apply Rmult_lt_pos.
-Apply Rlt_Rinv; Sup.
-Assert H8 : ``0<eps/(2*(Rabsolu C))``.
-Unfold Rdiv; Apply Rmult_lt_pos.
-Apply Rlt_Rinv; Apply Rmult_lt_pos.
-Sup.
-Apply Rabsolu_pos_lt.
-Elim (H5 ? H8); Intros; Exists x; Intros; Assert H11 := (H9 ? H10); Unfold R_dist in H11; Unfold Rminus in H11; Rewrite Ropp_O in H11; Rewrite Rplus_Or in H11.
-Apply Rle_lt_trans with (Rabsolu ``C/(sum_f_R0 An n)``).
-Apply Rle_Rabsolu.
-Unfold Rdiv; Rewrite Rabsolu_mult; Apply Rlt_monotony_contra with ``/(Rabsolu C)``.
-Apply Rlt_Rinv; Apply Rabsolu_pos_lt.
-Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1l; Replace ``/(Rabsolu C)*(eps*/2)`` with ``eps/(2*(Rabsolu C))``.
-Unfold Rdiv; Rewrite Rinv_Rmult.
-Ring.
-DiscrR.
-Apply Rabsolu_no_R0.
-Apply Rabsolu_no_R0.
-Elim H7; Clear H7; Intros N2 H7; Pose N := (max N1 N2); Exists (S N); Intros; Unfold R_dist; Replace (Rminus (Rdiv (sum_f_R0 [k:nat]``(An k)*(Bn k)`` n) (sum_f_R0 An n)) l) with (Rdiv (sum_f_R0 [k:nat]``(An k)*((Bn k)-l)`` n) (sum_f_R0 An n)).
-Assert H9 : (lt N1 n).
-Apply lt_le_trans with (S N).
-Apply le_lt_n_Sm; Unfold N; Apply le_max_l.
-Rewrite (tech2 [k:nat]``(An k)*((Bn k)-l)`` ? ? H9); Unfold Rdiv; Rewrite Rmult_Rplus_distrl; Apply Rle_lt_trans with (Rplus (Rabsolu (Rdiv (sum_f_R0 [k:nat]``(An k)*((Bn k)-l)`` N1) (sum_f_R0 An n))) (Rabsolu (Rdiv (sum_f_R0 [i:nat]``(An (plus (S N1) i))*((Bn (plus (S N1) i))-l)`` (minus n (S N1))) (sum_f_R0 An n)))).
-Apply Rabsolu_triang.
-Rewrite (double_var eps); Apply Rplus_lt.
-Unfold Rdiv; Rewrite Rabsolu_mult; Fold C; Rewrite Rabsolu_right.
-Apply (H7 n); Apply le_trans with (S N).
-Apply le_trans with N; [Unfold N; Apply le_max_r | Apply le_n_Sn].
-Apply Rle_sym1; Left; Apply Rlt_Rinv.
+Lemma Cesaro :
+ forall (An Bn:nat -> R) (l:R),
+   Un_cv Bn l ->
+   (forall n:nat, 0 < An n) ->
+   cv_infty (fun n:nat => sum_f_R0 An n) ->
+   Un_cv (fun n:nat => sum_f_R0 (fun k:nat => An k * Bn k) n / sum_f_R0 An n)
+     l.
+Proof with trivial.
+unfold Un_cv in |- *; intros; assert (H3 : forall n:nat, 0 < sum_f_R0 An n)...
+intro; apply tech1...
+assert (H4 : forall n:nat, sum_f_R0 An n <> 0)...
+intro; red in |- *; intro; assert (H5 := H3 n); rewrite H4 in H5;
+ elim (Rlt_irrefl _ H5)...
+assert (H5 := cv_infty_cv_R0 _ H4 H1); assert (H6 : 0 < eps / 2)...
+unfold Rdiv in |- *; apply Rmult_lt_0_compat...
+apply Rinv_0_lt_compat; prove_sup...
+elim (H _ H6); clear H; intros N1 H;
+ pose (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1));
+ assert
+  (H7 :
+    exists N : nat
+   | (forall n:nat, (N <= n)%nat -> C / sum_f_R0 An n < eps / 2))...
+case (Req_dec C 0); intro...
+exists 0%nat; intros...
+rewrite H7; unfold Rdiv in |- *; rewrite Rmult_0_l; apply Rmult_lt_0_compat...
+apply Rinv_0_lt_compat; prove_sup...
+assert (H8 : 0 < eps / (2 * Rabs C))...
+unfold Rdiv in |- *; apply Rmult_lt_0_compat...
+apply Rinv_0_lt_compat; apply Rmult_lt_0_compat...
+prove_sup...
+apply Rabs_pos_lt...
+elim (H5 _ H8); intros; exists x; intros; assert (H11 := H9 _ H10);
+ unfold R_dist in H11; unfold Rminus in H11; rewrite Ropp_0 in H11;
+ rewrite Rplus_0_r in H11...
+apply Rle_lt_trans with (Rabs (C / sum_f_R0 An n))...
+apply RRle_abs...
+unfold Rdiv in |- *; rewrite Rabs_mult; apply Rmult_lt_reg_l with (/ Rabs C)...
+apply Rinv_0_lt_compat; apply Rabs_pos_lt...
+rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym...
+rewrite Rmult_1_l; replace (/ Rabs C * (eps * / 2)) with (eps / (2 * Rabs C))...
+unfold Rdiv in |- *; rewrite Rinv_mult_distr...
+ring...
+discrR...
+apply Rabs_no_R0...
+apply Rabs_no_R0...
+elim H7; clear H7; intros N2 H7; pose (N := max N1 N2); exists (S N); intros;
+ unfold R_dist in |- *;
+ replace (sum_f_R0 (fun k:nat => An k * Bn k) n / sum_f_R0 An n - l) with
+  (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n / sum_f_R0 An n)...
+assert (H9 : (N1 < n)%nat)...
+apply lt_le_trans with (S N)...
+apply le_lt_n_Sm; unfold N in |- *; apply le_max_l...
+rewrite (tech2 (fun k:nat => An k * (Bn k - l)) _ _ H9); unfold Rdiv in |- *;
+ rewrite Rmult_plus_distr_r;
+ apply Rle_lt_trans with
+  (Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1 / sum_f_R0 An n) +
+   Rabs
+     (sum_f_R0 (fun i:nat => An (S N1 + i)%nat * (Bn (S N1 + i)%nat - l))
+        (n - S N1) / sum_f_R0 An n))...
+apply Rabs_triang...
+rewrite (double_var eps); apply Rplus_lt_compat...
+unfold Rdiv in |- *; rewrite Rabs_mult; fold C in |- *; rewrite Rabs_right...
+apply (H7 n); apply le_trans with (S N)...
+apply le_trans with N; [ unfold N in |- *; apply le_max_r | apply le_n_Sn ]...
+apply Rle_ge; left; apply Rinv_0_lt_compat...
 
-Unfold R_dist in H; Unfold Rdiv; Rewrite Rabsolu_mult; Rewrite (Rabsolu_right ``/(sum_f_R0 An n)``).
-Apply Rle_lt_trans with (Rmult (sum_f_R0 [i:nat](Rabsolu ``(An (plus (S N1) i))*((Bn (plus (S N1) i))-l)``) (minus n (S N1))) ``/(sum_f_R0 An n)``).
-Do 2 Rewrite <- (Rmult_sym ``/(sum_f_R0 An n)``); Apply Rle_monotony.
-Left; Apply Rlt_Rinv.
-Apply (sum_Rabsolu [i:nat]``(An (plus (S N1) i))*((Bn (plus (S N1) i))-l)`` (minus n (S N1))).
-Apply Rle_lt_trans with (Rmult (sum_f_R0 [i:nat]``(An (plus (S N1) i))*eps/2`` (minus n (S N1))) ``/(sum_f_R0 An n)``).
-Do 2 Rewrite <- (Rmult_sym ``/(sum_f_R0 An n)``); Apply Rle_monotony.
-Left; Apply Rlt_Rinv.
-Apply sum_Rle; Intros; Rewrite Rabsolu_mult; Pattern 2 (An (plus (S N1) n0)); Rewrite <- (Rabsolu_right (An (plus (S N1) n0))).
-Apply Rle_monotony.
-Apply Rabsolu_pos.
-Left; Apply H; Unfold ge; Apply le_trans with (S N1); [Apply le_n_Sn | Apply le_plus_l].
-Apply Rle_sym1; Left.
-Rewrite <- (scal_sum [i:nat](An (plus (S N1) i)) (minus n (S N1)) ``eps/2``); Unfold Rdiv; Repeat Rewrite Rmult_assoc; Apply Rlt_monotony.
-Pattern 2 ``/2``; Rewrite <- Rmult_1r; Apply Rlt_monotony.
-Apply Rlt_Rinv; Sup.
-Rewrite Rmult_sym; Apply Rlt_monotony_contra with (sum_f_R0 An n).
-Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1l; Rewrite Rmult_1r; Rewrite (tech2 An N1 n).
-Rewrite Rplus_sym; Pattern 1 (sum_f_R0 [i:nat](An (plus (S N1) i)) (minus n (S N1))); Rewrite <- Rplus_Or; Apply Rlt_compatibility.
-Apply Rle_sym1; Left; Apply Rlt_Rinv.
-Replace (sum_f_R0 [k:nat]``(An k)*((Bn k)-l)`` n) with (Rplus (sum_f_R0 [k:nat]``(An k)*(Bn k)`` n) (sum_f_R0 [k:nat]``(An k)*-l`` n)).
-Rewrite <- (scal_sum An n ``-l``); Field.
-Rewrite <- plus_sum; Apply sum_eq; Intros; Ring.
+unfold R_dist in H; unfold Rdiv in |- *; rewrite Rabs_mult;
+ rewrite (Rabs_right (/ sum_f_R0 An n))...
+apply Rle_lt_trans with
+ (sum_f_R0 (fun i:nat => Rabs (An (S N1 + i)%nat * (Bn (S N1 + i)%nat - l)))
+    (n - S N1) * / sum_f_R0 An n)...
+do 2 rewrite <- (Rmult_comm (/ sum_f_R0 An n)); apply Rmult_le_compat_l...
+left; apply Rinv_0_lt_compat...
+apply
+ (Rsum_abs (fun i:nat => An (S N1 + i)%nat * (Bn (S N1 + i)%nat - l))
+    (n - S N1))...
+apply Rle_lt_trans with
+ (sum_f_R0 (fun i:nat => An (S N1 + i)%nat * (eps / 2)) (n - S N1) *
+  / sum_f_R0 An n)...
+do 2 rewrite <- (Rmult_comm (/ sum_f_R0 An n)); apply Rmult_le_compat_l...
+left; apply Rinv_0_lt_compat...
+apply sum_Rle; intros; rewrite Rabs_mult;
+ pattern (An (S N1 + n0)%nat) at 2 in |- *;
+ rewrite <- (Rabs_right (An (S N1 + n0)%nat))...
+apply Rmult_le_compat_l...
+apply Rabs_pos...
+left; apply H; unfold ge in |- *; apply le_trans with (S N1);
+ [ apply le_n_Sn | apply le_plus_l ]...
+apply Rle_ge; left...
+rewrite <- (scal_sum (fun i:nat => An (S N1 + i)%nat) (n - S N1) (eps / 2));
+ unfold Rdiv in |- *; repeat rewrite Rmult_assoc; apply Rmult_lt_compat_l...
+pattern (/ 2) at 2 in |- *; rewrite <- Rmult_1_r; apply Rmult_lt_compat_l...
+apply Rinv_0_lt_compat; prove_sup...
+rewrite Rmult_comm; apply Rmult_lt_reg_l with (sum_f_R0 An n)...
+rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym...
+rewrite Rmult_1_l; rewrite Rmult_1_r; rewrite (tech2 An N1 n)...
+rewrite Rplus_comm;
+ pattern (sum_f_R0 (fun i:nat => An (S N1 + i)%nat) (n - S N1)) at 1 in |- *;
+ rewrite <- Rplus_0_r; apply Rplus_lt_compat_l...
+apply Rle_ge; left; apply Rinv_0_lt_compat...
+replace (sum_f_R0 (fun k:nat => An k * (Bn k - l)) n) with
+ (sum_f_R0 (fun k:nat => An k * Bn k) n +
+  sum_f_R0 (fun k:nat => An k * - l) n)...
+rewrite <- (scal_sum An n (- l)); field...
+rewrite <- plus_sum; apply sum_eq; intros; ring...
 Qed.
 
-Lemma Cesaro_1 : (An:nat->R;l:R) (Un_cv An l) -> (Un_cv [n:nat]``(sum_f_R0 An (pred n))/(INR n)`` l).
-Proof with Trivial.
-Intros Bn l H; Pose An := [_:nat]R1.
-Assert H0 : (n:nat) ``0<(An n)``.
-Intro; Unfold An; Apply Rlt_R0_R1.
-Assert H1 : (n:nat)``0<(sum_f_R0 An n)``.
-Intro; Apply tech1.
-Assert H2 : (cv_infty [n:nat](sum_f_R0 An n)).
-Unfold cv_infty; Intro; Case (total_order_Rle M R0); Intro.
-Exists O; Intros; Apply Rle_lt_trans with R0.
-Assert H2 : ``0<M``.
-Auto with real.
-Clear n; Pose m := (up M); Elim (archimed M); Intros; Assert H5 : `0<=m`.
-Apply le_IZR; Unfold m; Simpl; Left; Apply Rlt_trans with M.
-Elim (IZN ? H5); Intros; Exists x; Intros; Unfold An; Rewrite sum_cte; Rewrite Rmult_1l; Apply Rlt_trans with (IZR (up M)).
-Apply Rle_lt_trans with (INR x).
-Rewrite INR_IZR_INZ; Fold m; Rewrite <- H6; Right.
-Apply lt_INR; Apply le_lt_n_Sm.
-Assert H3 := (Cesaro ? ? ? H H0 H2).
-Unfold Un_cv; Unfold Un_cv in H3; Intros; Elim (H3 ? H4); Intros; Exists (S x); Intros; Unfold R_dist; Unfold R_dist in H5; Apply Rle_lt_trans with (Rabsolu (Rminus (Rdiv (sum_f_R0 [k:nat]``(An k)*(Bn k)`` (pred n)) (sum_f_R0 An (pred n))) l)).
-Right; Replace ``(sum_f_R0 Bn (pred n))/(INR n)-l`` with (Rminus (Rdiv (sum_f_R0 [k:nat]``(An k)*(Bn k)`` (pred n)) (sum_f_R0 An (pred n))) l).
-Unfold Rminus; Do 2 Rewrite <- (Rplus_sym ``-l``); Apply Rplus_plus_r.
-Unfold An; Replace (sum_f_R0 [k:nat]``1*(Bn k)`` (pred n)) with (sum_f_R0 Bn (pred n)).
-Rewrite sum_cte; Rewrite Rmult_1l; Replace (S (pred n)) with n.
-Apply S_pred with O; Apply lt_le_trans with (S x).
-Apply lt_O_Sn.
-Apply sum_eq; Intros; Ring.
-Apply H5; Unfold ge; Apply le_S_n; Replace (S (pred n)) with n.
-Apply S_pred with O; Apply lt_le_trans with (S x).
-Apply lt_O_Sn.
-Qed.
+Lemma Cesaro_1 :
+ forall (An:nat -> R) (l:R),
+   Un_cv An l -> Un_cv (fun n:nat => sum_f_R0 An (pred n) / INR n) l.
+Proof with trivial.
+intros Bn l H; pose (An := fun _:nat => 1)...
+assert (H0 : forall n:nat, 0 < An n)...
+intro; unfold An in |- *; apply Rlt_0_1...
+assert (H1 : forall n:nat, 0 < sum_f_R0 An n)...
+intro; apply tech1...
+assert (H2 : cv_infty (fun n:nat => sum_f_R0 An n))...
+unfold cv_infty in |- *; intro; case (Rle_dec M 0); intro...
+exists 0%nat; intros; apply Rle_lt_trans with 0...
+assert (H2 : 0 < M)...
+auto with real...
+clear n; pose (m := up M); elim (archimed M); intros;
+ assert (H5 : (0 <= m)%Z)...
+apply le_IZR; unfold m in |- *; simpl in |- *; left; apply Rlt_trans with M...
+elim (IZN _ H5); intros; exists x; intros; unfold An in |- *; rewrite sum_cte;
+ rewrite Rmult_1_l; apply Rlt_trans with (IZR (up M))...
+apply Rle_lt_trans with (INR x)...
+rewrite INR_IZR_INZ; fold m in |- *; rewrite <- H6; right...
+apply lt_INR; apply le_lt_n_Sm...
+assert (H3 := Cesaro _ _ _ H H0 H2)...
+unfold Un_cv in |- *; unfold Un_cv in H3; intros; elim (H3 _ H4); intros;
+ exists (S x); intros; unfold R_dist in |- *; unfold R_dist in H5;
+ apply Rle_lt_trans with
+  (Rabs
+     (sum_f_R0 (fun k:nat => An k * Bn k) (pred n) / sum_f_R0 An (pred n) - l))...
+right;
+ replace (sum_f_R0 Bn (pred n) / INR n - l) with
+  (sum_f_R0 (fun k:nat => An k * Bn k) (pred n) / sum_f_R0 An (pred n) - l)...
+unfold Rminus in |- *; do 2 rewrite <- (Rplus_comm (- l));
+ apply Rplus_eq_compat_l...
+unfold An in |- *;
+ replace (sum_f_R0 (fun k:nat => 1 * Bn k) (pred n)) with
+  (sum_f_R0 Bn (pred n))...
+rewrite sum_cte; rewrite Rmult_1_l; replace (S (pred n)) with n...
+apply S_pred with 0%nat; apply lt_le_trans with (S x)...
+apply lt_O_Sn...
+apply sum_eq; intros; ring...
+apply H5; unfold ge in |- *; apply le_S_n; replace (S (pred n)) with n...
+apply S_pred with 0%nat; apply lt_le_trans with (S x)...
+apply lt_O_Sn...
+Qed.
\ No newline at end of file