proposition: Lemma Lim_exp (x : Rbar) : Lim (fun y => exp y) x = match x with | Finite x => exp x | p_infty => p_infty | m_infty => 0 end.
proof: Proof. apply is_lim_unique. case: x => [x | | ]. apply is_lim_continuity. apply derivable_continuous_pt, derivable_pt_exp. by apply is_lim_exp_p. by apply is_lim_exp_m. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis