proposition: Lemma is_lim_div_ln1p_0 : is_lim (fun y => ln (1+y) / y) 0 1.
proof: Proof. apply is_lim_spec. move => eps. case: (derivable_pt_lim_ln 1 (Rlt_0_1) eps (cond_pos eps)) => delta H. exists delta => y Hy Hy0. rewrite /ball /= /AbsRing_ball /= /minus /plus /opp /= in Hy. rewrite /= -/(Rminus _ _) Rminus_0_r in Hy. move: (H y Hy0 Hy). by rewrite ln_1 Rinv_1 Rminus_0_r. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis