proposition: Lemma gt0_ler_poweR r : (0 <= r)%R -> {in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}.
proof: Proof. move=> r0 + y; case=> //= [x /[1!in_itv]/= /andP[xint _]| _ _]. - case: y => //= [y /[1!in_itv]/= /andP[yint _] xy| _ _]. + by rewrite !lee_fin ge0_ler_powR. + by case: eqP => [->|]; rewrite ?powRr0 ?leey. - by rewrite leye_eq => /eqP ->. 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