proposition: Lemma fun_const_series_Sum_IR : forall y H (H' : fun_series_convergent_IR J (fun n => [-C-] (y n))) x Hx, FSeries_Sum H' x Hx [=] series_sum y H.
proof: Proof. intros. simpl in |- *. apply series_sum_wd. algebra. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions