proposition: Lemma derive_diff_xlnx_pos x (Hx : 0 < x < 1) (pr : derivable_pt diff_xlnx x) : x < exp (-2) -> 0 < derive_pt diff_xlnx x pr.
proof: Proof. rewrite (proof_derive_irrelevance _ (derivable_pt_diff_xlnx Hx)) //. exact: derive_diff_xlnx_neg_aux. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex