proposition: Lemma Exp_le_increasing n x y : 1 < n -> x <= y -> Exp n x <= Exp n y.
proof: Proof. move=> n1; rewrite /Exp; case/Rle_lt_or_eq_dec. move/Exp_increasing => x_y; exact/ltRW/x_y. by move=> ->; apply/RleP; rewrite lexx. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext