proposition: Lemma xlnx_decreasing_0_Rinv_e x y : 0 <= x <= exp (-1) -> 0 <= y <= exp (-1) -> x <= y -> xlnx y <= xlnx x.
proof: Proof. move=> Hx Hy Hxy. case/boolP : (x == y) => [/eqP ->|/eqP H]. by apply/RleP; rewrite lexx. by apply/ltRW/xlnx_sdecreasing_0_Rinv_e => //; rewrite ltR_neqAle. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex