proposition: Lemma xlnx_sdecreasing_0_Rinv_e_helper : forall (t : R) (Ht : 0 < t <= exp (-1)), 0 < (if t == exp (-1) then 1 else derive_pt (fun x => - xlnx x) t (pderivable_Ropp_xlnx Ht)).
proof: Proof. move=> t [t0 te]; case: ifPn => [//|] /eqP Hcase. rewrite derive_pt_opp derive_pt_xlnx //. rewrite ltR_oppr oppR0 addRC -ltR_subRL sub0R. apply exp_lt_inv; by rewrite exp_ln // ltR_neqAle. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex