proposition: Lemma ex_lim_exp (x : Rbar) : ex_lim (fun y => exp y) x.
proof: Proof. case: x => [x | | ]. apply ex_finite_lim_correct, ex_lim_continuity. apply derivable_continuous_pt, derivable_pt_exp. exists p_infty ; by apply is_lim_exp_p. exists 0 ; by apply is_lim_exp_m. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis