proposition: Lemma poweRrM x r s : x `^ (r * s) = (x `^ r) `^ s.
proof: Proof. have [->|s0] := eqVneq s 0%R; first by rewrite mulr0 !poweRe0. have [->|r0] := eqVneq r 0%R; first by rewrite mul0r poweRe0 poweR1r. case: x => [x| |]//; first by rewrite /= powRrM. by rewrite !poweRyr// mulf_neq0. by rewrite !poweRNyr ?poweR0r ?(negPf s0)// mulf_neq0. 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