proposition: Lemma derivable_pt_diff_xlnx x (Hx : 0 < x < 1) : derivable_pt diff_xlnx x.
proof: Proof. rewrite /diff_xlnx. apply derivable_pt_plus ; last by apply derivable_pt_opp, derivable_pt_xlnx, Hx. apply (derivable_pt_comp (fun x => 1 + - x) xlnx). apply derivable_pt_plus ; first by apply derivable_pt_const. apply derivable_pt_Ropp. apply derivable_pt_xlnx. rewrite subR_gt0; by case: Hx. Defined.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex