proposition: Lemma sum_cte : forall (x:R) (N:nat), sum_f_R0 (fun _:nat => x) N = x * INR (S N).
proof: Proof. intros. induction N as [| N HrecN]. - simpl; ring. - rewrite tech5. rewrite HrecN; repeat rewrite S_INR; ring. Qed.
imports: Rbase Rfunctions Rseries Rcomplete