proposition: Lemma exp_pow n : forall k, exp (k%:R * n) = (exp n) ^ k.
proof: Proof. elim => [|k IH]; first by rewrite mul0R exp_0. by rewrite S_INR mulRDl mul1R exp_plus IH mulRC. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR Reals_ext mathcomp(reals) realType_ext