proposition: Lemma pow_Exp x n : 0 < x -> x ^ n = Exp x n%:R.
proof: Proof. by move=> x0; rewrite /Exp exp_pow exp_ln. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext