proposition: Lemma ord_powa_pr5 x : ordinalp x -> x ^O \1c = x ^o \1c.
proof: Proof. move: OS1 => oo ox; rewrite (opowx1 ox). have ese: inc emptyset (singleton emptyset) by fprops. have w1: worder (ordinal_o x) by apply:ordinal_o_wor. have w2: worder (ordinal_o \1o) by apply:ordinal_o_wor. have w3: worder (olexp (ordinal_o x) (ordinal_o \1c)) by apply olexp_worder. apply: ordinal_o_isu2 => //; apply: orderIS. move: w1 w2; set r := (ordinal_o x); set r':= (ordinal_o \1c). move => w1 w2. move: (olexp_osr w1 w2) => [ooo sr]. move: (ordinal_o_sr \1o); rewrite -/r' /ord_one /card_one => sr'. have oG: olexp_G r r'= (gfunctions (substrate r') (substrate r)). apply extensionality; first by apply: Zo_S. move => t tf; apply: Zo_i => //. have : finite_set (substrate r') by rewrite sr';apply: set1_finite. rewrite /olexp_I sr'; apply: sub_finite_set; apply: Zo_S. rewrite sr' in oG. set f := cst_graph (singleton emptyset). have ta: forall t, inc t (substrate r) -> inc (f t) (substrate (olexp r r')). move => t tsr; rewrite sr oG; apply /gfunctions_P2. rewrite /f/cst_graph;split => //;aw; fprops. by move => z /Lg_range_P [_ _ ->]. set F := Lf f (substrate r) (substrate (olexp r r')). have bf: bijection F. apply: lf_bijective => //. move => u v usr vsr sf; move: (f_equal (Vg ^~emptyset) sf). rewrite /f/cst_graph; rewrite !LgV//. move => y; rewrite sr oG =>ys;move:(gfunctions_hi ys)=> [k [fk sk tk gk]]. set z := Vf k emptyset. have zr: inc z (substrate r) by rewrite /z; Wtac ; rewrite sk; fprops. ex_tac;symmetry;rewrite /f /cst_graph - gk; apply: fgraph_exten; aww. by rewrite (domain_fg fk) sk. move => t ts /=; rewrite LgV//; move: ts => /set1_P -> //. exists F. apply: total_order_isomorphism; rewrite /F; aww. by apply: worder_total. move => a b asr bsr rab; rewrite !LfV //. apply /(olexp_gleP w1 w2); rewrite - sr;split;fprops. case: (equal_or_not a b) => eab; first by rewrite eab; left. right; exists emptyset; rewrite /f sr'; aw; split;fprops. by rewrite /cst_graph !LgV. move => i [pa] []. have: inc i (substrate r') by order_tac. by rewrite sr' => /set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)