proposition: 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).
proof: Proof. intros. induction N as [| N HrecN]. - simpl; 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. + ring. Qed.
imports: Rbase Rfunctions Rseries Rcomplete