proposition: Lemma Fun_Series_Sum_zero : forall (H : fun_series_convergent _ _ Hab (fun n => [-C-][0])) x Hx, Fun_Series_Sum H x Hx [=] [0].
proof: Proof. intros. simpl in |- *. apply series_sum_zero. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series