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, 439 insertions, 328 deletions

diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v
index a76307320..6cd5fa17f 100644
--- a/theories/Reals/Cauchy_prod.v
+++ b/theories/Reals/Cauchy_prod.v
@@ -8,340 +8,451 @@
  
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
-Require Rseries.
-Require PartSum.
-V7only [ Import nat_scope. Import Z_scope. Import R_scope. ].
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import Rseries.
+Require Import PartSum.
 Open Local Scope R_scope.
 
 (**********)
-Lemma sum_N_predN : (An:nat->R;N:nat) (lt O N) -> (sum_f_R0 An N)==``(sum_f_R0 An (pred N)) + (An N)``.
-Intros.
-Replace N with (S (pred N)).
-Rewrite tech5.
-Reflexivity.
-Symmetry; Apply S_pred with O; Assumption.
+Lemma sum_N_predN :
+ forall (An:nat -> R) (N:nat),
+   (0 < N)%nat -> sum_f_R0 An N = sum_f_R0 An (pred N) + An N.
+intros.
+replace N with (S (pred N)).
+rewrite tech5.
+reflexivity.
+symmetry  in |- *; apply S_pred with 0%nat; assumption.
 Qed.
 
 (**********)
-Lemma sum_plus : (An,Bn:nat->R;N:nat) (sum_f_R0 [l:nat]``(An l)+(Bn l)`` N)==``(sum_f_R0 An N)+(sum_f_R0 Bn N)``.
-Intros.
-Induction N.
-Reflexivity.
-Do 3 Rewrite tech5.
-Rewrite HrecN; Ring.
+Lemma sum_plus :
+ forall (An Bn:nat -> R) (N:nat),
+   sum_f_R0 (fun l:nat => An l + Bn l) N = sum_f_R0 An N + sum_f_R0 Bn N.
+intros.
+induction  N as [| N HrecN].
+reflexivity.
+do 3 rewrite tech5.
+rewrite HrecN; ring.
 Qed.
 
 (* The main result *)
-Theorem cauchy_finite : (An,Bn:nat->R;N:nat) (lt O N) -> (Rmult (sum_f_R0 An N) (sum_f_R0 Bn N)) == (Rplus (sum_f_R0 [k:nat](sum_f_R0 [p:nat]``(An p)*(Bn (minus k p))`` k) N) (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (plus l k)))*(Bn (minus N l))`` (pred (minus N k))) (pred N))). 
-Intros; Induction N.
-Elim (lt_n_n ? H).
-Cut N=O\/(lt O N).
-Intro; Elim H0; Intro.
-Rewrite H1; Simpl; Ring.
-Replace (pred (S N)) with (S (pred N)).
-Do 5 Rewrite tech5.
-Rewrite Rmult_Rplus_distrl; Rewrite Rmult_Rplus_distr; Rewrite (HrecN H1).
-Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r.
-Replace (pred (minus (S N) (S (pred N)))) with (O).
-Rewrite Rmult_Rplus_distr; Replace (sum_f_R0 [l:nat]``(An (S (plus l (S (pred N)))))*(Bn (minus (S N) l))`` O) with ``(An (S N))*(Bn (S N))``.
-Repeat Rewrite <- Rplus_assoc; Do 2 Rewrite <- (Rplus_sym ``(An (S N))*(Bn (S N))``); Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r.
-Rewrite <- minus_n_n; Cut N=(1)\/(le (2) N).
-Intro; Elim H2; Intro.
-Rewrite H3; Simpl; Ring.
-Replace (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (plus l k)))*(Bn (minus N l))`` (pred (minus N k))) (pred N)) with (Rplus (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (pred (minus N k)))) (pred (pred N))) (sum_f_R0 [l:nat]``(An (S l))*(Bn (minus N l))`` (pred N))).
-Replace (sum_f_R0 [p:nat]``(An p)*(Bn (minus (S N) p))`` N) with (Rplus (sum_f_R0 [l:nat]``(An (S l))*(Bn (minus N l))`` (pred N)) ``(An O)*(Bn (S N))``).
-Repeat Rewrite <- Rplus_assoc; Rewrite <- (Rplus_sym (sum_f_R0 [l:nat]``(An (S l))*(Bn (minus N l))`` (pred N))); Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r.
-Replace (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (plus l k)))*(Bn (minus (S N) l))`` (pred (minus (S N) k))) (pred N)) with (Rplus (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) (pred N)) (Rmult (Bn (S N)) (sum_f_R0 [l:nat](An (S l)) (pred N)))).
-Rewrite (decomp_sum An N H1); Rewrite Rmult_Rplus_distrl; Repeat Rewrite <- Rplus_assoc; Rewrite <- (Rplus_sym ``(An O)*(Bn (S N))``); Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r.
-Repeat Rewrite <- Rplus_assoc; Rewrite <- (Rplus_sym (Rmult (sum_f_R0 [i:nat](An (S i)) (pred N)) (Bn (S N)))); Rewrite <- (Rplus_sym (Rmult (Bn (S N)) (sum_f_R0 [i:nat](An (S i)) (pred N)))); Rewrite (Rmult_sym (Bn (S N))); Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r.
-Replace (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) (pred N)) with (Rplus (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (pred (minus N k)))) (pred (pred N))) (Rmult (An (S N)) (sum_f_R0 [l:nat](Bn (S l)) (pred N)))).
-Rewrite (decomp_sum Bn N H1); Rewrite Rmult_Rplus_distr.
-Pose Z := (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (pred (minus N k)))) (pred (pred N))); Pose Z2 := (sum_f_R0 [i:nat](Bn (S i)) (pred N)); Ring.
-Rewrite (sum_N_predN [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) (pred N)).
-Replace (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) (pred (pred N))) with (sum_f_R0 [k:nat](Rplus (sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (pred (minus N k)))) ``(An (S N))*(Bn (S k))``) (pred (pred N))).
-Rewrite (sum_plus [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (pred (minus N k)))) [k:nat]``(An (S N))*(Bn (S k))`` (pred (pred N))).
-Repeat Rewrite Rplus_assoc; Apply Rplus_plus_r.
-Replace (pred (minus N (pred N))) with O.
-Simpl; Rewrite <- minus_n_O.
-Replace (S (pred N)) with N.
-Replace (sum_f_R0 [k:nat]``(An (S N))*(Bn (S k))`` (pred (pred N))) with (sum_f_R0 [k:nat]``(Bn (S k))*(An (S N))`` (pred (pred N))).
-Rewrite <- (scal_sum [l:nat](Bn (S l)) (pred (pred N)) (An (S N))); Rewrite (sum_N_predN [l:nat](Bn (S l)) (pred N)).
-Replace (S (pred N)) with N.
-Ring.
-Apply S_pred with O; Assumption.
-Apply lt_pred; Apply lt_le_trans with (2); [Apply lt_n_Sn | Assumption].
-Apply sum_eq; Intros; Apply Rmult_sym.
-Apply S_pred with O; Assumption.
-Replace (minus N (pred N)) with (1).
-Reflexivity.
-Pattern 1 N; Replace N with (S (pred N)).
-Rewrite <- minus_Sn_m.
-Rewrite <- minus_n_n; Reflexivity.
-Apply le_n.
-Symmetry; Apply S_pred with O; Assumption.
-Apply sum_eq; Intros; Rewrite (sum_N_predN [l:nat]``(An (S (S (plus l i))))*(Bn (minus N l))`` (pred (minus N i))).
-Replace (S (S (plus (pred (minus N i)) i))) with (S N).
-Replace (minus N (pred (minus N i))) with (S i).
-Ring.
-Rewrite pred_of_minus; Apply INR_eq; Repeat Rewrite minus_INR.
-Rewrite S_INR; Ring.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_trans with (pred N); Apply le_pred_n.
-Apply INR_le; Rewrite minus_INR.
-Apply Rle_anti_compatibility with ``(INR i)-1``.
-Replace ``(INR i)-1+(INR (S O))`` with (INR i); [Idtac | Ring].
-Replace ``(INR i)-1+((INR N)-(INR i))`` with ``(INR N)-(INR (S O))``; [Idtac | Ring].
-Rewrite <- minus_INR.
-Apply le_INR; Apply le_trans with (pred (pred N)).
-Assumption.
-Rewrite <- pred_of_minus; Apply le_pred_n.
-Apply le_trans with (2).
-Apply le_n_Sn.
-Assumption.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_trans with (pred N); Apply le_pred_n.
-Rewrite <- pred_of_minus.
-Apply le_trans with (pred N).
-Apply le_S_n.
-Replace (S (pred N)) with N.
-Replace (S (pred (minus N i))) with (minus N i).
-Apply simpl_le_plus_l with i; Rewrite le_plus_minus_r.
-Apply le_plus_r.
-Apply le_trans with (pred (pred N)); [Assumption | Apply le_trans with (pred N); Apply le_pred_n].
-Apply S_pred with O.
-Apply simpl_lt_plus_l with i; Rewrite le_plus_minus_r.
-Replace (plus i O) with i; [Idtac | Ring].
-Apply le_lt_trans with (pred (pred N)); [Assumption | Apply lt_trans with (pred N); Apply lt_pred_n_n].
-Apply lt_S_n.
-Replace (S (pred N)) with N.
-Apply lt_le_trans with (2).
-Apply lt_n_Sn.
-Assumption.
-Apply S_pred with O; Assumption.
-Assumption.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_trans with (pred N); Apply le_pred_n.
-Apply S_pred with O; Assumption.
-Apply le_pred_n.
-Apply INR_eq; Rewrite pred_of_minus; Do 3 Rewrite S_INR; Rewrite plus_INR; Repeat Rewrite minus_INR.
-Ring.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_trans with (pred N); Apply le_pred_n.
-Apply INR_le.
-Rewrite minus_INR.
-Apply Rle_anti_compatibility with ``(INR i)-1``.
-Replace ``(INR i)-1+(INR (S O))`` with (INR i); [Idtac | Ring].
-Replace ``(INR i)-1+((INR N)-(INR i))`` with ``(INR N)-(INR (S O))``; [Idtac | Ring].
-Rewrite <- minus_INR.
-Apply le_INR.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Rewrite <- pred_of_minus.
-Apply le_pred_n.
-Apply le_trans with (2).
-Apply le_n_Sn.
-Assumption.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_trans with (pred N); Apply le_pred_n.
-Apply lt_le_trans with (1).
-Apply lt_O_Sn.
-Apply INR_le.
-Rewrite pred_of_minus.
-Repeat Rewrite minus_INR.
-Apply Rle_anti_compatibility with ``(INR i)-1``.
-Replace ``(INR i)-1+(INR (S O))`` with (INR i); [Idtac | Ring].
-Replace ``(INR i)-1+((INR N)-(INR i)-(INR (S O)))`` with ``(INR N)-(INR (S O)) -(INR (S O))``.
-Repeat Rewrite <- minus_INR.
-Apply le_INR.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Do 2 Rewrite <- pred_of_minus.
-Apply le_n.
-Apply simpl_le_plus_l with (1).
-Rewrite le_plus_minus_r.
-Simpl; Assumption.
-Apply le_trans with (2); [Apply le_n_Sn | Assumption].
-Apply le_trans with (2); [Apply le_n_Sn | Assumption].
-Ring.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_trans with (pred N); Apply le_pred_n.
-Apply simpl_le_plus_l with i.
-Rewrite le_plus_minus_r.
-Replace (plus i (1)) with (S i).
-Replace N with (S (pred N)).
-Apply le_n_S.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_pred_n.
-Symmetry; Apply S_pred with O; Assumption.
-Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Reflexivity.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_trans with (pred N); Apply le_pred_n.
-Apply lt_le_trans with (1).
-Apply lt_O_Sn.
-Apply le_S_n.
-Replace (S (pred N)) with N.
-Assumption.
-Apply S_pred with O; Assumption.
-Replace (sum_f_R0 [k:nat](sum_f_R0 [l:nat]``(An (S (plus l k)))*(Bn (minus (S N) l))`` (pred (minus (S N) k))) (pred N)) with (sum_f_R0 [k:nat](Rplus (sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) ``(An (S k))*(Bn (S N))``) (pred N)).
-Rewrite (sum_plus [k:nat](sum_f_R0 [l:nat]``(An (S (S (plus l k))))*(Bn (minus N l))`` (pred (minus N k))) [k:nat]``(An (S k))*(Bn (S N))``).
-Apply Rplus_plus_r.
-Rewrite scal_sum; Reflexivity.
-Apply sum_eq; Intros; Rewrite Rplus_sym; Rewrite (decomp_sum [l:nat]``(An (S (plus l i)))*(Bn (minus (S N) l))`` (pred (minus (S N) i))).
-Replace (plus O i) with i; [Idtac | Ring].
-Rewrite <- minus_n_O; Apply Rplus_plus_r.
-Replace (pred (pred (minus (S N) i))) with (pred (minus N i)).
-Apply sum_eq; Intros.
-Replace (minus (S N) (S i0)) with (minus N i0); [Idtac | Reflexivity].
-Replace (plus (S i0) i) with (S (plus i0 i)).
-Reflexivity.
-Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring.
-Cut (minus N i)=(pred (minus (S N) i)).
-Intro; Rewrite H5; Reflexivity.
-Rewrite pred_of_minus.
-Apply INR_eq; Repeat Rewrite minus_INR.
-Rewrite S_INR; Ring.
-Apply le_trans with N.
-Apply le_trans with (pred N).
-Assumption.
-Apply le_pred_n.
-Apply le_n_Sn.
-Apply simpl_le_plus_l with i.
-Rewrite le_plus_minus_r.
-Replace (plus i (1)) with (S i).
-Apply le_n_S.
-Apply le_trans with (pred N).
-Assumption.
-Apply le_pred_n.
-Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Ring.
-Apply le_trans with N.
-Apply le_trans with (pred N).
-Assumption.
-Apply le_pred_n.
-Apply le_n_Sn.
-Apply le_trans with (pred N).
-Assumption.
-Apply le_pred_n.
-Replace (pred (minus (S N) i)) with (minus (S N) (S i)).
-Replace (minus (S N) (S i)) with (minus N i); [Idtac | Reflexivity].
-Apply simpl_lt_plus_l with i.
-Rewrite le_plus_minus_r.
-Replace (plus i O) with i; [Idtac | Ring].
-Apply le_lt_trans with (pred N).
-Assumption.
-Apply lt_pred_n_n.
-Assumption.
-Apply le_trans with (pred N).
-Assumption.
-Apply le_pred_n.
-Rewrite pred_of_minus.
-Apply INR_eq; Repeat Rewrite minus_INR.
-Repeat Rewrite S_INR; Ring.
-Apply le_trans with N.
-Apply le_trans with (pred N).
-Assumption.
-Apply le_pred_n.
-Apply le_n_Sn.
-Apply simpl_le_plus_l with i.
-Rewrite le_plus_minus_r.
-Replace (plus i (1)) with (S i).
-Apply le_n_S.
-Apply le_trans with (pred N).
-Assumption.
-Apply le_pred_n.
-Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Ring.
-Apply le_trans with N.
-Apply le_trans with (pred N).
-Assumption.
-Apply le_pred_n.
-Apply le_n_Sn.
-Apply le_n_S.
-Apply le_trans with (pred N).
-Assumption.
-Apply le_pred_n.
-Rewrite Rplus_sym.
-Rewrite (decomp_sum [p:nat]``(An p)*(Bn (minus (S N) p))`` N).
-Rewrite <- minus_n_O.
-Apply Rplus_plus_r.
-Apply sum_eq; Intros.
-Reflexivity.
-Assumption.
-Rewrite Rplus_sym.
-Rewrite (decomp_sum [k:nat](sum_f_R0 [l:nat]``(An (S (plus l k)))*(Bn (minus N l))`` (pred (minus N k))) (pred N)).
-Rewrite <- minus_n_O.
-Replace (sum_f_R0 [l:nat]``(An (S (plus l O)))*(Bn (minus N l))`` (pred N)) with (sum_f_R0 [l:nat]``(An (S l))*(Bn (minus N l))`` (pred N)).
-Apply Rplus_plus_r.
-Apply sum_eq; Intros.
-Replace (pred (minus N (S i))) with (pred (pred (minus N i))).
-Apply sum_eq; Intros.
-Replace (plus i0 (S i)) with (S (plus i0 i)).
-Reflexivity.
-Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Rewrite S_INR; Ring.
-Cut (pred (minus N i))=(minus N (S i)).
-Intro; Rewrite H5; Reflexivity.
-Rewrite pred_of_minus.
-Apply INR_eq.
-Repeat Rewrite minus_INR.
-Repeat Rewrite S_INR; Ring.
-Apply le_trans with (S (pred (pred N))).
-Apply le_n_S; Assumption.
-Replace (S (pred (pred N))) with (pred N).
-Apply le_pred_n.
-Apply S_pred with O.
-Apply lt_S_n.
-Replace (S (pred N)) with N.
-Apply lt_le_trans with (2).
-Apply lt_n_Sn.
-Assumption.
-Apply S_pred with O; Assumption.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_trans with (pred N); Apply le_pred_n.
-Apply simpl_le_plus_l with i.
-Rewrite le_plus_minus_r.
-Replace (plus i (1)) with (S i).
-Replace N with (S (pred N)).
-Apply le_n_S.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_pred_n.
-Symmetry; Apply S_pred with O; Assumption.
-Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Ring.
-Apply le_trans with (pred (pred N)).
-Assumption.
-Apply le_trans with (pred N); Apply le_pred_n.
-Apply sum_eq; Intros.
-Replace (plus i O) with i; [Reflexivity | Trivial].
-Apply lt_S_n.
-Replace (S (pred N)) with N.
-Apply lt_le_trans with (2); [Apply lt_n_Sn | Assumption].
-Apply S_pred with O; Assumption.
-Inversion H1.
-Left; Reflexivity.
-Right; Apply le_n_S; Assumption.
-Simpl.
-Replace (S (pred N)) with N.
-Reflexivity.
-Apply S_pred with O; Assumption.
-Simpl.
-Cut (minus N (pred N))=(1).
-Intro; Rewrite H2; Reflexivity.
-Rewrite pred_of_minus.
-Apply INR_eq; Repeat Rewrite minus_INR.
-Ring.
-Apply lt_le_S; Assumption.
-Rewrite <- pred_of_minus; Apply le_pred_n.
-Simpl; Symmetry; Apply S_pred with O; Assumption.
-Inversion H.
-Left; Reflexivity.
-Right; Apply lt_le_trans with (1); [Apply lt_n_Sn | Exact H1].
-Qed.
+Theorem cauchy_finite :
+ forall (An Bn:nat -> R) (N:nat),
+   (0 < N)%nat ->
+   sum_f_R0 An N * sum_f_R0 Bn N =
+   sum_f_R0 (fun k:nat => sum_f_R0 (fun p:nat => An p * Bn (k - p)%nat) k) N +
+   sum_f_R0
+     (fun k:nat =>
+        sum_f_R0 (fun l:nat => An (S (l + k)) * Bn (N - l)%nat)
+          (pred (N - k))) (pred N). 
+intros; induction  N as [| N HrecN].
+elim (lt_irrefl _ H).
+cut (N = 0%nat \/ (0 < N)%nat).
+intro; elim H0; intro.
+rewrite H1; simpl in |- *; ring.
+replace (pred (S N)) with (S (pred N)).
+do 5 rewrite tech5.
+rewrite Rmult_plus_distr_r; rewrite Rmult_plus_distr_l; rewrite (HrecN H1).
+repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l.
+replace (pred (S N - S (pred N))) with 0%nat.
+rewrite Rmult_plus_distr_l;
+ replace
+  (sum_f_R0 (fun l:nat => An (S (l + S (pred N))) * Bn (S N - l)%nat) 0) with
+  (An (S N) * Bn (S N)).
+repeat rewrite <- Rplus_assoc;
+ do 2 rewrite <- (Rplus_comm (An (S N) * Bn (S N)));
+ repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l.
+rewrite <- minus_n_n; cut (N = 1%nat \/ (2 <= N)%nat).
+intro; elim H2; intro.
+rewrite H3; simpl in |- *; ring.
+replace
+ (sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (l + k)) * Bn (N - l)%nat) (pred (N - k)))
+    (pred N)) with
+ (sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (pred (N - k)))) (pred (pred N)) +
+  sum_f_R0 (fun l:nat => An (S l) * Bn (N - l)%nat) (pred N)).
+replace (sum_f_R0 (fun p:nat => An p * Bn (S N - p)%nat) N) with
+ (sum_f_R0 (fun l:nat => An (S l) * Bn (N - l)%nat) (pred N) +
+  An 0%nat * Bn (S N)).
+repeat rewrite <- Rplus_assoc;
+ rewrite <-
+  (Rplus_comm (sum_f_R0 (fun l:nat => An (S l) * Bn (N - l)%nat) (pred N)))
+  ; repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l.
+replace
+ (sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (l + k)) * Bn (S N - l)%nat)
+         (pred (S N - k))) (pred N)) with
+ (sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (N - k))) (pred N) +
+  Bn (S N) * sum_f_R0 (fun l:nat => An (S l)) (pred N)).
+rewrite (decomp_sum An N H1); rewrite Rmult_plus_distr_r;
+ repeat rewrite <- Rplus_assoc; rewrite <- (Rplus_comm (An 0%nat * Bn (S N)));
+ repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l.
+repeat rewrite <- Rplus_assoc;
+ rewrite <-
+  (Rplus_comm (sum_f_R0 (fun i:nat => An (S i)) (pred N) * Bn (S N)))
+  ;
+ rewrite <-
+  (Rplus_comm (Bn (S N) * sum_f_R0 (fun i:nat => An (S i)) (pred N)))
+  ; rewrite (Rmult_comm (Bn (S N))); repeat rewrite Rplus_assoc;
+ apply Rplus_eq_compat_l.
+replace
+ (sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (N - k))) (pred N)) with
+ (sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (pred (N - k)))) (pred (pred N)) +
+  An (S N) * sum_f_R0 (fun l:nat => Bn (S l)) (pred N)).
+rewrite (decomp_sum Bn N H1); rewrite Rmult_plus_distr_l.
+pose
+ (Z :=
+  sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (pred (N - k)))) (pred (pred N)));
+ pose (Z2 := sum_f_R0 (fun i:nat => Bn (S i)) (pred N)); 
+ ring.
+rewrite
+ (sum_N_predN
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (N - k))) (pred N)).
+replace
+ (sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (N - k))) (pred (pred N))) with
+ (sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (pred (N - k))) + An (S N) * Bn (S k)) (
+    pred (pred N))).
+rewrite
+ (sum_plus
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (pred (N - k)))) (fun k:nat => An (S N) * Bn (S k))
+    (pred (pred N))).
+repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l.
+replace (pred (N - pred N)) with 0%nat.
+simpl in |- *; rewrite <- minus_n_O.
+replace (S (pred N)) with N.
+replace (sum_f_R0 (fun k:nat => An (S N) * Bn (S k)) (pred (pred N))) with
+ (sum_f_R0 (fun k:nat => Bn (S k) * An (S N)) (pred (pred N))).
+rewrite <- (scal_sum (fun l:nat => Bn (S l)) (pred (pred N)) (An (S N)));
+ rewrite (sum_N_predN (fun l:nat => Bn (S l)) (pred N)).
+replace (S (pred N)) with N.
+ring.
+apply S_pred with 0%nat; assumption.
+apply lt_pred; apply lt_le_trans with 2%nat; [ apply lt_n_Sn | assumption ].
+apply sum_eq; intros; apply Rmult_comm.
+apply S_pred with 0%nat; assumption.
+replace (N - pred N)%nat with 1%nat.
+reflexivity.
+pattern N at 1 in |- *; replace N with (S (pred N)).
+rewrite <- minus_Sn_m.
+rewrite <- minus_n_n; reflexivity.
+apply le_n.
+symmetry  in |- *; apply S_pred with 0%nat; assumption.
+apply sum_eq; intros;
+ rewrite
+  (sum_N_predN (fun l:nat => An (S (S (l + i))) * Bn (N - l)%nat)
+     (pred (N - i))).
+replace (S (S (pred (N - i) + i))) with (S N).
+replace (N - pred (N - i))%nat with (S i).
+ring.
+rewrite pred_of_minus; apply INR_eq; repeat rewrite minus_INR.
+rewrite S_INR; ring.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_trans with (pred N); apply le_pred_n.
+apply INR_le; rewrite minus_INR.
+apply Rplus_le_reg_l with (INR i - 1).
+replace (INR i - 1 + INR 1) with (INR i); [ idtac | ring ].
+replace (INR i - 1 + (INR N - INR i)) with (INR N - INR 1); [ idtac | ring ].
+rewrite <- minus_INR.
+apply le_INR; apply le_trans with (pred (pred N)).
+assumption.
+rewrite <- pred_of_minus; apply le_pred_n.
+apply le_trans with 2%nat.
+apply le_n_Sn.
+assumption.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_trans with (pred N); apply le_pred_n.
+rewrite <- pred_of_minus.
+apply le_trans with (pred N).
+apply le_S_n.
+replace (S (pred N)) with N.
+replace (S (pred (N - i))) with (N - i)%nat.
+apply (fun p n m:nat => plus_le_reg_l n m p) with i; rewrite le_plus_minus_r.
+apply le_plus_r.
+apply le_trans with (pred (pred N));
+ [ assumption | apply le_trans with (pred N); apply le_pred_n ].
+apply S_pred with 0%nat.
+apply plus_lt_reg_l with i; rewrite le_plus_minus_r.
+replace (i + 0)%nat with i; [ idtac | ring ].
+apply le_lt_trans with (pred (pred N));
+ [ assumption | apply lt_trans with (pred N); apply lt_pred_n_n ].
+apply lt_S_n.
+replace (S (pred N)) with N.
+apply lt_le_trans with 2%nat.
+apply lt_n_Sn.
+assumption.
+apply S_pred with 0%nat; assumption.
+assumption.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_trans with (pred N); apply le_pred_n.
+apply S_pred with 0%nat; assumption.
+apply le_pred_n.
+apply INR_eq; rewrite pred_of_minus; do 3 rewrite S_INR; rewrite plus_INR;
+ repeat rewrite minus_INR.
+ring.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_trans with (pred N); apply le_pred_n.
+apply INR_le.
+rewrite minus_INR.
+apply Rplus_le_reg_l with (INR i - 1).
+replace (INR i - 1 + INR 1) with (INR i); [ idtac | ring ].
+replace (INR i - 1 + (INR N - INR i)) with (INR N - INR 1); [ idtac | ring ].
+rewrite <- minus_INR.
+apply le_INR.
+apply le_trans with (pred (pred N)).
+assumption.
+rewrite <- pred_of_minus.
+apply le_pred_n.
+apply le_trans with 2%nat.
+apply le_n_Sn.
+assumption.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_trans with (pred N); apply le_pred_n.
+apply lt_le_trans with 1%nat.
+apply lt_O_Sn.
+apply INR_le.
+rewrite pred_of_minus.
+repeat rewrite minus_INR.
+apply Rplus_le_reg_l with (INR i - 1).
+replace (INR i - 1 + INR 1) with (INR i); [ idtac | ring ].
+replace (INR i - 1 + (INR N - INR i - INR 1)) with (INR N - INR 1 - INR 1).
+repeat rewrite <- minus_INR.
+apply le_INR.
+apply le_trans with (pred (pred N)).
+assumption.
+do 2 rewrite <- pred_of_minus.
+apply le_n.
+apply (fun p n m:nat => plus_le_reg_l n m p) with 1%nat.
+rewrite le_plus_minus_r.
+simpl in |- *; assumption.
+apply le_trans with 2%nat; [ apply le_n_Sn | assumption ].
+apply le_trans with 2%nat; [ apply le_n_Sn | assumption ].
+ring.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_trans with (pred N); apply le_pred_n.
+apply (fun p n m:nat => plus_le_reg_l n m p) with i.
+rewrite le_plus_minus_r.
+replace (i + 1)%nat with (S i).
+replace N with (S (pred N)).
+apply le_n_S.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_pred_n.
+symmetry  in |- *; apply S_pred with 0%nat; assumption.
+apply INR_eq; rewrite S_INR; rewrite plus_INR; reflexivity.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_trans with (pred N); apply le_pred_n.
+apply lt_le_trans with 1%nat.
+apply lt_O_Sn.
+apply le_S_n.
+replace (S (pred N)) with N.
+assumption.
+apply S_pred with 0%nat; assumption.
+replace
+ (sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (l + k)) * Bn (S N - l)%nat)
+         (pred (S N - k))) (pred N)) with
+ (sum_f_R0
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (N - k)) + An (S k) * Bn (S N)) (pred N)).
+rewrite
+ (sum_plus
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (S (l + k))) * Bn (N - l)%nat)
+         (pred (N - k))) (fun k:nat => An (S k) * Bn (S N)))
+ .
+apply Rplus_eq_compat_l.
+rewrite scal_sum; reflexivity.
+apply sum_eq; intros; rewrite Rplus_comm;
+ rewrite
+  (decomp_sum (fun l:nat => An (S (l + i)) * Bn (S N - l)%nat)
+     (pred (S N - i))).
+replace (0 + i)%nat with i; [ idtac | ring ].
+rewrite <- minus_n_O; apply Rplus_eq_compat_l.
+replace (pred (pred (S N - i))) with (pred (N - i)).
+apply sum_eq; intros.
+replace (S N - S i0)%nat with (N - i0)%nat; [ idtac | reflexivity ].
+replace (S i0 + i)%nat with (S (i0 + i)).
+reflexivity.
+apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring.
+cut ((N - i)%nat = pred (S N - i)).
+intro; rewrite H5; reflexivity.
+rewrite pred_of_minus.
+apply INR_eq; repeat rewrite minus_INR.
+rewrite S_INR; ring.
+apply le_trans with N.
+apply le_trans with (pred N).
+assumption.
+apply le_pred_n.
+apply le_n_Sn.
+apply (fun p n m:nat => plus_le_reg_l n m p) with i.
+rewrite le_plus_minus_r.
+replace (i + 1)%nat with (S i).
+apply le_n_S.
+apply le_trans with (pred N).
+assumption.
+apply le_pred_n.
+apply INR_eq; rewrite S_INR; rewrite plus_INR; ring.
+apply le_trans with N.
+apply le_trans with (pred N).
+assumption.
+apply le_pred_n.
+apply le_n_Sn.
+apply le_trans with (pred N).
+assumption.
+apply le_pred_n.
+replace (pred (S N - i)) with (S N - S i)%nat.
+replace (S N - S i)%nat with (N - i)%nat; [ idtac | reflexivity ].
+apply plus_lt_reg_l with i.
+rewrite le_plus_minus_r.
+replace (i + 0)%nat with i; [ idtac | ring ].
+apply le_lt_trans with (pred N).
+assumption.
+apply lt_pred_n_n.
+assumption.
+apply le_trans with (pred N).
+assumption.
+apply le_pred_n.
+rewrite pred_of_minus.
+apply INR_eq; repeat rewrite minus_INR.
+repeat rewrite S_INR; ring.
+apply le_trans with N.
+apply le_trans with (pred N).
+assumption.
+apply le_pred_n.
+apply le_n_Sn.
+apply (fun p n m:nat => plus_le_reg_l n m p) with i.
+rewrite le_plus_minus_r.
+replace (i + 1)%nat with (S i).
+apply le_n_S.
+apply le_trans with (pred N).
+assumption.
+apply le_pred_n.
+apply INR_eq; rewrite S_INR; rewrite plus_INR; ring.
+apply le_trans with N.
+apply le_trans with (pred N).
+assumption.
+apply le_pred_n.
+apply le_n_Sn.
+apply le_n_S.
+apply le_trans with (pred N).
+assumption.
+apply le_pred_n.
+rewrite Rplus_comm.
+rewrite (decomp_sum (fun p:nat => An p * Bn (S N - p)%nat) N).
+rewrite <- minus_n_O.
+apply Rplus_eq_compat_l.
+apply sum_eq; intros.
+reflexivity.
+assumption.
+rewrite Rplus_comm.
+rewrite
+ (decomp_sum
+    (fun k:nat =>
+       sum_f_R0 (fun l:nat => An (S (l + k)) * Bn (N - l)%nat) (pred (N - k)))
+    (pred N)).
+rewrite <- minus_n_O.
+replace (sum_f_R0 (fun l:nat => An (S (l + 0)) * Bn (N - l)%nat) (pred N))
+ with (sum_f_R0 (fun l:nat => An (S l) * Bn (N - l)%nat) (pred N)).
+apply Rplus_eq_compat_l.
+apply sum_eq; intros.
+replace (pred (N - S i)) with (pred (pred (N - i))).
+apply sum_eq; intros.
+replace (i0 + S i)%nat with (S (i0 + i)).
+reflexivity.
+apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring.
+cut (pred (N - i) = (N - S i)%nat).
+intro; rewrite H5; reflexivity.
+rewrite pred_of_minus.
+apply INR_eq.
+repeat rewrite minus_INR.
+repeat rewrite S_INR; ring.
+apply le_trans with (S (pred (pred N))).
+apply le_n_S; assumption.
+replace (S (pred (pred N))) with (pred N).
+apply le_pred_n.
+apply S_pred with 0%nat.
+apply lt_S_n.
+replace (S (pred N)) with N.
+apply lt_le_trans with 2%nat.
+apply lt_n_Sn.
+assumption.
+apply S_pred with 0%nat; assumption.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_trans with (pred N); apply le_pred_n.
+apply (fun p n m:nat => plus_le_reg_l n m p) with i.
+rewrite le_plus_minus_r.
+replace (i + 1)%nat with (S i).
+replace N with (S (pred N)).
+apply le_n_S.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_pred_n.
+symmetry  in |- *; apply S_pred with 0%nat; assumption.
+apply INR_eq; rewrite S_INR; rewrite plus_INR; ring.
+apply le_trans with (pred (pred N)).
+assumption.
+apply le_trans with (pred N); apply le_pred_n.
+apply sum_eq; intros.
+replace (i + 0)%nat with i; [ reflexivity | trivial ].
+apply lt_S_n.
+replace (S (pred N)) with N.
+apply lt_le_trans with 2%nat; [ apply lt_n_Sn | assumption ].
+apply S_pred with 0%nat; assumption.
+inversion H1.
+left; reflexivity.
+right; apply le_n_S; assumption.
+simpl in |- *.
+replace (S (pred N)) with N.
+reflexivity.
+apply S_pred with 0%nat; assumption.
+simpl in |- *.
+cut ((N - pred N)%nat = 1%nat).
+intro; rewrite H2; reflexivity.
+rewrite pred_of_minus.
+apply INR_eq; repeat rewrite minus_INR.
+ring.
+apply lt_le_S; assumption.
+rewrite <- pred_of_minus; apply le_pred_n.
+simpl in |- *; symmetry  in |- *; apply S_pred with 0%nat; assumption.
+inversion H.
+left; reflexivity.
+right; apply lt_le_trans with 1%nat; [ apply lt_n_Sn | exact H1 ].
+Qed.
\ No newline at end of file