proposition: Lemma gt0_ltr_powR r : 0 < r -> {in Num.nneg &, {homo powR ^~ r : x y / x < y >-> x < y}}.
proof: Proof. move=> r0 x y x0 y0 xy; have := ge0_ler_powR (ltW r0) x0 y0 (ltW xy). rewrite le_eqVlt => /orP[/eqP/(powR_injective r0 x0 y0)/eqP|//]. by rewrite lt_eqF. 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