proposition: Lemma ord_powa_pr4 y : ordinalp y -> \1o ^O y = \1o ^o y.
proof: Proof. move: OS1=> oz ox; rewrite opow1x. have w1: worder (ordinal_o y) by apply:ordinal_o_wor. have w2: worder (ordinal_o \1o) by apply:ordinal_o_wor. move:(olexp_osr w2 w1) => [pra prb]. apply: set1_ordinal => //. apply /singletonP; split. have ne1: nonempty (substrate (ordinal_o \1o)). exists emptyset; rewrite /ord_one /card_one ordinal_o_sr;fprops. move:(olexp_G_least w2 w1 ne1) => [h _]; ex_tac. rewrite prb /olexp_G /olexp_I ! ordinal_o_sr. move=> a b => /Zo_P [pa _] /Zo_P [pb _]. move: (gfunctions_hi pa)=> [f [ff sf tf <-]]. move: (gfunctions_hi pb)=> [g [fg sg tg <-]]. suff: f = g by move => ->. apply: function_exten => //; (try ue) => x xsf. have : inc (Vf f x) \1o by Wtac. rewrite sf in xsf; have : inc (Vf g x) \1o by Wtac. by move => /set1_P -> /set1_P ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)