proposition: 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.
proof: Proof. intros. induction N as [| N HrecN]. - reflexivity. - do 3 rewrite tech5. rewrite HrecN; ring. Qed.
imports: Rbase Rfunctions Rseries PartSum