proposition: Lemma is_lim_ln_p : is_lim (fun y => ln y) p_infty p_infty.
proof: Proof. apply is_lim_spec. move => M. exists (exp M) => x Hx. rewrite -(ln_exp M). apply ln_increasing. apply exp_pos. by apply Hx. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis