proposition: Lemma le1r_powRZ x y r : x >= 1 -> 0 <= y -> 1 <= r -> (x * y) `^ r >= x * (y `^ r).
proof: Proof. move=> x1 y0 r1. by rewrite (powRM _ (le_trans _ x1))// ler_wpM2r ?powR_ge0// le1r_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