proposition: Lemma xlnx_ineq x : 0 <= x <= exp (-2) -> xlnx x <= xlnx (1-x).
proof: Proof. move=> [Hx1 Hx2]. apply Rge_le, Rminus_ge, Rle_ge. rewrite -diff_xlnx_0 -/(diff_xlnx x). case/boolP : (0 == x) => [/eqP ->|/eqP xnot0]. by apply/RleP; rewrite lexx. apply/ltRW/diff_xlnx_sincreasing_0_Rinv_e2 => //. split; [ | exact/ltRW/exp_pos]. by apply/RleP; rewrite lexx. by rewrite ltR_neqAle. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex