proposition: Lemma ord_powa_same a b: ordinalp a -> ordinalp b -> a ^O b = a ^o b.
proof: Proof. move => oa ob. case: (ord2_trichotomy oa); first by move => ->; apply: ord_powa_pr3. by move => ->; apply: ord_powa_pr4. move => a2. ex_middle bad0. pose p y := a ^O y = a ^o y. have pb: ~ (p b) by []. move: (least_ordinal3 ob pb); set y :=least_ordinal _ _; move => [oy py lpy]; case: py; rewrite /p. case: (ordinal_limA oy) => ly. by rewrite ly; apply: ord_powa_pr1. move: ly => [t ot tx]; rewrite tx. have lty: t <o y by rewrite tx; apply: oltS. by rewrite (ord_powa_succ oa ot) (opow_succ oa ot) (lpy _ lty). rewrite (proj2 (opow_normal a2) _ ly). have pa: forall t, inc t y -> a ^O t = a ^o t. by move => t ty; apply lpy; apply/(oltP oy). rewrite - (ord_sup_2funI pa). have: union (fun_image y (ord_powa a)) <=o a ^O y. apply: ord_ub_sup. by apply: OS_ord_powa. move => i /funI_P [z zy ->]; apply: ord_powa_M_eqle => //. have [zy1 _] //: z <o y by apply/(oltP oy). move => az; case: (oleNgt a2); rewrite az; exact: olt_02. set C := \osup _. move => le1; ex_middle ne1. move: (proj32 le1) => op. have lt1: inc C (a ^O y) by apply /(oltP op); split => //; apply:nesym. move: (ordinal_o_wor oa) (ordinal_o_wor oy)=> wora wory. move: (ordinal_o_sr a) (ordinal_o_sr y) => sra sry. move: (ordinal_o_is (olexp_worder wora wory)); rewrite -/(a ^O y). move => [f isf]; move: (order_isomorphism_w isf) => morf. move: isf => [or1 or2 [bf sf tf] sif]. move: tf; rewrite (ordinal_o_sr (a ^O y)) => tf. move: sf; rewrite(proj2 (olexp_osr wora wory)) => sf. rewrite- tf in lt1; move: ((bij_surj bf) _ lt1) => [x xsf fx]. move: (xsf); rewrite sf /olexp_G; move /Zo_P; rewrite sra sry. move =>[xg fsx]; move: (xg) => /gfunctions_P2 [fgx dx rx]. set zz:= olexp_lE (ordinal_o a). have[c cy cp]: exists2 c, inc c y & forall t, inc t (domain x) -> c <=o t -> Vg x t = zz. set ol := (olexp_I (ordinal_o a) (ordinal_o y) x). case: (emptyset_dichot ol) => ole. exists \0o;first by exact (proj32 ly). move => t tdx _; ex_middle bad. by empty_tac1 t; apply: Zo_i => //; rewrite sry - dx. have sol: sub ol (substrate (ordinal_o y)) by apply: Zo_S. move: (finite_subset_torder_greatest (worder_total wory) fsx ole sol). move => [c []]; rewrite (iorder_sr (proj1 wory) sol). move => col cleast. move: (sol _ col); rewrite sry => cy; move: ((proj33 ly) _ cy) => scy. ex_tac; move => t tdx st. have ct: c <o t by apply /oleSltP. case: (inc_or_not t ol) => tol. move: (iorder_gle1 (cleast _ tol)) => /ordo_leP [_ _ tc]. by move: ct => [[_ _ ca] cb]; case: cb; apply: extensionality. by ex_middle nv; case: tol; apply: Zo_i => //; rewrite sry -dx. move: (Os_ordinal oy cy) => oc. move: (ordinal_o_wor oc) => worc. move: (orderIS (ordinal_o_is (olexp_worder wora worc))); rewrite -/(a ^O c). move => [g isg]; move: (order_isomorphism_w isg) => morg. move: isg => [or3 or4 [bg sg tg] sig]. move: tg; rewrite (proj2(olexp_osr wora worc)) => tg. move: (OS_ord_powa oa oc) => op'. move: (ordinal_o_sr c) => src. move: sg; rewrite (ordinal_o_sr (a ^O c)) => sg. pose h t := Lg y (fun u => (Yo (inc u c) (Vg t u) zz)). have ne2: nonempty (substrate (ordinal_o a)). move: (olt_leT olt_02 a2) => /(oltP oa);rewrite sra => he;ex_tac. move: (olexp_lEp wora ne2); rewrite -/zz sra; move => [zza zzp]. have scy: sub c y. move => t tc; apply: (ordinal_transitive oy cy tc). have hp1: forall t, inc t (target g) -> inc (h t) (source f). move => t; rewrite sf tg =>/Zo_P; rewrite sra src; move => [t1 t2]. apply /Zo_P; rewrite sra sry; move: t1 => /gfunctions_P2 [ft dt rt]. split. apply /gfunctions_P2; rewrite /h; aw; split;fprops =>s. move => /Lg_range_P [b0 b0y ->]; Ytac bc => //; apply: rt. apply /(range_gP ft); rewrite dt; ex_tac. move: t2; rewrite /olexp_I src sry; set e1 := Zo _ _ ; set e2 := Zo _ _. have -> //: e1 = e2. set_extens u => /Zo_P [uc sv]; apply /Zo_P. by move: (scy _ uc) => uy; split => //; rewrite /h LgV//; Ytac0. move: sv; rewrite /h LgV//; Ytac uu => //. set hf:= Lf h (target g) (source f). have injh: injection hf. apply: lf_injective => // u v usg vsg sv. move: usg vsg; rewrite tg /olexp_G src sra => /Zo_P [] /gfunctions_P2. move => [gru du _] _ /Zo_P [] /gfunctions_P2 [grv dv _] _. apply: fgraph_exten => //; first (by ue); rewrite du => s sc. move: (scy _ sc) => sy. by move: (f_equal (Vg ^~s) sv); rewrite /h ! LgV//; Ytac0; Ytac0. have monh: order_morphism hf (olexp (ordinal_o a) (ordinal_o c)) (olexp (ordinal_o a) (ordinal_o y)). apply: total_order_morphism; try exact. by apply: worder_total; apply: olexp_worder. by rewrite /hf; aw; rewrite tg (proj2 (olexp_osr _ _)). by rewrite /hf; aw; rewrite sf (proj2 (olexp_osr _ _)). rewrite /hf; aw => u v ush vsh; rewrite !LfV//. move/(olexp_gleP wora worc) => [us1 vs1 cuv]; apply/(olexp_gleP wora wory). move: (hp1 _ ush) (hp1 _ vsh); rewrite - sf => us2 vs2. split; [exact | exact | case: cuv ; first by move => ->; left]. rewrite src sry; move => [j [jc ja jb]]; right;exists j. move: (scy _ jc) => jy. split; [exact | by rewrite /h !LgV//; Ytac0; Ytac0 |]. move => i []/sub_gleP [_ iy ji] nji. rewrite /h !LgV//; Ytac ic; Ytac0; last by exact. by apply: jb; split => //; apply /sub_gleP. have hbounded: forall x', inc x' (source f) -> (forall t : Set, inc t (domain x') -> c <=o t -> Vg x' t = zz) -> (inc (restr x' c) (target g) /\ (Vf hf (restr x' c) = x')). move => w. rewrite sf /olexp_G => /Zo_P; rewrite sra sry. move =>[wg fsw] cp'; move: (wg) => /gfunctions_P2 [fgw dw rw]. have scdx: sub c (domain w) by ue. have fgr: fgraph (restr w c) by fprops. have rg: inc (restr w c) (target g). rewrite tg; apply Zo_i. rewrite src sra; apply /gfunctions_P2; saw. move => t /(range_gP fgr); aw; move => [u uc ->]; rewrite LgV//; apply: rw. apply /(range_gP fgw); exists u;fprops. move: fsw; rewrite /olexp_I sry src; apply: sub_finite_set. move => s /Zo_P [sc vnz]; apply: Zo_i; first by apply: scy. move: vnz; rewrite LgV//. split; [by exact | rewrite /hf /h LfV //; apply: fgraph_exten; aww]. move => s sy /=; rewrite(LgV sy); Ytac sc; first by rewrite LgV//; ue. symmetry; apply: cp'; [ue |case: (oleT_el oc (Os_ordinal oy sy))=>//]. by move /oltP0 => [_ _]. move: (compose_order_morphism morg monh) => morgh. move: (compose_order_morphism morgh morf). set oac:= (ordinal_o (a ^O c)). set oay:= (ordinal_o (a ^O y)). set fgh:= f \co (hf \co g) => morfhg. have chg: hf \coP g by split => //; try fct_tac; rewrite /hf; aw. have cfhg: f \coP (hf \co g) by split => //; try fct_tac; rewrite /hf; aw. have srh: segmentp oay (Imf fgh). red; move: morfhg => [_ _ [ffgh _ _] _]; rewrite (ordinal_o_sr ((a ^O y))). split; first by move:(Imf_Starget ffgh); rewrite {2} /fgh -tf; aw. move => u v; case: (equal_or_not u v); [by move => -> | move => unv]. rewrite /fgh; move /(Imf_P ffgh); rewrite /fgh; aw. move=> [u3 usg3 uv] lvu; apply /(Imf_P ffgh). have vtf: inc v (target f). move: lvu => /sub_gleP [ok _]; ue. move: (bij_surj bf vtf) => [v1 v1df v1f]. set u2 := (Vf g u3); set u1 := Vf hf u2. have u2tag: inc u2 (target g) by rewrite /u2; Wtac; fct_tac. have u1sf: inc u1 (source f). have ->: source f = target hf by rewrite /hf; aw. rewrite /u1; Wtac; [fct_tac | by rewrite /hf; aw ]. have aux: inc u3 (source (hf \co g)) by aw. have hh: gle (olexp (ordinal_o a) (ordinal_o y)) v1 u1 <-> gle oay v u. rewrite /oay v1f uv (compfV cfhg aux) (compfV chg usg3). exact:(sif _ _ v1df u1sf). have unv1: u1 <> v1. dneg u1v1; rewrite v1f -u1v1 uv ! compfV //. move /hh: lvu => /(olexp_gleP wora wory). move => [v1g u1g]; case; first by move => hh1; case: unv1. move => [j [jsy cuvj cuvgj]]. have cp': (forall t, inc t (domain v1) -> c <=o t -> Vg v1 t = zz). move: v1g =>/Zo_P []; rewrite sra sry => /gfunctions_P2 [fgv dv rv] fsv. move: u1g =>/Zo_P []; rewrite sra sry => /gfunctions_P2 [fgu du ru] fsu. move => t td1 ct. have sa: forall s, inc s y -> c <=o s -> Vg u1 s = zz. move => s sd sv; rewrite /u1 /hf /h LfV// LgV//; Ytac sc; last by exact. by move/(oltP oc): sc => /(oleNgt sv). move: jsy; rewrite sry => jy. case: (oleT_el oc (Os_ordinal oy jy)) => ccj. move : cuvj; rewrite (sa _ jy ccj). have va: inc (Vg v1 j) a. apply: rv; apply /(range_gP fgv); rewrite dv; ex_tac. move: wora (zzp _ va) => [ora _ ] la lb; order_tac. have : inc j t by apply/ (oltP (proj32 ct)); exact (olt_leT ccj ct). rewrite dv in td1; move /(ordo_ltP oy jy td1) => h1. by rewrite (cuvgj _ h1); apply: sa. move: (hbounded _ v1df cp') => [vtg v1v]. move: (bij_surj bg vtg) => [w wdg wv]. exists w; rewrite /fgh ? compfV//; aww. by rewrite -wv v1v v1f. move: (hbounded _ xsf cp) => [rsx1 hfz]. move: (bij_surj bg rsx1); rewrite sg. move => [s sa sv]. have sg1: inc s (source g) by rewrite sg. have ltc: a ^O c <=o C. have os1: ordinal_set (fun_image y (ord_powa a)). move => t /funI_P [z zy ->]; apply: OS_ord_powa => //. exact: (Os_ordinal oy zy). apply: ord_sup_ub => //; apply /funI_P;ex_tac. have ltaC: C <o a ^O y by split => //; apply:nesym. have ltacay := ole_ltT ltc ltaC. move: (inclusion_morphism_b ltacay srh morfhg sa) ltc. rewrite /fgh ! compfV//; aw; trivial;rewrite - sv hfz fx => ->. by move: sa => /(oltP op') ta /(oltNge ta). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)