proposition: Lemma ord_powa_pr3 y : ordinalp y -> \0o ^O y = \0o ^o y.
proof: Proof. move => oy; case: (equal_or_not y \0o) => ynz. rewrite ynz; apply:ord_powa_pr1; fprops. by apply:ord_powa_pr2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)