proposition: Lemma natRExp n : (0 < n)%nat -> forall m, Exp n%:R m%:R = (expn n m)%:R.
proof: Proof. move=> n0. elim=> [|m IH]; first by rewrite /Exp mul0R exp_0. rewrite S_INR ExpD expnS natRM IH /Exp mul1R exp_ln; [by rewrite mulRC | exact/ltR0n]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext