proposition: Lemma expRMm n x : expR (n%:R * x) = expR x ^+ n.
proof: Proof. elim: n x => [x|n IH x] /=; first by rewrite mul0r expr0 expR0. by rewrite exprS -nat1r mulrDl mul1r expRD IH. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(boolp classical_sets functions) mathcomp(mathcomp_extra) reals ereal signed topology normedtype landau sequences derive realfun itv convex