proposition: Lemma natRexp r n : r%:R ^ n = (expn r n)%:R.
proof: Proof. by elim: n => // n IH; rewrite (expnSr r n) natRM -addn1 pow_add /= mulR1 IH. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)