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