proposition: Lemma Lim_f_p_infty : is_lim f p_infty 0.
proof: Proof. apply is_lim_ext_loc with (fun x => 2 / x + 2 * (ln x / x)). exists 0. move => y Hy. rewrite /f /fab. field. by apply Rgt_not_eq. eapply is_lim_plus. apply is_lim_scal_l. apply is_lim_inv. by apply is_lim_id. by []. apply is_lim_scal_l. by apply is_lim_div_ln_p. unfold is_Rbar_plus, Rbar_plus' ; apply f_equal, f_equal ; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)