proposition: Lemma gt0_powR a x : 0 < x -> 0 <= a -> 0 < a `^ x -> 0 < a.
proof: Proof. move=> x0 a0; rewrite /powR; case: ifPn => [_|a_neq0 _]. by rewrite gt_eqF//= ltxx. by rewrite lt_neqAle a0 andbT eq_sym. 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