proposition: Lemma xlnx_neg x : 0 < x < 1 -> xlnx x < 0.
proof: Proof. case => lt0x ltx1. rewrite /xlnx. have -> : (0 < x)%mcR ; first exact/RltP. rewrite -(oppRK 0) ltR_oppr oppR0 -mulRN. apply mulR_gt0 => //. rewrite ltR_oppr oppR0. apply exp_lt_inv. by rewrite exp_ln // exp_0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex