proposition: Lemma opow_pos a b: \0o <o a -> ordinalp b -> \0o <o (a ^o b).
proof: Proof. move=> ap ob; move: (ap) => [[_ oa _] anz]. apply: ord_ne0_pos; fprops => bad; case: anz. by move: (opow_nz0 oa ob bad) => [-> _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)