proposition: Lemma ge0_ler_powR r : 0 <= r -> {in Num.nneg &, {homo powR ^~ r : x y / x <= y >-> x <= y}}.
proof: Proof. rewrite le_eqVlt => /predU1P[<- x y _ _ _|]; first by rewrite !powRr0. move=> a0 x y; rewrite 2!nnegrE !le_eqVlt => /predU1P[<-|x0]. move=> /predU1P[<- _|y0 _]; first by rewrite eqxx. by rewrite !powR0 ?(gt_eqF a0)// powR_gt0 ?orbT. move=> /predU1P[<-|y0]; first by rewrite gt_eqF//= ltNge (ltW x0). move=> /predU1P[->//|xy]; first by rewrite eqxx. by apply/orP; right; rewrite /powR !gt_eqF// ltr_expR ltr_pM2l// ltr_ln. 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