proposition: Lemma scal_sum : forall (An:nat -> R) (N:nat) (x:R), x * sum_f_R0 An N = sum_f_R0 (fun i:nat => An i * x) N.
proof: Proof. intros; induction N as [| N HrecN]. - simpl; ring. - do 2 rewrite tech5. rewrite Rmult_plus_distr_l; rewrite <- HrecN; ring. Qed.
imports: Rbase Rfunctions Rseries Rcomplete