proposition: Lemma conv_zero_fun_series_IR : fun_series_convergent_IR J (fun n => [-C-][0]).
proof: Proof. apply conv_fun_const_series_IR with (x := fun n : nat => ZeroR). apply conv_zero_series. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions