proposition: Lemma Exp_le_inv n x y : 1 < n -> Exp n x <= Exp n y -> x <= y.
proof: Proof. rewrite /Exp => n1 /exp_le_inv H. apply/RleP; rewrite -(@ler_pM2l _ (ln n)); last exact/RltP/ln_pos. by rewrite mulrC -(mulrC y); exact/RleP. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext