proposition: Lemma ord_powa_pr1 x : ordinalp x -> x ^O \0o = x ^o \0o.
proof: Proof. move: OS0=> oz ox; rewrite opowx0. have w1: worder (ordinal_o x) by apply:ordinal_o_wor. have w2: worder (ordinal_o \0o) by apply:ordinal_o_wor. move:(olexp_osr w1 w2) => [pa pb]. apply: set1_ordinal => //; rewrite pb. by apply: olex_Fe; rewrite ordinal_o_sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)