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