proposition: Lemma poweRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
proof: Proof. have [->|rN0] := eqVneq r 0%R; first by rewrite !poweRe0 mule1. have powyrM s : (0 <= s)%R -> (+oo * s%:E) `^ r = +oo `^ r * s%:E `^ r. case: ltgtP => // [s_gt0 _|<- _]; last first. by rewrite mule0 poweRyr// !poweR0r// mule0. by rewrite gt0_mulye// poweRyr// gt0_mulye// poweR_gt0. case: x y => [x| |] [y| |]// x0 y0; first by rewrite /= -EFinM powRM. - by rewrite muleC powyrM// muleC. - by rewrite powyrM. - by rewrite mulyy !poweRyr// mulyy. 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