proposition: Lemma powRrM x y z : x `^ (y * z) = (x `^ y) `^ z.
proof: Proof. rewrite /powR mulf_eq0; have [_|xN0] := eqVneq x 0. by case: (y == 0); rewrite ?eqxx//= oner_eq0 ln1 mulr0 expR0. by rewrite expR_eq0 expRK mulrCA mulrA. 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