proposition: Lemma OS_pow x y: ordinalp x -> ordinalp y -> ordinalp (x ^o y).
proof: Proof. move=> ox oy. case: (ord2_trichotomy ox). - move=> xz; case: (equal_or_not y \0o) => yz. rewrite xz yz opow00; fprops. rewrite xz opow0x //; fprops. - by move => xo; rewrite xo opow1x; fprops. - move:(ord_pow_axioms) =>[ [ax1 _ _ _] _ _ _]. move => xo; rewrite (opow2x _ xo). apply:(ord_induction_p5 (erefl opow') ax1 xo oy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)