proposition: Lemma xlnx_sdecreasing_0_Rinv_e x y : 0 <= x <= exp (-1) -> 0 <= y <= exp (-1) -> x < y -> xlnx y < xlnx x.
proof: Proof. move=> [x1 x2] [y1 y2] xy. case/boolP : (x == 0) => [/eqP ->|x0]. - rewrite xlnx_0; apply xlnx_neg. exact: (conj (@leR_ltR_trans x _ _ _ _) (leR_ltR_trans y2 ltRinve1)). - rewrite -[X in _ < X]oppRK ltR_oppr. have {}x0 : 0 < x by apply/RltP; rewrite lt0r x0; exact/RleP. have {x1 y1}y0 : 0 < y by exact: (@ltR_trans x). exact: (pderive_increasing (exp_pos _) xlnx_sdecreasing_0_Rinv_e_helper). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex