proposition: Lemma Exp_conv' : fun_series_abs_convergent_IR realline Exp_ps.
proof: Proof. unfold Exp_ps in |- *. apply FPowerSeries'_conv'. exists 0; exists OneR. apply pos_one. intros; apply eq_imp_leEq; algebra. Qed.
imports: CoRN.ftc.FTC