proposition: Lemma is_cvg_series_exp_coeff x : cvgn (series (exp x)).
proof: Proof. have [->|x0] := eqVneq x 0. apply/cvg_ex; exists 1; apply/cvgrPdist_lt => // => _/posnumP[e]. near=> n; have [m ->] : exists m, n = m.+1. by exists n.-1; rewrite prednK //; near: n; exists 1%N. by rewrite series_exp_coeff0 subrr normr0. apply: normed_cvg; rewrite normed_series_exp_coeff. by apply: is_cvg_series_exp_coeff_pos; rewrite normr_gt0. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau