proposition: Lemma is_lim_ln_0 : filterlim ln (at_right 0) (Rbar_locally m_infty).
proof: Proof. intros P [M HM]. exists (mkposreal (exp M) (exp_pos _)) => x /= Hx Hx0. apply HM. rewrite <- (ln_exp M). apply ln_increasing. exact Hx0. rewrite /ball /= /AbsRing_ball /= /abs /minus /plus /opp /= in Hx. rewrite -/(Rminus _ _) Rminus_0_r Rabs_pos_eq in Hx. exact Hx. now apply Rlt_le. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis