proposition: Lemma ord_powa_pr2 y : ordinalp y -> y <> \0o -> \0o ^O y = \0o ^o y.
proof: Proof. move: OS0=> oz oy ynz; rewrite opow0x //. have w1: worder (ordinal_o y) by apply:ordinal_o_wor. have w2: worder (ordinal_o \0o) by apply:ordinal_o_wor. move:(olexp_osr w2 w1) => [pa pb]. apply: ordinal0_pr1 => //;rewrite pb. by apply: olex_nFe_Ee;rewrite ordinal_o_sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)