proposition: Lemma Exp_increasing n x y : 1 < n -> x < y -> Exp n x < Exp n y.
proof: Proof. move=> ? ?; apply/exp_increasing/ltR_pmul2r => //; exact/ln_pos. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext