proposition: Lemma norm_powR a x : 0 <= a -> `|a `^ x| = `|a| `^ x.
proof: Proof. move=> a0; rewrite /powR; case: ifPn => [/eqP ->|]. by rewrite normr0 eqxx normr_nat. rewrite neq_lt ltNge a0/= => {}a0. by rewrite gtr0_norm ?expR_gt0// gtr0_norm// gt_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