proposition: Lemma is_cvg_series_exp_coeff_pos : cvgn (series (exp x)).
proof: Proof. rewrite /series; near \oo => N; have xN : x < N%:R; last first. rewrite -(@is_cvg_series_restrict N.+1). by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; apply: S1_sup. near: N; exists (absz (floor x)).+1 => // m; rewrite /mkset -(@ler_nat R). move/lt_le_trans => -> //; rewrite (lt_le_trans (lt_succ_floor x)) // -addn1. by rewrite natrD lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW. 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