proposition: Lemma powR_intmul a (z : int) : 0 <= a -> a `^ z%:~R = a ^ z.
proof: Proof. by move=> a0; case: z => n; [exact: powR_mulrn | exact: powR_invn]. 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