proposition: Lemma derive_pt_diff_xlnx x (Hx : 0 < x < 1) : derive_pt diff_xlnx x (derivable_pt_diff_xlnx Hx) = -(2 + ln (x * (1-x))).
proof: Proof. rewrite derive_pt_plus derive_pt_opp derive_pt_xlnx; last by apply Hx. rewrite derive_pt_comp derive_pt_plus derive_pt_const. rewrite derive_pt_xlnx /=; last first. rewrite subR_gt0; by case: Hx. rewrite add0R ln_mult; first field. - by apply Hx. - rewrite subR_gt0; by case: Hx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex