proposition: Lemma derivable_xlnx_delta eps (Heps : 0 < eps < 1) x (Hx : 0 < x < 1 - eps) : derivable_pt (xlnx_delta eps) x.
proof: Proof. rewrite /xlnx_delta. apply derivable_pt_minus. - apply (derivable_pt_comp (fun x => x + eps) xlnx). apply derivable_pt_plus ; first by apply derivable_pt_id. by apply derivable_pt_const. apply derivable_pt_xlnx. apply addR_gt0; by [apply Heps | apply Hx]. - by apply derivable_pt_xlnx, Hx. Defined.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex