proposition: Lemma derive_pt_xlnx_delta eps (Heps : 0 < eps < 1) x (Hx : 0 < x < 1 - eps) : derive_pt (xlnx_delta eps) x (derivable_xlnx_delta Heps Hx) = ln (x + eps) - ln x.
proof: Proof. rewrite derive_pt_minus derive_pt_comp derive_pt_plus derive_pt_id. rewrite derive_pt_const derive_pt_xlnx; last first. apply addR_gt0; by [apply Hx | apply Heps]. rewrite derive_pt_xlnx ; by [field | apply Hx]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex