proposition: Lemma exp_le_inv x y : exp x <= exp y -> x <= y.
proof: Proof. case/Rle_lt_or_eq_dec; [move/exp_lt_inv => ?; exact/ltRW | move/exp_inv => ->]. by apply/RleP; rewrite lexx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext