proposition: Lemma is_lim_exp_p : is_lim (fun y => exp y) p_infty p_infty.
proof: Proof. apply is_lim_le_p_loc with (fun y => 1 + y). exists 0 => y Hy. by apply Rlt_le, exp_ineq1; auto with real. pattern p_infty at 2. replace p_infty with (Rbar_plus 1 p_infty) by auto. eapply is_lim_plus. apply is_lim_const. apply is_lim_id. by []. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis