proposition: Lemma derive_diff_xlnx_neg_aux x (Hx : 0 < x < 1) : x < exp (-2) -> 0 < derive_pt diff_xlnx x (derivable_pt_diff_xlnx Hx).
proof: Proof. rewrite derive_pt_diff_xlnx; case: Hx => Hx1 Hx2 xltexp2. rewrite oppRD subR_gt0. apply exp_lt_inv. rewrite exp_ln ; last first. apply mulR_gt0 => //; by rewrite subR_gt0. apply (@ltR_trans (exp (-2) * (1 - x))). apply ltR_pmul2r => //; by rewrite ltR_subRL addR0. rewrite -{2}(mulR1 (exp (-2))). apply ltR_pmul2l; first exact: exp_pos. apply (@ltR_add2r (-1)). by rewrite addRAC -[X in _ < X](addR0 _) ltR_add2l ltR_oppl oppR0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex