proposition: Lemma power_of_suma a b c: ordinalp a -> ordinalp b -> ordinalp c -> (a ^O (b +o c)) = (a ^O b) *o (a ^O c).
proof: Proof. move => oa ob oc. move: (ordinal_o_wor oa) => woa. move: (ordinal_o_wor ob) => wob. move: (ordinal_o_wor oc) => woc. move: (ordinal_o_wor (OS_sum2 ob oc)) => wo_bc. move: (OS_ord_powa oa ob) => o_ab. move: (OS_ord_powa oa oc) => o_ac. move: (ordinal_o_wor o_ab) => wo_ab. move: (ordinal_o_wor o_ac) => wo_ac. apply: ordinal_o_isu1; [ by apply: olexp_worder | by apply: orprod2_wor | ]. rewrite /ord_powa. move: (orprod_invariant4 (ordinal_o_is (olexp_worder woa wob)) (ordinal_o_is (olexp_worder woa woc))). apply: orderIT. rewrite /osum2. move: (orsum2_wor wob woc) => pa. move: (ordinal_o_is (orsum2_wor wob woc)) => pb. move: (worder_invariance pb pa) => pc. move: (orderIR (proj1 woa)) => pd. move: (orderIS(opowa_invariant woa woa pa pc pd pb)) => h. apply: (orderIT h). move: woa wob woc. set A := ordinal_o a; set B := ordinal_o b; set C:= ordinal_o c => woa wob woc. clear wo_ab wo_ac pa pb pc pd h wo_bc o_ab o_ac. set Gab:= (olexp_G A B). set Gac := (olexp_G A C). set Gabc := olexp_G A (order_sum2 B C). set gab:= (gfunctions b a). set gac:= (gfunctions c a). set gabc:= (gfunctions (canonical_du2 b c) a). pose fOI u v := fun x => finite_set (olexp_I u v x). move: (olexp_worder woa woc) (olexp_worder woa wob) => woac woab. move: (orsum2_wor wob woc) => wobc. move: (woab)(woac) => [oab _] [oac _]. move:(ordinal_o_sr a) (ordinal_o_sr b) (ordinal_o_sr c) => sa sb sc. move:(olexp_osr woa wob) (olexp_osr woa woc) => [_ sab][_ sac]. have sr0: product2 (substrate (olexp A C)) (substrate (olexp A B)) = product2 Gac Gab. by rewrite sab sac. have sr1: substrate (order_prod2 (olexp A B) (olexp A C)) = product2 Gac Gab. by rewrite (proj2 (orprod2_osr oab oac)). have sr2: substrate (olexp A (order_sum2 B C)) = Gabc. by rewrite (proj2 (olexp_osr woa wobc)). have sr3: (substrate (order_sum2 B C)) = canonical_du2 b c. by rewrite (orsum2_sr (proj1 wob) (proj1 woc)) sb sc. have Gab1: Gab = Zo gab (fOI A B) by rewrite /Gab /olexp_G sa sb. have Gac1: Gac = Zo gac (fOI A C) by rewrite /Gac /olexp_G sa sc. have Gabc1: Gabc = Zo gabc (fOI A (order_sum2 B C)). by rewrite /Gabc /olexp_G sr3 sa. pose pr1f f := Lg b (fun z => Vg f (J z C0)). pose pr2f f := Lg c (fun z => Vg f (J z C1)). pose pr3f f := variantLc (pr2f f) (pr1f f). have pr1f1: forall f, inc f gabc -> inc (pr1f f) gab. move => f; rewrite /gabc /gab. move /gfunctions_P2; move => [fgf df rf]. apply /gfunctions_P2; rewrite /pr1f; split; [ fprops| by aw | ]. move => t /Lg_range_P [x xb ->]; apply: rf; apply /(range_gP fgf). by exists (J x C0) => //;rewrite df; apply candu2_pra. have pr2f1: forall f, inc f gabc -> inc (pr2f f) gac. move => f; rewrite /gabc /gac. move /gfunctions_P2; move => [fgf df rf]. apply /gfunctions_P2; rewrite /pr2f; split; [ fprops| by aw | ]. move => t /Lg_range_P [x xb ->]; apply: rf; apply /(range_gP fgf). by exists (J x C1) => //;rewrite df; apply candu2_prb. have pr1f2: forall f, inc f Gabc -> inc (pr1f f) Gab. move => f; rewrite Gab1 Gabc1 => /Zo_P [pa pb]; apply /Zo_P; split;fprops. move: pb; rewrite /fOI /olexp_I sr3 sb. set e1:= Zo _ _; set e2 := Zo _ _ => fe1. have hp: forall x, inc x e2 -> inc (J x C0) e1. move => x => /Zo_P [xb xx]; apply: Zo_i; first by apply candu2_pra. move: xx;rewrite /pr1f LgV//. apply: (sub_image_finite_set fe1 hp) => u v _ _ sv; apply: (pr1_def sv). have pr2f2: forall f, inc f Gabc -> inc (pr2f f) Gac. move => f; rewrite Gac1 Gabc1; move /Zo_P => [pa pb]; apply Zo_i; fprops. move: pb; rewrite /fOI /olexp_I sr3 sc. set e1:= Zo _ _; set e2 := Zo _ _ => fe1. have hp: forall x, inc x e2 -> inc (J x C1) e1. move => x => /Zo_P [xb xx]; apply: Zo_i; first by apply candu2_prb. move: xx;rewrite /pr2f LgV//. apply: (sub_image_finite_set fe1 hp) => u v _ _ sv; apply: (pr1_def sv). have pr2f3: forall f, inc f Gabc -> inc (pr3f f) (product2 Gac Gab). move => f fi; move: (pr1f2 _ fi)(pr2f2 _ fi) => pa pb. apply /setX2_P; rewrite /pr3f !LgV//; aw; fprops; split;fprops. pose g := Lf pr3f Gabc (product2 Gac Gab). have bg: bijection g. apply: lf_bijective => //. rewrite Gabc1;move => u v /Zo_S ug /Zo_S vg sv. move: (f_equal (Vg ^~ C0) sv) (f_equal (Vg ^~ C1) sv). rewrite /pr3f; aw; rewrite /pr1f /pr2f => eq1 eq2. move: ug vg => /gfunctions_P1 [fgu du _] /gfunctions_P1 [fgv dv _]. apply: fgraph_exten => //; rewrite du // => x /candu2P. move => [px]; case; move => [Px Qx]; move: px; rewrite /pairp Qx => px. move: (f_equal (Vg ^~ (P x)) eq2); rewrite !LgV//; ue. move: (f_equal (Vg ^~ (P x)) eq1); rewrite !LgV//; ue. move => y /setX2_P [fgy dy vy1 vy2]. set z := Lg (canonical_du2 b c) (fun t => (Yo (Q t = C0) (Vg (Vg y C1) (P t))(Vg (Vg y C0) (P t)))). have fgz: fgraph z by rewrite /z;fprops. have dz: domain z = canonical_du2 b c by rewrite /z; aw. move: (vy1) => /Zo_P [] /gfunctions_P2 [pa1 pb1 pc1] pd1. move: (vy2) => /Zo_P [] /gfunctions_P2 [pa2 pb2 pc2] pd2. move: C1_ne_C0 => td. have eqa: pr3f z = y. rewrite /pr3f; apply:fgraph_exten. - fprops. - done. - by aw. - aw => x xtp; rewrite /pr1f /pr2f. try_lvariant xtp;apply:fgraph_exten; fprops; aw. + by rewrite pb1. + move => t tc; move: (candu2_prb b tc) => h. by rewrite (LgV tc) (LgV h) pr1_pair pr2_pair; Ytac0. + by rewrite pb2. - move => t tc; move: (candu2_pra c tc) => h. by rewrite (LgV tc) (LgV h) pr1_pair pr2_pair; Ytac0. exists z; last by exact. have zg: inc z gabc. apply /gfunctions_P2; split => // t /(range_gP fgz). rewrite dz;move => [x xdz ->]. move: (xdz) => /candu2P. move => [px]; case; move => [Px Qx]; rewrite /z LgV//; rewrite Qx; Ytac0. move: vy2 =>/Zo_P [] /gfunctions_P2 [pa pb pc] _. rewrite - sa; apply:pc; apply /(range_gP pa). rewrite pb;exists (P x) => //; ue. move: vy1 =>/Zo_P [] /gfunctions_P2 [pa pb pc] _. rewrite - sa; apply:pc; apply /(range_gP pa). rewrite pb;exists (P x) => //; ue. apply: Zo_i; first by rewrite sr3 sa. move: pd1 pd2;rewrite /olexp_I. set e1 := Zo _ _; set e2 := Zo _ _; set e3 := Zo _ _ => fe1 fe2. move: (finite_fun_image (fun z => (J z C1)) fe1). move: (finite_fun_image (fun z => (J z C0)) fe2) => fe1' fe2'. move: (finite_union2 fe1' fe2') => fe3'. apply: sub_finite_set fe3'. move => t /Zo_P; rewrite sr3; move => [tdi vt]; apply /setU2_P. move: (tdi) => /candu2P [pt]; case=> [][Pt Qt]; [left | right ]; move: vt; rewrite (LgV tdi) Qt; Ytac0 => tnl; apply /funI_P; rewrite -Qt; exists (P t) => //; apply: Zo_i => //; ue. exists g; apply: total_order_isomorphism. - apply: worder_total; apply: olexp_worder => //. - by apply: orprod2_or; apply: (proj1 (olexp_osr _ _)). - done. - by rewrite /g; aw. - by rewrite /g; aw. - rewrite /g lf_source; move => x y xsg ysg /=. rewrite (LfV pr2f3 xsg)(LfV pr2f3 ysg). move /(olexp_gleP woa wobc) => [_ _ cxy]. apply / (orprod2_gleP (proj1 woab) (proj1 woac)); rewrite sr0. move: (pr2f3 _ xsg) (pr2f3 _ ysg) => ip1 ip2. split; [by done | by done | case: cxy]. move => <-; left; split; [reflexivity | order_tac]. by move: ip1; rewrite - sr0 ; move /setX2_P=> [_ _ _]. rewrite sr3; move => [j [jc jv ajv]]. rewrite /pr3f; aw. move: jc => /candu2P [pj]; case; move => [Pj Qj]. left; split. have xg: inc x gabc by move: xsg =>/Zo_P []; rewrite sr3 sa. have yg: inc y gabc by move: ysg =>/Zo_P []; rewrite sr3 sa. move: (pr2f1 _ xg) =>/gfunctions_P1 [fg1 d1 v1]. move: (pr2f1 _ yg) =>/gfunctions_P1 [fg2 d2 v2]. apply: fgraph_exten => //; rewrite d1 // => t tc. have lt1: glt (order_sum2 B C) j (J t C1). rewrite - pj Qj; apply:orsum2_gle_spec. by rewrite sb. by rewrite sc. move: (ajv _ lt1); rewrite /pr2f!LgV//. apply /(olexp_gleP woa wob). split; [ by apply: pr1f2 | by apply: pr1f2 | right ]. exists (P j); rewrite sb /pr1f !LgV//; rewrite -Qj pj; split => //. move => i [iv niv]. have ib: inc i b by rewrite - sb; order_tac. rewrite ! LgV//; apply: ajv; split; last by rewrite -{1} pj; dneg uu; exact (pr1_def uu). apply /orsum2_gleP; rewrite -{1} pj Qj pr1_pair pr2_pair. split; first by apply: candu2_pra; rewrite sb. by apply: candu2_pra; rewrite sb. by constructor 1. right; move: (jv) => [_ jvb]. split; last first. move => sv; case: jvb;move: (f_equal (Vg ^~(P j)) sv); rewrite /pr2f !LgV//. by rewrite -Qj pj. apply /(olexp_gleP woa woc). split; [ by apply: pr2f2 | by apply: pr2f2 | right]. exists (P j); rewrite sc /pr2f !LgV//; rewrite -Qj pj; split => //. move => i [iv niv]. have ic: inc i c by rewrite - (ordinal_o_sr c); order_tac. rewrite !LgV//; apply: ajv; split; last by rewrite -{1} pj; dneg uu; exact (pr1_def uu). apply /orsum2_gleP; rewrite -{1} pj Qj pr1_pair pr2_pair. split; first by apply: candu2_prb; rewrite sc. by apply: candu2_prb; rewrite sc. by constructor 2; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)