proposition: Lemma ge1r_powRZ x y r : 0 < x <= 1 -> 0 <= y -> 1 <= r -> (x * y) `^ r <= x * (y `^ r).
proof: Proof. move=> /andP[x0 x1] y0 r1. by rewrite (powRM _ (ltW _))// ler_wpM2r ?powR_ge0// ge1r_powR// x0. 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