proposition: Lemma conv_zero_fun_series : fun_series_convergent _ _ Hab (fun n => [-C-][0]).
proof: Proof. apply conv_fun_const_series with (x := fun n : nat => ZeroR). apply conv_zero_series. Qed.
imports: CoRN.ftc.FunctSequence CoRN.reals.Series