(** * Theory of Sets : Ordinals Copyright INRIA (2009-2013 Apics; Marelle Team (Jose Grimm). *) (* $Id: sset11.v,v 1.177 2016/04/07 16:44:23 grimm Exp$ *) Require Import ssreflect ssrfun ssrbool eqtype ssrnat. Require Export sset10. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Module Ordinals1. (** ** Sums and products of orders *) (** Ordinal sum of a family of orders g indexed by the substrate of r *) Lemma orprod_wor r g: worder_on r (domain g) -> worder_fam g -> finite_set (substrate r) -> worder (order_prod r g). Proof. move=> [wor sr] alw fs. have lea:orprod_ax r g by split => // i ie; exact (proj1 (alw _ ie)). move h: (cardinal (substrate r)) => n. have nN: natp n by apply /NatP; rewrite - h. clear wor sr fs; move:n nN r g lea alw h. apply: Nat_induction. move=> r g lea alw cr. move:(orprod_osr lea) => [lo]. rewrite /prod_of_substrates /fam_of_substrates. move: lea => [_ <- _];rewrite (card_nonempty cr) setXb_0' => s1. exact:(worder_set1 (conj lo s1)). move=> n nN hrec r g lea alwo csr. have lo: (order (order_prod r g)) by fprops. have [[or _] sr alo] := lea. apply:(worder_prop_rev lo) => [x xsr [x0 x0x]]. move: xsr; bw => xsr. case: (emptyset_dichot (substrate r)) => nesr. by case: (@succ_nz n); rewrite - csr nesr cardinal_set0. move: (worder_least (proj31 lea) nesr) => [i []]; rewrite {1} sr => isr ilsr. set Y := fun_image x (fun z => Vg z i). have sYs: (sub Y (substrate (Vg g i))). move=> t /funI_P [z zx ->]; apply: prod_of_substrates_p; fprops. have neY: (nonempty Y) by exists (Vg x0 i); apply /funI_P; ex_tac. move: (worder_prop (alwo _ isr) sYs neY) => [z zY zl]. move: (proj1 (alwo _ isr)) => or'. set X1 := Zo x (fun t => Vg t i = z). have p1: (forall a b, inc a x -> inc b x -> inc a X1 -> ~ inc b X1 -> glt (order_prod r g) a b). move=> a b ax bx aX1 bX1; split; last by dneg ab; rewrite -ab. apply orprod_gleP =>//; split;fprops. right; exists i; split => //; first by ue. have ib: z <> Vg b i by move=> eq2; move: bX1 => /Zo_P; apply;split => //. have vbY: (inc (Vg b i) Y) by apply /funI_P; ex_tac. move: aX1 => /Zo_P [_ ->]; split => //; apply: (zl _ vbY). move=> j rj. have jsr: (inc j (substrate r)) by order_tac. move: (ilsr _ jsr) => le2; order_tac. set I1 := (substrate r) -s1 i. set r1 := induced_order r I1. set g1 := restr g I1. have I1sr: (sub I1 (substrate r)) by apply: sub_setC. have hh: sub I1 (domain g) by ue. have dg1: domain g1 = I1 by rewrite /g1;bw; ue. have sdg1g: sub (domain g1) (domain g) by rewrite dg1; ue. have la1: orprod_ax r1 g1. split => //. + move: lea => [WO _ _]; apply: induced_wor => //. + by rewrite /r1; aw. + hnf; rewrite /g1 => j j1; move: (alo _ (sdg1g _ j1)) => og1;bw; ue. have alw: allf g1 worder. move=>j jdg; rewrite /g1 restr_ev; [by apply: alwo;apply: sdg1g| ue]. have cs: cardinal (substrate r1) = n. rewrite - sr in isr. rewrite /r1 /I1; aw; rewrite - cpred_pr5 // csr cpred_pr1; fprops. set X2 := fun_image X1 (fun z => restr z I1). have X2s: sub X2 (substrate (order_prod r1 g1)). bw; move=> t /funI_P [u uX1 ->]; apply /setXb_P. have ux: (inc u x) by move: uX1=> /Zo_S. move: (xsr _ ux) => /prod_of_substratesP [fgfu du iVV]. bw; rewrite /g1;bw; split;fprops; move => j jI1; bw; apply: iVV; ue. have neX2: (nonempty X2). apply: funI_setne; move: zY => /funI_P [z0 z0x pz0];exists z0. by apply /Zo_P. move:(worder_prop (hrec _ _ la1 alw cs) X2s neX2)=> [w /funI_P [v vX1 rv] wle]. have vx: inc v x by move: vX1 => /Zo_S. have sxs: sub x (substrate (order_prod r g)) by bw. ex_tac. move=> u ux1. case: (equal_or_not (Vg u i) z)=> Vu; last first. have nv: (~ inc u X1) by move /Zo_P => [_]. by move: (p1 _ _ vx ux1 vX1 nv)=> [le _]. have uX1: (inc u X1) by apply: Zo_i. have rX2: (inc (restr u I1) X2) by apply /funI_P; ex_tac. move: (wle _ rX2). move /(orprod_gle1P la1) => [wp rp]; set T:= Zo _ _ => op. apply /(orprod_gle1P lea); split;fprops. have aa:sub (Zo (domain g) (fun i0 => Vg v i0 <> Vg u i0)) (substrate r). by rewrite sr; apply: Zo_S. move=> j []; rewrite (iorder_sr or aa) => /Zo_P [jd nsv] aux. have jI1: inc j I1. by apply /setC1_P;split => //; [ ue | dneg ij; rewrite ij Vu; move:vX1 => /Zo_P []]. move/prod_of_substratesP: (xsr _ vx) => [fgv dv vp]. move /prod_of_substratesP: (xsr _ ux1) => [fgu du up]. have pa: sub I1 (domain u) by rewrite du -dg1. have pb: sub I1 (domain v) by rewrite dv -dg1. have jT: inc j T by apply: Zo_i; [ue | bw; rewrite rv; bw]. have lej: (least (induced_order r1 T) j). move: (iorder_osr or I1sr) => [or1' sr1']. have sT: sub T (substrate r1) by rewrite /r1; aw;rewrite -dg1;apply: Zo_S. hnf; aw; split =>// x1 aux2. move: (aux2) => /Zo_P []; rewrite dg1 => xi; rewrite rv; bw => pc. apply /(iorder_gleP _ jT aux2); apply /(iorder_gleP _ jI1 xi). have aux3: (inc x1 (Zo (domain g) (fun i => Vg v i <> Vg u i))). apply: Zo_i => //; ue. exact: (iorder_gle1 (aux _ aux3)). move: (op _ lej); rewrite rv /g1; bw. Qed. Lemma orprod2_wor r r': worder r -> worder r' -> worder (order_prod2 r r'). Proof. move: cdo_wor => [pa pb] wor wor'; apply: orprod_wor => //. - split => //; bw. - hnf; bw; move=> i ind; try_lvariant ind. - apply: finite_set_scdo. Qed. Lemma orsum2_wor r r': worder r -> worder r' -> worder (order_sum2 r r'). Proof. move: cdo_wor => [pa pb] wor wor'; apply: orsum_wor; first by split; bw. hnf; bw;move=> i ind; try_lvariant ind. Qed. Hint Resolve orsum2_wor orprod2_wor: fprops. Lemma set_ord_lt_prop3a a: ordinalp a -> ole_on a = ordinal_o a. Proof. move => oa. have [p2 p1]:= (wordering_ole_pr (ordinal_set_ordinal oa)). apply: sgraph_exten; try apply: order_is_graph; fprops. move => u v; split; move /graph_on_P1=> [pa pb pc]; apply /graph_on_P1 => //;split => //. + by move: pc => [_ _]. + split; [ exact:ordinal_hi oa pa | exact:ordinal_hi oa pb | done]. Qed. Lemma set_ord_lt_prop3 a: ordinalp a -> ordinal (ole_on a) = a. Proof. move=> oa; rewrite (set_ord_lt_prop3a oa); apply: (ordinal_o_o oa). Qed. Lemma finite_ordinal1 n: natp n -> n = ordinal (Nint_co n). Proof. move=> nN. have cn: cardinalp n by fprops. have ox: ordinalp n by apply: OS_cardinal. have cnn: cardinal n = n by apply: card_card. have fs: finite_set n by apply /NatP; ue. have w1 := (Nintco_wor n). have on := (OS_ordinal (proj1 w1)). have p1 := (worder_total (ordinal_o_wor ox)). have p2 := (worder_total (ordinal_o_wor on)). have pa := (ordinal_o_sr n). have [f [_ _ [bf sf tf] _]]:= (ordinal_o_is (proj1 w1)). have : (source f) \Eq (target f) by exists f;split => //. rewrite tf sf (proj2 w1). set S := substrate _ => /card_eqP aux. have p3: (substrate (ordinal_o n)) \Eq S. by apply/card_eqP; rewrite pa - aux card_Nint. have fs1: finite_set (substrate (ordinal_o n)) by rewrite (ordinal_o_sr n). move: (isomorphism_worder_finite p1 p2 fs1 p3) => [g [fiso _]]. by apply: (ordinal_o_isu ox on); exists g. Qed. Lemma ord_omega_pr: omega0 = ordinal Nat_order. Proof. have bwo := proj1 Nat_order_wor. suff: (ordinal_o omega0 = Nat_order). move => <-; symmetry;apply: ordinal_o_o; fprops. apply: sgraph_exten; try apply: order_is_graph; fprops. move=> u v; split. move /graph_on_P1 => [p1 p2 p3]; apply Nat_order_leP. split => //;split => //; fprops. by move/Nat_order_leP => [pa pb [_ _ pc]];apply /graph_on_P1. Qed. Lemma olt_omegaP x: x natp x. Proof. apply: (oltP OS_omega). Qed. Lemma clt_omegaP x: x natp x. Proof. split => h; first by move: (oclt h) => /olt_omegaP. by apply: oclt3; [fprops| apply: CS_omega | apply /olt_omegaP]. Qed. Lemma olt_0omega: \0o \0o. Proof. exact (nesym (proj2 olt_0omega)). Qed. Lemma olt_1omega: \1o /olt_omegaP; case. Qed. Lemma olt_2omega: \2o substrate x = emptyset -> ordinal x = \0o. Proof. move=> ox sx; rewrite (empty_substrate_zero sx) ordinal0_pr //. Qed. Lemma ordinal0_pr2 x: worder x -> ordinal x = \0o -> substrate x = emptyset. Proof. move=> /ordinal_o_is => ha hb. move: ha; rewrite hb => [] [f [_ _ [bf sf tf] _]]. rewrite (ordinal_o_sr \0o) /ord_zero in tf; rewrite - sf. apply /set0_P => y ysf; empty_tac1 (Vf f y); Wtac; fct_tac. Qed. Lemma osucc_nz x : osucc x <> \0o. Proof. by move => h; move: (succ_i x); rewrite h => /in_set0. Qed. Lemma ordinal1_pr x: ordinal (singleton (J x x)) = \1o. Proof. have [p1 p2]:= (set1_wor x). apply: (ordinal_o_isu2 p1 OS1); apply: set1_order_is2; fprops. by rewrite p2; exists x. by rewrite ordinal_o_sr; exists emptyset. Qed. Lemma set1_ordinal x: order x -> singletonp (substrate x) -> ordinal x = \1o. Proof. move=> ox sx; move: (set1_order_is1 ox sx) => [y ->]; exact:ordinal1_pr. Qed. (** ** ordinal sum and product *) Definition osum r g := ordinal (order_sum r (Lg (domain g) (fun z => (ordinal_o (Vg g z))))). Definition oprod r g := ordinal (order_prod r (Lg (domain g) (fun z => (ordinal_o (Vg g z))))). Definition osum2 a b := ordinal (order_sum2 (ordinal_o a) (ordinal_o b)). Definition oprod2 a b := ordinal (order_prod2 (ordinal_o a) (ordinal_o b)). Notation "x +o y" := (osum2 x y) (at level 50). Notation "x *o y" := (oprod2 x y) (at level 40). Lemma OS_sum r g: worder_on r (domain g) -> ordinal_fam g -> ordinalp (osum r g). Proof. move=> [or sr] alo ; apply: OS_ordinal. apply: orsum_wor; [ split; bw | hnf; bw => i idg; bw; fprops]. Qed. Lemma OS_prod r g: worder_on r (domain g) -> ordinal_fam g -> finite_set (substrate r) -> ordinalp (oprod r g). Proof. move=> osr alo fs; apply: OS_ordinal. apply: orprod_wor => //; [ bw| hnf; bw=> i idg; bw; fprops ]. Qed. Lemma osum2_rw a b: a +o b = osum canonical_doubleton_order (variantLc a b). Proof. by rewrite /osum2 /osum /order_sum2 variantLc_comp. Qed. Lemma oprod2_rw a b: a *o b = oprod canonical_doubleton_order (variantLc b a). Proof. by rewrite /oprod2 /oprod /order_prod2 variantLc_comp. Qed. Lemma OS_sum2 a b: ordinalp a -> ordinalp b -> ordinalp (a +o b). Proof. move=> wo1 wo2;apply: OS_ordinal; fprops. Qed. Lemma OS_prod2 a b: ordinalp a -> ordinalp b -> ordinalp (a *o b). Proof. move=> wo1 wo2; apply: OS_ordinal; fprops. Qed. Hint Resolve OS_sum2 OS_prod2 : fprops. Lemma orsum_invariant1 r r' f g g': order_on r (domain g) -> order_on r' (domain g') -> order_isomorphism f r r' -> (forall i, inc i (substrate r) -> (Vg g i) \Is (Vg g' (Vf f i))) -> (order_sum r g) \Is (order_sum r' g'). Proof. move=> [or sr] [or' sr'] oi ali. have oa: (orsum_ax r g). by split => //; hnf;rewrite - sr=> i idg; move:(ali _ idg)=> [h []]. move: (oi) => [_ _ [[[ff ijf] sjf] srf tgf] oif]. have oa': orsum_ax r' g'. split => //; hnf;rewrite - sr' - tgf=> i idg. move: ((proj2 sjf) _ idg) => [x xsf <-]. by rewrite srf in xsf; move: (ali _ xsf)=> [h [o1 o2 _]]. move: (orsum_or oa) (orsum_or oa') => h1 h2; aw. set fa := fam_of_substrates g. set fb := fam_of_substrates g'. pose oj i := choose (fun z => order_isomorphism z (Vg g i) (Vg g' (Vf f i))). have ojp: (forall i, inc i (substrate r) -> order_isomorphism (oj i) (Vg g i) (Vg g' (Vf f i))). move=> i isr; rewrite /oj; apply: (choose_pr (ali _ isr)). pose h x := J (Vf (oj (Q x)) (P x)) (Vf f (Q x)). have ta: (forall x, inc x (disjointU fa) -> inc (h x) (disjointU fb)). move=> x xd; move: (disjointU_hi xd); rewrite /fa/fam_of_substrates. rewrite Lg_domain; move=> [qd]; bw; move => ps px. have wq: (inc (Vf f (Q x)) (domain g')). by rewrite - sr' - tgf; Wtac; rewrite srf sr. apply: disjointU_pi; rewrite /fb;bw. rewrite sr in ojp;move: (ojp _ qd) => [_ _ [fx sx tx] _]. by rewrite - tx; Wtac; fct_tac. have ta1: lf_axiom h (substrate (order_sum r g)) (substrate(order_sum r' g')). bw. exists (Lf h (substrate (order_sum r g)) (substrate (order_sum r' g'))). hnf; rewrite /bijection_prop lf_source lf_target; split => //; bw. split=> //; apply: lf_bijective =>//. rewrite /h => u v us vs eq; move:(du_index_pr1 us) (du_index_pr1 vs). move=> [Qu Pu pu][Qv Pv pv]. move: (pr2_def eq) (pr1_def eq) => r1 r2. have sQ: Q u = Q v by apply: ijf => //; rewrite srf;ue. rewrite - sQ in r2 Pv; rewrite - sr in Qu. move: (ojp _ Qu) => [_ _ [[[_ ijfj] _] sfj _] _]. apply: pair_exten =>//; apply: ijfj =>//; ue. move=> y ys; move: (du_index_pr1 ys)=> [Qy Py py]. rewrite - sr' -tgf in Qy; move:((proj2 sjf) _ Qy) =>[x xsf Wx]. rewrite srf in xsf; move: (ojp _ xsf) => [_ _ [[_ sjj] sfj tjj] _]. rewrite -Wx - tjj in Py; move: ((proj2 sjj) _ Py)=> [x0 x0s x0w]. exists (J x0 x) => //. apply: disjointU_pi; bw; ue. by rewrite /h; aw; rewrite Wx x0w; aw; rewrite py. hnf; aw => x y xs ys; aw. move: ta1; bw => ta2; move: (ta2 _ xs)(ta2 _ ys) => ha hb. move: (du_index_pr1 xs) (du_index_pr1 ys) => [Qx Px px][Qy Py py]. rewrite - sr - srf in Qx Qy; rewrite - srf in ojp. move: (ojp _ Qx) => [_ _ [_ sfj _] ojj]. have qa: inc (P x) (source (oj (Q x))) by ue. have qb: Q x = Q y -> inc (P y) (source (oj (Q x))) by rewrite sfj => ->. split; move/orsum_gleP => [_ _ aux]; apply /orsum_gleP;split => //; move: aux; rewrite /order_sum_r /h !pr1_pair !pr2_pair. case => pa; first by left; apply /(order_isomorphism_siso oi Qx Qy). move: pa => [pa pb];rewrite - pa; right; split => //. by apply/ojj => //; apply: qb. case => pa; first by left; apply /(order_isomorphism_siso oi Qx Qy). move: pa => [pa]; move: (ijf _ _ Qx Qy pa) => pc; rewrite - pc => pb. by right;split => //; apply /ojj => //; apply: qb. Qed. Lemma orsum_invariant2 r g g': order r -> substrate r = domain g -> substrate r = domain g' -> (forall i, inc i (substrate r) -> (Vg g i) \Is (Vg g' i)) -> (order_sum r g) \Is (order_sum r g'). Proof. move=> or sr sr' ai. apply: (orsum_invariant1 (conj or sr) (conj or sr') (identity_is or)). move => i isr; bw; apply: ai =>//. Qed. Lemma orsum_invariant3 r g: worder_on r (domain g) -> worder_fam g -> ordinal (order_sum r g) = osum r (Lg (substrate r) (fun i => ordinal (Vg g i))). Proof. move => [wor sr] alo. have or: order r by fprops. rewrite /osum; apply: ordinal_o_isu1. - by apply: orsum_wor. - apply: orsum_wor; [ split; bw | hnf; bw => i isr; bw ]. rewrite sr in isr; apply: (ordinal_o_wor (OS_ordinal (alo _ isr))). - apply: orsum_invariant2 => //; bw. rewrite sr => i isr ; bw; apply: (ordinal_o_is (alo _ isr)). Qed. Lemma orsum_invariant4 r1 r2 r3 r4: r1 \Is r3 -> r2 \Is r4 -> (order_sum2 r1 r2) \Is (order_sum2 r3 r4). Proof. move=> h1 h2; rewrite /order_sum2. move: cdo_wor => [[res _] sr]. apply: orsum_invariant2; rewrite ?sr; bw; fprops. move=> i itp; try_lvariant itp. Qed. Lemma orprod_invariant1 r r' f g g': worder_on r (domain g) -> order_on r' (domain g') -> order_isomorphism f r r' -> (forall i, inc i (substrate r) -> (Vg g i) \Is (Vg g' (Vf f i))) -> (order_prod r g) \Is (order_prod r' g'). Proof. move=> [wor sr] [or' sr'] oif ali. have aux: (order_isomorphic r r') by exists f. have wor':= (worder_invariance aux wor). clear aux. have bf: bijection f by move: oif => [_ _ [bf _ _] _]. move: (oif) => [or _ [[[ff ijf] sjf] srf tgf] oif']. have oa: (orprod_ax r g). by split => //;hnf;rewrite - sr=> i idg; move:(ali _ idg)=> [h [o1 o2 _]]. have oa': orprod_ax r' g'. split => //;hnf;rewrite - sr' - tgf=> i idg. move: ((proj2 sjf) _ idg) => [x xsf <-]. by rewrite srf in xsf; move: (ali _ xsf)=> [h [o1 o2 _]]. move: (orprod_or oa)(orprod_or oa') => o1 o2; aw. set fa := fam_of_substrates g. set fb := fam_of_substrates g'. pose oi i := choose (fun z => order_isomorphism z (Vg g i) (Vg g' (Vf f i))). have oip: (forall i, inc i (substrate r) -> order_isomorphism (oi i) (Vg g i) (Vg g' (Vf f i))). by move=> i isr; apply: (choose_pr (ali _ isr)). pose fi := Vf (inverse_fun f). have fip: (forall i, inc i (substrate r') -> Vf f (fi i) = i). move=> i isr; rewrite inverse_V //; ue. have fis: (forall i, inc i (substrate r') -> inc (fi i) (substrate r)). rewrite - tgf - srf; move=> i isf; apply:inverse_Vis =>//. pose fj := Vf f. have fjs: forall i, inc i (substrate r) -> (inc (fj i) (substrate r')). rewrite - srf - tgf /fj; move=> i isg; fprops. have fij: forall i, inc i (substrate r) -> fi (fj i) = i. rewrite - srf /fi/fj;move => i idf; rewrite inverse_V2 //. pose h z := Lg (substrate r') (fun i => Vf (oi (fi i))(Vg z (fi i)) ). set (A := substrate(order_prod r g)). set (B := substrate(order_prod r' g')). have HA : A = (prod_of_substrates g) by rewrite /A orprod_sr. have HB : B = (prod_of_substrates g') by rewrite /B orprod_sr. have ta: (forall z, inc z A -> inc (h z) B). rewrite HA HB => z /prod_of_substratesP [fgf dz iVV]. apply /prod_of_substratesP; rewrite /h;split => //; [fprops | bw | ]. rewrite - sr' => i isr; bw. have fisr:= (fis _ isr). move: (oip _ fisr) => [_ _ [boi soi]]. rewrite (fip _ isr) => <- _; Wtac; try fct_tac. rewrite soi; apply: iVV; rewrite - sr //. have ta': (forall w, inc w B -> exists2 z, inc z A & w = h z). rewrite HA HB; move => w /prod_of_substratesP [fgf dz iVV]. exists (Lg (substrate r) (fun i => Vf (inverse_fun (oi i))(Vg w (fj i)))). apply /prod_of_substratesP;split => //; [ fprops | bw | ]. rewrite - sr => i isr; bw. move: (oip _ isr) => [_ _ [boi soi toi] _ ]. rewrite - soi; apply: inverse_Vis =>//; rewrite toi. apply: iVV; rewrite - sr'; apply: (fjs _ isr). rewrite /h; apply: fgraph_exten; [ exact | fprops | bw ; ue | ]. rewrite dz - sr'; move=> x xdw /=; move: (fis _ xdw) => fisr. bw; move: (oip _ fisr) => [_ _ [boi soi toi] _ ]. rewrite /fj (fip _ xdw) inverse_V // toi (fip _ xdw); apply: iVV; ue. have hi: (forall z z', inc z A -> inc z' A -> h z = h z' -> z = z'). rewrite HA => z z' zA zA' p3; apply: (setXb_exten zA zA'). hnf; bw;move=> i idg; move: (prod_of_substrates_p zA idg) =>p4. have p5 := (prod_of_substrates_p zA' idg). rewrite - sr in idg; move: (fij _ idg)(fjs _ idg) => p6 p7. move: (f_equal (Vg ^~(fj i)) p3); rewrite /h; bw; rewrite p6. move: (oip _ idg) => [_ _ [[[_ ioi] _] soi toi] _ ]. apply: ioi; ue. have ta2: (lf_axiom h A B) by []. exists (Lf h A B). split => //; [ by split; aw;apply: lf_bijective | hnf; aw]. move=> x y xA yA; aw; split. move /(orprod_gleP oa) => [_ _ ha]; apply /(orprod_gleP oa'). rewrite -HB; split => //; try apply: ta =>//; case:ha => ha. by left; rewrite ha. move: ha => [j [jst jlt ieq]]; right. move: (fjs _ jst)(fij _ jst) => fjst fijt; rewrite /h;ex_tac. by bw;rewrite fijt; apply: (order_isomorphism_sincr (oip _ jst)) => //. move=> i ifj. have isr: inc i (substrate r') by order_tac. bw;rewrite (ieq (fi i)) // - fijt; apply /(order_isomorphism_siso oif); [by rewrite srf; apply: fis | ue | rewrite ! fip //]. move /(orprod_gleP oa') => [_ _ ha]; apply /(orprod_gleP oa). rewrite - HA;split => //. case:ha=> aux; first by left; apply: hi =>//. right; move: aux => [j [jsr jlt jle]]. move: (fip _ jsr)(fis _ jsr) => fipa fisa. ex_tac. move: (oip _ fisa) => [_ _ [_ soi toi] _ ]. apply /(order_isomorphism_siso (oip _ fisa)); try (rewrite soi; apply: prod_of_substrates_p; ue); move: jlt; rewrite /h fipa; bw. move=> i lti. have isr: inc i (substrate r) by order_tac. move: (isr) => isr1. move: (oip _ isr) => [_ _ [[[_ ioi] _] soi toi] _ ]. apply: ioi. move: xA isr; rewrite soi sr HA; apply: prod_of_substrates_p. move: yA isr; rewrite soi sr HA; apply: prod_of_substrates_p. rewrite - srf in isr fisa. move /(order_isomorphism_siso oif isr fisa): lti; rewrite fip // => aux. by move: (jle _ aux); rewrite /h; bw; try order_tac; rewrite fij //. Qed. Lemma orprod_invariant2 r g g': worder r -> substrate r = domain g -> substrate r = domain g' -> (forall i, inc i (substrate r) -> (Vg g i) \Is (Vg g' i)) -> (order_prod r g) \Is (order_prod r g'). Proof. move=> wor sr sr' alo. have or:=proj1 wor. apply: (orprod_invariant1 (conj wor sr) (conj or sr') (identity_is or)). by move=> i isr; rewrite identity_V //; apply: alo. Qed. Lemma orprod_invariant3 r g: worder_on r (domain g) -> worder_fam g -> finite_set (substrate r) -> ordinal (order_prod r g) = oprod r (Lg (substrate r) (fun i => ordinal (Vg g i))). Proof. move => [wor sr] alo fsr. have or:= proj1 wor. rewrite /oprod; apply: ordinal_o_isu1; first by apply: orprod_wor. apply: orprod_wor; bw; first by split; bw. hnf; bw; move=> i isr; bw. rewrite sr in isr; apply: (ordinal_o_wor (OS_ordinal (alo _ isr))). apply: orprod_invariant2=> //; bw. rewrite sr;move=> i isr ; bw; apply: (ordinal_o_is (alo _ isr)). Qed. Lemma orprod_invariant4 r1 r2 r3 r4: r1 \Is r3 -> r2 \Is r4 -> (order_prod2 r1 r2) \Is (order_prod2 r3 r4). Proof. move=> h1 h2; rewrite /order_prod2. move:cdo_wor => [pa pb]. apply: orprod_invariant2; rewrite ? pb; bw => i itp; try_lvariant itp. Qed. Lemma orsum_invariant5 a b c: worder a -> worder b -> (order_sum2 a b) \Is c -> (ordinal a) +o (ordinal b) = ordinal c. Proof. move=> oa ob h. rewrite /osum2; apply: ordinal_o_isu1. apply: orsum2_wor. apply: (ordinal_o_wor (OS_ordinal oa)). apply: (ordinal_o_wor (OS_ordinal ob)). move: h (orsum2_wor oa ob); apply: worder_invariance. apply: orderIT h; apply: orsum_invariant4. apply: orderIS; apply: (ordinal_o_is oa). apply: orderIS; apply: (ordinal_o_is ob). Qed. Lemma orprod_invariant5 a b c: worder a -> worder b -> (order_prod2 a b) \Is c -> (ordinal a) *o (ordinal b) = ordinal c. Proof. move=> oa ob h. rewrite /oprod2; apply: ordinal_o_isu1. apply: orprod2_wor. apply: (ordinal_o_wor (OS_ordinal oa)). apply: (ordinal_o_wor (OS_ordinal ob)). move: h (orprod2_wor oa ob); apply: worder_invariance. apply: orderIT h; apply: orprod_invariant4. apply: orderIS; apply: (ordinal_o_is oa). apply: orderIS; apply: (ordinal_o_is ob). Qed. Lemma oprod_pr1 a b c: ordinalp a -> ordinalp b -> (ordinal_o b) \Is c -> a *o b = osum c (cst_graph (substrate c) a). Proof. move=> ota otb ibc. have wo0:= (ordinal_o_wor ota). have wo1 := (ordinal_o_wor otb). have wo2:= (worder_invariance ibc wo1). rewrite /oprod2 /osum {1} /cst_graph; bw. apply: ordinal_o_isu1. by apply: orprod2_wor; apply: ordinal_o_wor. apply: orsum_wor; [split; bw | hnf;bw]. move=> i isc; bw; apply: (ordinal_o_wor ota). move: (order_prod_pr (worder_or wo0)(worder_or wo1)). set aux := order_sum _ _ . move=> h; apply: (orderIT h). have [f isf] := ibc. rewrite /aux /cst_graph; apply: (@orsum_invariant1 _ _ f); bw. rewrite ordinal_o_sr; apply: sub_osr. split; fprops. move: isf => [_ _ [[[ff _] _] sf tf] _]. rewrite - sf => i id. move: (Vf_target ff id); rewrite tf=> vt;bw; apply: orderIR; fprops. Qed. Lemma osum_set0 r x: domain x = emptyset -> osum r x = \0o. Proof. move=> sre. rewrite /osum sre /Lg funI_set0 /order_sum; set g := graph_on _ _. suff: g = emptyset by move => ->; exact ordinal0_pr. apply/set0_P => t /Zo_S /setX_P [_ _] /du_index_pr1; rewrite domain_set0. by move => [/in_set0]. Qed. Lemma oprod_set0 r x: domain x = emptyset -> oprod r x = \1o. Proof. move=> sre. have si: singletonp (prod_of_substrates emptyset). by apply: setX_set1; hnf;rewrite /fam_of_substrates; bw => t/in_set0. rewrite /oprod sre /Lg funI_set0. rewrite /order_prod;move: si => [y ->]; rewrite /graph_on. set s1 := Zo _ _. suff: s1 = singleton (J y y) by move => ->; exact:ordinal1_pr. apply:set1_pr. apply /Zo_P; split; first by apply: setXp_i; apply /set1_P. move => j; set s := Zo _ _. have ->: s = emptyset by apply /set0_P => t /Zo_S /funI_P [z] /in_set0. rewrite /induced_order /coarse setX_0l setI2_0 // /least /substrate. by rewrite domain_set0 range_set0 setU2_id; move => [] /in_set0. by move => z /Zo_S /setX_P [pz /set1_P pa /set1_P pb]; rewrite - pz pa pb. Qed. Lemma osum_set1 r x e: order_on r (domain x) -> substrate r = singleton e -> ordinalp (Vg x e) -> osum r x = Vg x e. Proof. set w := Vg x e;move=> [or sr] srs otve. have dxe: domain x = singleton e by rewrite - sr srs. have edx: (inc e (domain x)) by rewrite dxe; fprops. have wor:= (worder_set1 (conj or srs)). have ove:= (ordinal_o_wor otve). rewrite /osum. set g := Lg _ _. have osa: orsum_ax r g. rewrite /g; hnf; bw;split => //;hnf; bw. rewrite dxe => i /set1_P ->; bw ; fprops. have wos: worder (order_sum r g). rewrite /g;apply: orsum_wor; first by split; bw. hnf; bw; rewrite dxe; move=> i /set1_P ->; bw; fprops. apply: (ordinal_o_isu2 wos otve). set (E:= substrate (order_sum r g)); set (F := substrate (ordinal_o w)). have He:E =sum_of_substrates g by rewrite /E orsum_sr //. have Hf:F = w by rewrite /F; apply: (ordinal_o_sr w). have uE: (forall u, inc u E <-> [/\ pairp u, Q u = e &inc (P u) F]). move=> u; rewrite He /g; split. move=> us; move: (du_index_pr1 us) => []. rewrite Lg_domain; move=> Qu; bw. move: Qu; rewrite dxe=> /set1_P -> pa pb; split => //; ue. move => [pu Qu Pu]. rewrite - pu Qu; apply: disjointU_pi; bw. have ta: (lf_axiom P E F) by move=> t /uE [_]. exists (Lf P E F). split; fprops; first (hnf;split; aw). apply: lf_bijective => //. move=> u v =>/uE [pu Qu Pu] /uE [pv Qv Pv] sp. apply: pair_exten =>//; ue. move=> y ys; exists (J y e); aw => //; apply /uE; aw;split;fprops. hnf; aw => a b aE bE; aw. move: (aE)(bE) => /uE [pu Qu Pu] /uE [pv Qv Pv]. have aux: inc (Q a) (domain x) by rewrite dxe Qu ; fprops. have <-: (Vg g (Q a)) = ordinal_o (Vg x e) by rewrite /g; bw; ue. split. by move /orsum_gleP => [_ _]; case; move => [_] //; rewrite Qu Qv. move => h; apply /orsum_gleP;split; rewrite - ? He //; right;split => //; ue. Qed. Lemma oprod_set1 r x e: order_on r (domain x) -> substrate r = singleton e -> ordinalp (Vg x e) -> oprod r x = Vg x e. Proof. move=> [or sr] srs otve. have wor :=(worder_set1 (conj or srs)). have dxe: domain x = singleton e by rewrite - sr srs. have edx: (inc e (domain x)) by rewrite dxe; fprops. have ove:= (ordinal_o_wor otve). rewrite /oprod. set g := Lg _ _. have la: (orprod_ax r g). rewrite /g; split => //; first by bw; ue. hnf; bw; move=> i; rewrite dxe=> id; bw; aw; fprops. have ora := (orprod_or la). have wos: worder(order_prod r g). apply: orprod_wor=> //; first by split => //; rewrite /g; bw. hnf; rewrite /g; bw; rewrite dxe; move=> i /set1_P ->; bw; fprops. rewrite srs; apply: set1_finite. apply: (ordinal_o_isu2 wos otve). move: (orprod_sr la). set E := substrate (order_prod r g). set F := substrate (ordinal_o (Vg x e)). have Hf: F = Vg x e by rewrite /F; apply: ordinal_o_sr. have Hf': F = substrate (Vg g e) by rewrite /g; bw. move=> slo; move: (slo). rewrite /prod_of_substrates/fam_of_substrates=> slo'. have dg: domain g = singleton e by rewrite /g ; bw. have eg: inc e (domain g) by rewrite /g ; bw. have ta: lf_axiom (Vg ^~ e) E F. move=> t te; move: te eg; rewrite slo Hf'; apply: prod_of_substrates_p. have Hc:forall a b, inc a E-> inc b E -> Vg a e = Vg b e -> a = b. move=> a b; rewrite slo' dg => aE bE sV. by apply: (setXb_exten aE bE); bw; move=> i /set1_P ->. exists (Lf (Vg ^~e) E F). hnf;rewrite /bijection_prop lf_source lf_target; split;fprops. split; aw;apply: lf_bijective =>//. move=> y ys; exists (cst_graph (singleton e) y); bw; fprops. rewrite slo' dg; bw; apply /setXb_P; fprops;split;fprops; bw. by move=> i /set1_P ->; bw; fprops; rewrite - Hf'. hnf; aw; move=> a b aE bE; aw. have qa: fgraph (Lg (domain g) (fun i => substrate (Vg i g))) by fprops. have aux: (ordinal_o (Vg x e)) = Vg g e by rewrite /g; bw. split. move/(orprod_gleP la) => [_ _]; case. have orve:= (worder_or ove). move=> ->; order_tac. move: bE; rewrite slo'; move /setXb_P=> [fgb db]. rewrite - db => aa. have ed: inc e (domain b) by rewrite db dg; bw; fprops. by move: (aa _ ed); bw; rewrite aux. rewrite sr dxe;move=> [j [jsr]]; bw; move /set1_P: (jsr) => <-. by move => [jle _] _; move: jle; rewrite /g; bw; rewrite dxe. move=> h; apply /(orprod_gleP la); rewrite - slo;split => //. case: (equal_or_not a b) => ab; [left => // | right; exists e; split]. by rewrite sr. bw; split => //; [ by rewrite - aux | dneg nab; apply: Hc =>// ]. move=> i [lie]. have : inc i (substrate r) by order_tac. by rewrite srs; move => /set1_P => ->. Qed. Lemma osum_unit1 r g j: orsum_ax r g -> sub j (domain g) -> (forall i, inc i ((domain g) -s j) -> Vg g i = emptyset) -> (order_sum r g) \Is (order_sum (induced_order r j) (restr g j)). Proof. move => oa sj alz; move: (oa) => [or sr alo]. have dr: (domain (restr g j)) = j by bw. have sj1: sub j (substrate r) by ue. have oa': orsum_ax (induced_order r j) (restr g j). have [pa pb]:= (iorder_osr or sj1). hnf; rewrite pb;split => //; hnf;rewrite dr. move=> i id; bw; apply: (alo _ (sj _ id)). have o1: order (order_sum r g) by fprops. have o2: order (order_sum (induced_order r j) (restr g j)) by fprops. set E := substrate (order_sum r g). set F := substrate (order_sum (induced_order r j) (restr g j)). have EF: E = F. set_extens z; rewrite /E/F; bw. move => zs; move: (du_index_pr1 zs) => [Qd Pd pz]. have ->: z = J (P z) (Q z) by aw. case: (p_or_not_p (inc (Q z) (domain (restr g j)))) => aux. apply: disjointU_pi => //; bw; ue. have Qx: inc (Q z) ((domain g) -s j) by bw;ue. have Ve := (alz _ Qx). by move:Pd;rewrite Ve (proj2 set0_wor) => /in_set0. move => zs; move: (du_index_pr1 zs); rewrite dr; move => [Qd Pd pz]. have ->: z = J (P z) (Q z) by aw. apply: disjointU_pi => //; [ by bw; apply: sj | move: Pd; bw; ue ]. exists (identity E). hnf; rewrite/bijection_prop identity_s identity_t; split => //. split => //;apply: identity_fb. have a1: forall x, inc x F -> inc (Q x) j. move=> x; rewrite /F; bw => xs; move: (du_index_pr1 xs)=> [aux _]; ue. hnf; aw; move=> x y xE yE; bw. rewrite orsum_gleP orsum_gleP. have <-: E = (sum_of_substrates g) by rewrite /E; bw. have <-: F = (sum_of_substrates (restr g j)) by rewrite /F; bw. rewrite /order_sum_r -EF /glt. have aux: (gle (induced_order r j) (Q x) (Q y) <-> (gle r (Q x) (Q y))). rewrite/gle/related/induced_order; split. by move /setI2_P => []. move=> h; apply /setI2_P; split => //; apply: setXp_i; apply: a1; ue. have -> //: Vg (restr g j) (Q x) = (Vg g (Q x)). bw; apply: a1; ue. by split; move => [pa pb pc];split => //; case: pc => //; try (by right); move => [/aux pd pe];left. Qed. Lemma osum_unit2 r g j: worder_on r (domain g) -> ordinal_fam g -> sub j (domain g) -> (forall i, inc i ((domain g) -s j) -> Vg g i = \0o) -> osum r g = osum (induced_order r j) (restr g j). Proof. move => [wor sr] odf sj alne. have or:= proj1 wor. apply: ordinal_o_isu1. apply: orsum_wor; [split; bw | hnf; bw => i idg; bw; fprops]. apply: orsum_wor. split; bw;first by apply: induced_wor => //; ue. aw; ue. hnf; bw; move=> i idg; bw; fprops. set g1:= (Lg (domain g) (fun z => ordinal_o (Vg g z))). set g2:= Lg _ _; have ->: g2 = (restr g1 j). by rewrite /g1 /g2; bw; apply: Lg_exten => x xd; bw; apply: sj. have dg1: domain g1 = domain g by rewrite /g1; bw. apply: osum_unit1. split; [exact | ue | ]. by hnf; rewrite dg1; move=> i idg; rewrite /g1; bw; apply: ordinal_o_or. ue. rewrite dg1; move=> i ic; rewrite /g1; bw. by rewrite (alne _ ic); apply: empty_substrate_zero; rewrite ordinal_o_sr. by move: ic => /setC_P [ok _]. Qed. Lemma oprod_unit1 r g j: orprod_ax r g -> sub j (domain g) -> (forall i, inc i ((domain g) -s j) -> singletonp (substrate (Vg g i))) -> (order_prod r g) \Is (order_prod (induced_order r j) (restr g j)). Proof. move => oa sj alse; move: (oa) => [wor sr alo]. have dr: (domain (restr g j)) = j by bw. have sj1: sub j (substrate r) by ue. have [or _] := (wor). have oa': orprod_ax (induced_order r j) (restr g j). hnf; aw; split => //; first by apply: induced_wor => //. hnf;rewrite dr;move=> i id;bw; apply: (alo _ (sj _ id)). have o1: order (order_prod r g) by fprops. have o2: order (order_prod (induced_order r j) (restr g j)) by fprops. set E := substrate (order_prod r g). set F := substrate (order_prod (induced_order r j) (restr g j)). have Ep: E = prod_of_substrates g by rewrite /E ; bw. have Fp: F = prod_of_substrates (restr g j) by rewrite /F; bw. have fg1: fgraph (fam_of_substrates (restr g j)) by rewrite /fam_of_substrates ;fprops. have fg2: fgraph (fam_of_substrates g) by rewrite /fam_of_substrates; fprops. have rd: j = domain (restr g j) by bw. have ta: lf_axiom (fun z => restr z j) E F. move=> z; rewrite Ep Fp; move /prod_of_substratesP => [fgz dz iVV]. have sj2: sub j (domain z) by ue. apply /prod_of_substratesP;split;fprops; bw. by move=> i ij; bw; apply: iVV; apply: sj. have specs: forall i x y, inc i (domain g) -> ~ inc i j -> inc x E -> inc y E -> Vg x i = Vg y i. move => i x y idg nij ; rewrite Ep. move /prod_of_substratesP => [fgu du up]. move /prod_of_substratesP => [fgv dv vp]. have xc: (inc i ((domain g) -s j)) by apply /setC_P; split => //. move: (up _ idg) (vp _ idg) => pa pb. by move: (alse _ xc) => /singletonP [_]; apply. have ri: forall u v, inc u E -> inc v E -> restr u j = restr v j -> u = v. move=> u v uE vE. move: (uE)(vE); rewrite Ep. move /prod_of_substratesP => [fgu du up]. move /prod_of_substratesP => [fgv dv vp] sar. apply: fgraph_exten => //; [ ue | move => x ; rewrite du => xdg]. case: (inc_or_not x j). move=> xj; move: (f_equal (Vg ^~ x) sar); bw. move=> nxj; apply: specs => //. exists (Lf (fun z => restr z j) E F). hnf; aw;split => //. split; aw;apply: lf_bijective => //. move=> y; rewrite Ep Fp; move /prod_of_substratesP=> [fgy dy iVV]. set x := (Lg (domain g) (fun z => Yo (inc z j) (Vg y z) (rep (substrate (Vg g z))))). have fgx: fgraph x by rewrite /x; fprops. have dx: domain x = domain g by rewrite /x; bw. exists x. apply /prod_of_substratesP;split => // => i idx; rewrite /x; bw; Ytac xj. rewrite- rd in iVV; move: (iVV _ xj); bw. have xc: (inc i ((domain g) -s j)) by apply /setC_P; split => //. by move: (alse _ xc) => /singletonP [ne1 _]; apply: rep_i. apply: fgraph_exten; fprops; rewrite dy; bw; bw => i ij; rewrite /x; bw. by Ytac0. fprops. have sjr: sub j (substrate r) by ue. hnf; aw; move=> x y xE yE; aw. move: (xE)(yE); rewrite Ep. move /prod_of_substratesP => [fgx dx xp]. move /prod_of_substratesP => [fgy dy yp]. have pa : substrate (induced_order r j) = j by rewrite iorder_sr. have sjx: sub j (domain x) by rewrite dx. have sjy: sub j (domain y) by rewrite dy. split. move /(orprod_gleP oa) => [_ _ h]; apply /(orprod_gleP oa'). rewrite -Fp;split; [by apply: ta | by apply: ta | ]. case: h; first by move=> -> ; left. move => [k [ksr klt kle]]; right; rewrite pa;exists k. case: (inc_or_not k j) => kj. split => //; bw; move => i ilt. move: (iorder_gle4 ilt) => [ij _]; bw. apply: (kle _ (iorder_gle2 ilt)). rewrite sr in ksr; move: klt => [_ []]. apply: specs => //. move /(orprod_gleP oa') => [_ _ h]; apply /(orprod_gleP oa). rewrite -Ep; split => //; case: h; first by move => h;left; apply: ri. rewrite pa;move=> [k [ksr klt kle]]; right; exists k. rewrite sr; split; [by apply: sj | by move: klt; bw | ]. move=> i [lik nik]; case: (inc_or_not i j) => ij. have lik1: glt (induced_order r j) i k by split => //; apply/iorder_gleP. move: (kle _ lik1); bw. apply: specs => //; rewrite - sr;order_tac. Qed. Lemma oprod_unit2 r g j: worder_on r (domain g) -> ordinal_fam g -> sub j (domain g) -> finite_set (substrate r) -> (forall i, inc i ((domain g) -s j) -> Vg g i = \1o) -> oprod r g = oprod (induced_order r j) (restr g j). Proof. move=> [wor sr] ofg jd fs alz. have or: order r by fprops. have jsr: sub j (substrate r) by ue. rewrite /oprod; apply: ordinal_o_isu1. by apply: orprod_wor;[bw; split | hnf; bw => i idg; bw; fprops |]. apply: orprod_wor; bw. split; [apply: induced_wor => // |]; aw. hnf; bw => i idg; bw; fprops. aw; apply: (sub_finite_set jsr fs). set g1:= (Lg (domain g) (fun z => ordinal_o (Vg g z))). have ->: (Lg (domain (restr g j)) (fun z => ordinal_o (Vg (restr g j) z)) = (restr g1 j)). by rewrite /g1;bw; apply: Lg_exten => x xd /=; bw;apply: jd. have dg1: domain g1 = domain g by rewrite /g1; bw. apply: oprod_unit1; rewrite /orprod_ax ? dg1 //. split => //;move=> i idg; rewrite /g1; bw; fprops; ue. move=> i ic; move /setC_P: (ic) => [ic1 _]. by rewrite /g1; bw; rewrite (alz _ ic) (ordinal_o_sr ); exists emptyset. Qed. Lemma orsum_assoc_iso r g r' g': orsum_ax r g -> orsum_ax r' g' -> r = order_sum r' g' -> let order_sum_assoc_aux := fun l => order_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in let order_sum_assoc := order_sum r' (Lg (domain g') order_sum_assoc_aux) in order_isomorphism (Lf (fun x=> J (J (P x) (P (Q x))) (Q (Q x))) (sum_of_substrates g) (substrate (order_sum_assoc))) (order_sum r g) (order_sum_assoc). Proof. move=> oa oa' oa_link F G. move: (oa) => [or sr alo]. move: (oa') => [or' sr' alo']. have alo'' :forall l, inc l (substrate r') -> orsum_ax (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))). move=> l ls; split => //; bw; first by apply: alo' =>//; ue. hnf; bw;move => i isg; bw;apply: alo; rewrite - sr oa_link. rewrite orsum_sr //; apply: disjoint_union_pi1 =>// ; ue. have order_sum_assoc_aux2 :forall l, inc l (domain g') -> order (F l). move=> l ldg'; rewrite /F; rewrite - sr' in ldg'; fprops. have oa'' : orsum_ax r' (Lg (domain g') (fun l=> F l)). hnf; bw; split => //; hnf;bw. by move => i idf; bw; apply: order_sum_assoc_aux2. have org : order G by rewrite /G; fprops. have ta: (lf_axiom (fun x => J (J (P x) (P (Q x))) (Q (Q x))) (sum_of_substrates g) (substrate G)). move=> x xs; rewrite /G; aw; move: (du_index_pr1 xs) => [Qd Ps px]. move: Qd;rewrite - sr oa_link; bw => Qd. move: (du_index_pr1 Qd) => [QQd PQs pQ]. apply: disjoint_union_pi1; bw. rewrite /F;bw; first by apply: disjoint_union_pi1; bw; rewrite pQ. apply: alo''; ue. set(FF:= Lf (fun x => J (J (P x) (P (Q x))) (Q (Q x))) (sum_of_substrates g) (substrate G)). have injF: injection FF. apply: lf_injective => //. move => u v us vs eq; move: (pr1_def eq) (pr2_def eq)=> eq1 eq2. move: (pr1_def eq1) (pr2_def eq1) => eq3 eq4. move: (du_index_pr1 us) (du_index_pr1 vs) => [Qu _ pu][Qv _ pv]. apply: pair_exten =>//. move: Qu Qv;rewrite - sr oa_link; bw=> Qu Qv. move: (du_index_pr1 Qu)(du_index_pr1 Qv) => [_ _ pqu][_ _ pqv]. apply: pair_exten => //. have bF: (bijection FF). split =>//; apply: lf_surjective => //. move=> y; rewrite /G; bw => yG. move: (du_index_pr1 yG); rewrite Lg_domain=> [[Qd]]; bw; move=> Py Qpy. rewrite sr' in alo''; move: (alo'' _ Qd) => al. move: (Py); rewrite /F; bw => paux. move: (du_index_pr1 paux);rewrite Lg_domain=> [[PQd]]; bw; move=> PPy Ppy. set (x:= J (P (P y)) (J (Q (P y)) (Q y))). have xs: (inc x (sum_of_substrates g)). rewrite /x;apply: disjoint_union_pi1 =>//. rewrite - sr oa_link; bw; apply: disjoint_union_pi1 =>//. by ex_tac; rewrite /x ; aw; rewrite Ppy Qpy. rewrite /FF;hnf; split; fprops; first split; aw; bw. hnf; aw;move=> x y xs ys; aw. set gx := (J (J (P x) (P (Q x))) (Q (Q x))). set gy := (J (J (P y) (P (Q y))) (Q (Q y))). move: (du_index_pr1 xs)(du_index_pr1 ys) => [Qu Pu pu][Qv Pv pv]. move: Qu Qv;rewrite - sr oa_link (orsum_sr oa') => Qu Qv. move: (du_index_pr1 Qu)(du_index_pr1 Qv) => [QQx PQx pqu][QQy pQy pqv]. have aux3: (J (P (Q x)) (Q (Q x))) = Q x by aw. have aux4: (J (P (Q y)) (Q (Q y))) = Q y by aw. set P1:=inc gx (sum_of_substrates (Lg (domain g') F)). set P2:=inc gy (sum_of_substrates (Lg (domain g') F)). have p1p: P1. rewrite /P1; apply: disjoint_union_pi1; bw. have Qs: inc (Q (Q x)) (substrate r') by ue. rewrite /F; bw; try apply: alo'' =>//. apply: disjoint_union_pi1; [ rewrite Lg_domain // | bw; ue]. have p2p: P2. rewrite /P2; apply: disjoint_union_pi1; bw. have Qs: inc (Q (Q y)) (substrate r') by ue. rewrite /F; bw; try apply: alo'' =>//. apply: disjoint_union_pi1; [ rewrite Lg_domain // | bw; ue]. have ww: Q gx = Q (Q x) by rewrite /gx; aw. have ww1: Q gy = Q (Q y) by rewrite /gy; aw. split; move /orsum_gleP => [_ _ h]; apply /orsum_gleP; split => //. have aux1: inc (Q (Q x)) (substrate r') by ue. hnf; rewrite ww ww1; bw; rewrite /gx !pr1_pair. move: (alo'' _ aux1) => aux2. case: h. move => [] /orsum_gleP [Qx1 Qx2 hr] nxy. case: hr; first by left. move => [aa bb]; right; split => //; bw; apply /orsum_gleP;split => //. apply: disjoint_union_pi1; bw; ue. rewrite aa;apply: disjoint_union_pi1; bw; ue. hnf; rewrite !pr2_pair (LVg_E _ PQx) !pr1_pair aux3. case: (equal_or_not (P (Q x)) (P (Q y)))=> aux5; last by left;split. case: nxy; rewrite -aux3 -aux4 aa aux5 //. move=> [sq le1]; right;rewrite - sq; split => //. bw;apply /orsum_gleP;split => //. apply:disjoint_union_pi1; bw; ue. rewrite sq;apply: disjoint_union_pi1; bw; ue. hnf; rewrite !pr2_pair (LVg_E _ PQx) !pr1_pair aux3; right;split => //. case:h; rewrite ww ww1. move=> [le ne] ; left; split; last by dneg ne1; ue. by apply /orsum_gleP;split => //; left; split. move=> [qq]; bw. have Qs: inc (Q (Q x)) (substrate r') by ue. move /orsum_gleP => [_ _]. case; rewrite /gx /gy ! pr1_pair ! pr2_pair; move => [hyp1 hyp2]. have aux2: Q x <> Q y by dneg ne1; ue. left; split => //; apply /orsum_gleP;split => //; right;split => //. right; split => //; first by apply: pair_exten =>//. by move: hyp2; bw;rewrite pqu. Qed. Lemma orprod_assoc_iso r g r' g': orprod_ax r g -> orsum_ax r' g' -> r = order_sum r' g' -> worder r' -> (forall i, inc i (domain g') -> worder(Vg g' i)) -> let order_sum_assoc_aux := fun l => order_prod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in let ordinal_prod_assoc := order_prod r' (Lg (domain g') order_sum_assoc_aux) in order_isomorphism (Lf (fun z => Lg (domain g') (fun l => Lg (substrate (Vg g' l)) (fun j => Vg z (J j l)))) (prod_of_substrates g) (substrate (ordinal_prod_assoc))) (order_prod r g) (ordinal_prod_assoc). Proof. move=> la oa oa_link wor' alwo F G. move: (oa) => [or' sr' alo']. move: (la) => [wor sr alo]. have dgpr: forall i j, inc i (domain g') -> inc j (substrate (Vg g' i)) -> inc (J j i) (domain g). move=> i j id jd; rewrite - sr oa_link; bw; apply: disjoint_union_pi1 =>//. have la1: forall i, inc i (domain g') -> orprod_ax (Vg g' i) (Lg (substrate (Vg g' i)) (fun i0 : Set => Vg g (J i0 i))). move=> i idg; split;fprops; bw. hnf; bw; move=> j js; bw; apply: alo; apply: dgpr =>//. have la': orprod_ax r' (Lg (domain g') F). split => //;hnf;bw;move=> i idg'; rewrite /F; bw; fprops. have oG: order G by rewrite /G; fprops. have s1: substrate (order_prod r g) = prod_of_substrates g by bw. have sG1: substrate G = productb (Lg (domain g') (fun i => substrate (F i))). rewrite /G; bw; rewrite /prod_of_substrates /fam_of_substrates; bw. apply: f_equal; apply: Lg_exten; move=> i idg /=; bw. have sG0: substrate G = (prod_of_substrates (Lg (domain g') F)). rewrite /G orprod_sr // /prod_of_substrates /fam_of_substrates; bw. have sG2: substrate G = productb (Lg (domain g') (fun i => productb (Lg (substrate (Vg g' i))(fun i0 : Set => substrate (Vg g (J i0 i)))))). rewrite sG1; f_equal; apply: Lg_exten. move=> i idg; rewrite /F;bw; last by apply: la1 =>//. rewrite /prod_of_substrates /fam_of_substrates; bw. f_equal; apply: Lg_exten; move=> x xs /=; bw. pose h z := Lg (domain g') (fun l => Lg (substrate (Vg g' l)) (fun j => Vg z (J j l))). have p1: forall z, inc z (prod_of_substrates g) -> inc (h z) (substrate G). move=> z zp; move: (zp) => /prod_of_substratesP [fgz dz iVV]. rewrite sG2; apply /setXf_P; rewrite /h;split;[fprops | bw | ]. move=> i idg; bw; apply /setXf_P;split;fprops; bw. move => j js; bw; apply: iVV; exact (dgpr _ _ idg js). have p2: forall a b, inc a (prod_of_substrates g) -> inc b (prod_of_substrates g) -> h a = h b -> a = b. move=> a b /prod_of_substratesP [fga da iVVa] /prod_of_substratesP [fgb db iVVb] eqn. apply: fgraph_exten =>//; try ue; move=> x xda. move: xda; rewrite da - sr oa_link; bw => xsr. move: (du_index_pr1 xsr) => [Qx Px px]. move: (f_equal (Vg ^~ (Q x)) eqn); bw => eq2. by move: (f_equal (Vg ^~ (P x)) eq2); rewrite /h;bw; rewrite px. have p3: forall x, inc x (substrate G) -> exists2 z, inc z (prod_of_substrates g) & x = (h z). move=> x;rewrite sG2 => /setXf_P [fgx dx iVVx]. exists (Lg (domain g) (fun w => Vg (Vg x (Q w)) (P w))). apply /prod_of_substratesP; split;fprops;bw; move=> i idg; bw. move : idg; rewrite - sr oa_link; bw => xsr. move: (du_index_pr1 xsr) => [Qx Px px]; move: (iVVx _ Qx); bw. move /setXf_P => [fg1 d1 ivv1]. by rewrite -{3} px; apply: ivv1. rewrite /h; symmetry;apply: fgraph_exten =>//;[ fprops | bw; ue | bw]. move=> j jdg /=; bw; move: (iVVx _ jdg) => /setXf_P [fgj dj iVV2]. apply: fgraph_exten; [ fprops | exact | bw; ue| bw]. move=> w ws /=; bw; [ aw | apply: dgpr =>//]. split;fprops; aw; first by split; aw => //;apply: lf_bijective => //. hnf; rewrite lf_source ; move=> a b ap bp; rewrite !lf_V //. split. move /(orprod_gleP la) => [_ _ ha]; apply/(orprod_gleP la'). split; first by rewrite - sG0; apply: p1. by rewrite - sG0; apply: p1. case: ha; first by move=> ->; left. move=> [j [jsr [jlt diff] jle]]; right. move: jsr; rewrite oa_link; bw => jsg'. move: (du_index_pr1 jsg') => [Qx Px px]. rewrite sr';ex_tac. have paux: forall c, inc c (prod_of_substrates g) -> inc (Vg (h c) (Q j)) (prod_of_substrates (Lg (substrate (Vg g' (Q j))) (fun i : Set => Vg g (J i (Q j))))). move=> i ic;move: (p1 _ ic); rewrite sG1. move /setXf_P=> [fgh dh ivv]; move: (ivv _ Qx); bw. rewrite /F orprod_sr //; apply: la1 => //. rewrite -/(h a) - /(h b); bw; rewrite /F ;split; last first. rewrite /h; bw; dneg aa; move: (f_equal (Vg ^~(P j)) aa);bw. rewrite px //. apply/(orprod_gleP (la1 _ Qx));split => //; try apply: paux => //. right; ex_tac; bw. rewrite /h; bw; by have ->: (J (P j) (Q j)) = j by aw. move=> i [ile ne]. have isr: inc i (substrate (Vg g' (Q j))) by order_tac. rewrite /h; bw; apply: jle; split; last by dneg aa; rewrite -aa; aw. rewrite oa_link; apply /orsum_gleP; split => //. apply: disjoint_union_pi1=> //. by right; aw. move=> i ilt. have idg: inc i (domain g') by rewrite - sr'; order_tac. rewrite /h; bw; apply: Lg_exten =>// k ks. apply: jle; split; last by move: ilt => [_ bad]; dneg aa; rewrite -aa; aw. rewrite oa_link; apply /orsum_gleP; split => //. apply: disjoint_union_pi1=> //. by hnf; aw; left. move => /(orprod_gleP la') [_ _ ha]; apply /(orprod_gleP la);split => //. case: ha; first by move=> eq; left; apply: p2. move=> [j [jsr jlt jle]]; right. rewrite sr' in jsr; move: jlt; rewrite /h /F; bw; move=> [le ns]. move: le; move /(orprod_gleP (la1 _ jsr)). move=> [p6 p7];case; first by move=> p8; case: ns. move=> [k [ks klt kle]]. rewrite sr; move: (dgpr _ _ jsr ks) => pd. ex_tac; first by move: klt; bw. move=> i [lei nei]; move: lei;rewrite oa_link=> lti. have : inc i (substrate (order_sum r' g')) by order_tac. bw=> iso; move: (du_index_pr1 iso) => [Qdg Psg' pi]. move: (orsum_gle1 lti); aw; case => ch. move: (jle _ ch); rewrite /h; bw => eq1. by move: (f_equal (Vg ^~(P i)) eq1); bw; rewrite pi. move: ch => [Qi aux]. have ->: i = J (P i) j by rewrite -Qi; aw. have aux2: glt (Vg g' j) (P i) k. rewrite -Qi; split => //; dneg aa; rewrite -aa - Qi pi; aw. rewrite Qi in Psg'; move: (kle _ aux2); bw. Qed. Lemma osum_assoc1 r g r' g': worder_on r (domain g) -> worder_on r' (domain g') -> ordinal_fam g -> worder_fam g' -> r = order_sum r' g' -> let order_sum_assoc_aux := fun l => osum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in osum r g = osum r' (Lg (domain g') (order_sum_assoc_aux)). Proof. move=> [wor sr] [wor' sr'] alB alw oal osa. have oa': orsum_ax r' g'. split;fprops; move => j jd; exact (proj1 (alw _ jd)). apply: ordinal_o_isu1. apply: orsum_wor; [split; bw| hnf; bw => i idg /=; bw; fprops]. apply: orsum_wor; [split; bw|hnf; bw=> i idg'; bw;apply: ordinal_o_wor]. rewrite /osa;apply: OS_sum=> //;first by split; bw; by apply: alw. hnf;bw;move => j js; bw;apply: alB;rewrite - sr oal (orsum_sr oa'). by apply: disjoint_union_pi1. set g'' := (Lg (domain g) (fun z => ordinal_o (Vg g z))). have oa: orsum_ax r g''. rewrite /g'';hnf; bw;split;fprops; hnf; bw; move=> i idg; bw; fprops. move: (orsum_assoc_iso oa oa' oal) => /=. pose aux' l:= order_sum (Vg g' l) (Lg (substrate (Vg g' l))(fun i=> Vg g'' (J i l))). set f:= Lf _ _ _. move => oi1; move: (oi1) => [o1 o2 _ _]. apply: (@orderIT (order_sum r' (Lg (domain g') aux'))); first by exists f. apply: orsum_invariant2 =>//; bw; fprops. rewrite sr';move=> i isr; bw; rewrite /osa /osum; bw. set s:= order_sum _ _. have -> : (aux' i = s). rewrite /aux' /s; f_equal; apply: Lg_exten;move=> j js. have pd: inc (J j i) (domain g). rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. rewrite /g''; bw. apply: ordinal_o_is; apply: orsum_wor; first by split; [ apply: alw | bw]. hnf; bw;move=> j js; bw;apply: ordinal_o_wor; apply: alB. rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. Qed. Lemma oprod_assoc1 r g r' g': worder_on r (domain g) -> worder_on r' (domain g') -> ordinal_fam g -> worder_fam g' -> r = order_sum r' g' -> finite_set (substrate r) ->finite_set (substrate r') -> (forall i, inc i (domain g') -> finite_set (substrate (Vg g' i))) -> let order_prod_assoc_aux := fun l => oprod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in oprod r g = oprod r' (Lg (domain g') order_prod_assoc_aux). Proof. move=> [wor sr] [wor' sr'] alB alw oal fs fs' alfs osa. have oa': orsum_ax r' g'. split;fprops; hnf; move => j jd; exact (proj1 (alw _ jd)). apply: ordinal_o_isu1; bw. apply: orprod_wor; hnf; bw => //; hnf; bw;move=> i idg; bw; fprops. apply: orprod_wor; hnf; bw => //; hnf; bw; move=> i idg'; bw. apply: ordinal_o_wor. rewrite /osa; apply:OS_prod; first by split; bw; fprops. hnf; bw;move => j js; bw; apply: alB; rewrite - sr oal (orsum_sr oa'). by apply: disjoint_union_pi1. by apply: alfs. set g'' := (Lg (domain g) (fun z => ordinal_o (Vg g z))). have oa: orprod_ax r g''. rewrite /g'';hnf; bw; split => //;hnf; bw; move=> i idg; bw; fprops. move: (orprod_assoc_iso oa oa' oal wor' alw) => /=. pose ax' l := order_prod (Vg g' l) (Lg (substrate (Vg g' l))(fun i=> Vg g'' (J i l))). set f:= Lf _ _ _. move => oi1; move: (oi1) => [o1 o2 _ _]. apply: (@orderIT (order_prod r' (Lg (domain g') ax'))); first by exists f. apply: orprod_invariant2 =>//; bw; fprops. rewrite sr';move=> i isr; bw; rewrite /osa /oprod; bw. set s:= order_prod _ _. have -> : (ax' i = s). rewrite /ax' /s; f_equal; apply: Lg_exten;move=> j js. have pd: inc (J j i) (domain g). by rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. rewrite /g''; bw. apply: ordinal_o_is;apply: orprod_wor; [ by split; bw; fprops | | fprops]. hnf; bw;move=> j js; bw; apply: ordinal_o_wor; apply: alB. rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1. Qed. Lemma osum_rec_def a b: ordinalp a -> ordinalp b -> a +o b = a \cup fun_image b (osum2 a). Proof. move => oa ob. case: (least_ordinal6 (fun b => a +o b = a \cup fun_image b (osum2 a)) ob). exact. set c := least_ordinal _ _;move => [oc prc]; case. set r := (order_sum2 (ordinal_o a) (ordinal_o c)). have woc:worder r by apply: orsum2_wor; apply: ordinal_o_wor. move: (sub_osr a) (sub_osr c) => [ora sra][orc src]. move: C1_ne_C0 C0_ne_C1 => ha hb. pose f x := Yo (Q x = C0) (P x) (a +o (P x)). have sr: substrate r = canonical_du2 a c by rewrite /r orsum2_sr // sra src. suff h: forall x, inc x (substrate r) -> f x = fun_image (segment r x) f. move:(ordinal_isomorphism_exists woc); rewrite -/(ordinal _) -/(a +o c). set ff := ordinal_iso r; move => [pa pb]. move: (pb) => [o1 o2 [[[fuf _] bf] sf tf] sif]; rewrite ordinal_o_sr in tf. rewrite - tf; set_extens w => wt. move /(proj2 bf):wt; rewrite sf; move => [p ps <-]; apply /setU2_P. rewrite -(transdef_tg3 woc (substrate_segment o1) h ps). move: ps; rewrite sr => /candu2P [pp hh]. rewrite /f; case: hh => [] [p1 p2]; rewrite p2;Ytac0;first by left. right;apply/funI_P; ex_tac. case /setU2_P:wt => wt1. have xsr: inc (J w C0) (substrate r) by rewrite sr; apply: candu2_pra. move: (transdef_tg3 woc (substrate_segment o1) h xsr). rewrite /f; aw; Ytac0 => ->; rewrite -/ff;Wtac. move /funI_P: wt1 => [z zc ->]. have xsr: inc (J z C1) (substrate r) by rewrite sr; apply: candu2_prb. move: (transdef_tg3 woc (substrate_segment o1) h xsr). rewrite /f; aw; Ytac0 => ->;rewrite -/ff;Wtac. move => x; rewrite sr =>/candu2P [px]; case=> [][Px Qx]; rewrite /f. Ytac0; set_extens t. move => tp; apply /funI_P; exists (J t C0); last by aw; Ytac0. move: (ordinal_transitive oa Px tp)(ordinal_hi oa Px) => ta opx. apply /segmentP; split. apply /orsum2_gleP; rewrite sra src; split => //. + by apply: candu2_pra. + by rewrite - px Qx; apply: candu2_pra. + constructor 1; aw; split => //; apply /ordo_leP; split => //. apply: (ordinal_transitive opx tp). move => h;case: (ordinal_irreflexive opx); rewrite -{1} h; aw. move => /funI_P [z /segmentP [/orsum2_gleP s1 nzx] ->]. move: s1; rewrite sra src; aw;move => [/candu2P [pz _] _]; case. + move => [q1 _ /ordo_leP [q5 q6 q7]]; Ytac0. case: (ordinal_sub (ordinal_hi oa q5) (ordinal_hi oa q6) q7) => //. move => sp; case: nzx; apply: pair_exten => //;ue. + by move => [_]; case. + by move => [_]; case. rewrite Qx; Ytac0; rewrite (prc _ Px);set_extens t. case /setU2_P. move => ta; apply /funI_P; exists (J t C0); last by aw; Ytac0. apply /segmentP; split; last by move => e; case: ha; rewrite - Qx -e; aw. apply /orsum2_gleP; rewrite sra src; split => //. + by apply: candu2_pra. + by apply /candu2P; split => //;right. + by constructor 3; rewrite Qx;aw. move => /funI_P [z zp ->];apply /funI_P; exists (J z C1); last by aw; Ytac0. move: (ordinal_transitive oc Px zp)(ordinal_hi oc Px) => ta opx. apply /segmentP; split; last first. move => h;case: (ordinal_irreflexive opx); rewrite -{1} h; aw. apply /orsum2_gleP; rewrite sra src; split => //. + by apply: candu2_prb. + by apply /candu2P; split => //;right. + constructor 2; rewrite Qx;aw; split => //; apply /ordo_leP; split => //. apply: (ordinal_transitive (ordinal_hi oc Px) zp). move /funI_P => [z /segmentP [/orsum2_gleP s1 s2] ->]. move: s1; rewrite sra src; aw;move => [/candu2P [pz p4] _ p5]; case: p4. by move => [Pz Qz]; Ytac0; apply /setU2_P; left. move => [Pz Qz]; rewrite Qz; Ytac0; case: p5; rewrite Qz; move => [] //. move => _ _ /ordo_leP [h1 h2 h3]; apply /setU2_P; right; apply /funI_P. exists (P z) => //. case: (ordinal_sub (ordinal_hi oc h1) (ordinal_hi oc h2) h3) => //. move => e; case: s2; apply: pair_exten => //;ue. Qed. Lemma oprod_rec_def a b: ordinalp a -> ordinalp b -> a *o b = fun_image (a\times b) (fun z => a *o (Q z) +o (P z)). Proof. move => oa ob. case: (least_ordinal6 (fun b => a *o b = fun_image (a\times b) (fun z => a *o (Q z) +o (P z))) ob) => //. set c := least_ordinal _ _;move => [oc prc]; case. set r := (order_prod2 (ordinal_o a) (ordinal_o c)). have woc:worder r by apply: orprod2_wor; apply: ordinal_o_wor. move: (sub_osr a) (sub_osr c) => [ora sra][orc src]. pose f x := a *o (Vg x C0) +o (Vg x C1). have sr: substrate r = product2 c a by rewrite /r orprod2_sr // sra src. suff h: forall x, inc x (substrate r) -> f x = fun_image (segment r x) f. move:(ordinal_isomorphism_exists woc); rewrite -/(ordinal _) -/(a *o c). set ff := ordinal_iso r; move => [pa pb]. move: (pb) => [o1 o2 [[[fuf _] bf] sf tf] sif]; rewrite ordinal_o_sr in tf. rewrite - tf; set_extens w => wt. move /(proj2 bf):wt; rewrite sf; move => [p ps <-]; apply /funI_P. move:(transdef_tg3 woc (substrate_segment o1) h ps) => <-. move: ps; rewrite sr => /setX2_P [fp dp vpa vpb]. exists (J (Vg p C1) (Vg p C0)); [ fprops | aw]. move /funI_P: wt => [z /setX_P [pz pza qzb] ->]. set x := variantLc (Q z) (P z). have xsr: inc x (substrate r). rewrite sr; rewrite /x;apply /setX2_P; split => //; bw; fprops. move: (transdef_tg3 woc (substrate_segment o1) h xsr). rewrite /f {1 2}/x; bw => ->;rewrite -/ff;Wtac. move => x; rewrite sr => /setX2_P [fp dp vpa vpb]; rewrite /f. set u := (Vg x C0); set v := (Vg x C1). have ou:=(ordinal_hi oc vpa). have ov:=(ordinal_hi oa vpb). rewrite (osum_rec_def (OS_prod2 oa ou) ov). set_extens t. have xca:inc x (product2 c a) by apply/setX2_P. case/setU2_P. rewrite (prc _ vpa); move =>/funI_P [z /setX_P[p za zb] ->]. apply /funI_P; exists (variantLc (Q z) (P z)); bw. move: (ordinal_hi ou zb)=> oqz. have sa: Q z <> Vg x C0. by move => s;apply: (ordinal_irreflexive oqz); rewrite {2} s. have qzc:=(ordinal_transitive oc vpa zb). apply/segmentP; split; last first. move => sv; move: (f_equal (Vg ^~C0) sv); bw. apply/(orprod2_gleP ora orc); rewrite sra src; split => //. + apply/setX2_P; split => //; bw; fprops. + right; bw; split => //; apply /ordo_leP; split => //. apply: (ordinal_transitive ou zb). move => /funI_P [z za ->];apply /funI_P; exists (variantLc u z); bw. have iza:=(ordinal_transitive oa vpb za). apply/segmentP; split; last first. move => sv; move: (f_equal (Vg ^~C1) sv); bw. by move => s;apply: (ordinal_irreflexive ov); rewrite -{1} s. apply/(orprod2_gleP ora orc); rewrite sra src; split => //. + apply/setX2_P; split => //; bw; fprops. + left;bw; split => //; apply /ordo_leP; split => //. apply: (ordinal_transitive ov za). move => /funI_P [z /segmentP[/(orprod2_gleP ora orc) za zb] ->] . move: za; rewrite sra src; move => [/setX2_P [z1 z2 z3 z4] _]; case. move => [sv /ordo_leP [z5 z6 z7]]; apply /setU2_P; right. apply/funI_P; rewrite sv; exists (Vg z C1) => //. case: (ordinal_sub (ordinal_hi oa z4) ov z7) => //h ; case: zb. by apply: fgraph_exten => //; [ue | rewrite z2 => uu; move /C2_P; case => ->]. move => [/ordo_leP [z5 z6 z7] sv]; apply /setU2_P; left. rewrite (prc _ vpa); apply /funI_P; exists (J (Vg z C1) (Vg z C0)); aw. move: (ordinal_hi oc z3)(ordinal_hi oc z5) => o1 o2. by apply :setXp_i => //; apply /oltP. Qed. Lemma oprod_zero r g: (exists2 i, inc i (domain g) & substrate (Vg g i) = emptyset) -> order_prod r g = emptyset. Proof. move=> [j jdg Vz]. apply /set0_P => q /Zo_P [] /setX_P [_ /setXf_P [fgy dy p]]. by move: (p _ jdg); rewrite Vz => /in_set0. Qed. Lemma oprod0r x: x *o \0o = \0o. Proof. rewrite /oprod2 /order_prod2 oprod_zero ?ordinal0_pr //. bw; exists C0 => //; bw; fprops. rewrite ordinal_o_set0;exact: (proj2(set0_wor)). Qed. Lemma oprod0l x: \0o *o x = \0o. Proof. rewrite /oprod2 /order_prod2 oprod_zero ?ordinal0_pr //. bw; exists C1 => //; bw; fprops. rewrite ordinal_o_set0;exact: (proj2(set0_wor)). Qed. Lemma osum0r x: ordinalp x -> x +o \0o = x. Proof. by move => ox; rewrite (osum_rec_def ox OS0) funI_set0 setU2_0. Qed. Lemma osucc_pr x: ordinalp x -> x +o \1o = osucc x. Proof. by move => ox; rewrite (osum_rec_def ox OS1) funI_set1 osum0r. Qed. Lemma osum0l x: ordinalp x -> \0o +o x = x. Proof. move => ox; case: (least_ordinal6 (fun x => \0o +o x = x) ox) => //. set c := least_ordinal _ _; move => [oc prc]; case. rewrite (osum_rec_def OS0 oc) set0_U2; set_extens t. move => /funI_P [z zc ->]; rewrite prc //. by move => tc; apply/funI_P; ex_tac; rewrite prc. Qed. Lemma oprod1r x: ordinalp x -> x *o \1o = x. Proof. move=> ox; rewrite (oprod_rec_def ox OS1). have h: forall t, inc t x -> t = x *o \0o +o t. move => t tx; rewrite oprod0r osum0l //; exact: (ordinal_hi ox tx). set_extens t. by move/funI_P => [z /setX_P [p1 p2 /set1_P ->] ->]; rewrite - h. move => tx; apply /funI_P; exists (J t \0o); last by aw; apply h. by apply:setXp_i; fprops; apply/set1_P. Qed. Lemma oprod1l x: ordinalp x -> \1o *o x = x. Proof. move=> ox; case: (least_ordinal6 (fun x => \1o *o x = x) ox) => //. set c := least_ordinal _ _; move => [oc H]; case => //. rewrite (oprod_rec_def OS1 oc); set_extens t. move/funI_P => [z /setX_P [p1 /set1_P -> p2] ->]. rewrite H // osum0r //; exact: (ordinal_hi oc p2). move => tc; apply /funI_P; exists (J \0o t). by apply:setXp_i; fprops; apply/set1_P. aw; rewrite H // osum0r //; exact:(ordinal_hi oc tc). Qed. Lemma osumA a b c: ordinalp a -> ordinalp b -> ordinalp c -> a +o (b +o c) = (a +o b) +o c. Proof. move => oa ob oc. case: (least_ordinal6 (fun c => a +o (b +o c) = (a +o b) +o c) oc) => //. set d := least_ordinal _ _; move => [od H]; case. rewrite (osum_rec_def oa (OS_sum2 ob od)) (osum_rec_def ob od). rewrite (osum_rec_def (OS_sum2 oa ob) od) {1} (osum_rec_def oa ob). set_extens t; case /setU2_P => h; apply /setU2_P. - left; fprops. - move /funI_P:h => [z /setU2_P ha ->]; case: ha. move => zb; left; apply /setU2_P;right; apply/funI_P;ex_tac. move => /funI_P [w wd ->]; rewrite (H _ wd); right; apply/funI_P; ex_tac. - case /setU2_P :h; first by left. move /funI_P => [z za ->]; right; apply /funI_P; exists z; fprops. - right; apply /funI_P; move/funI_P: h => [z zd ->]; rewrite - (H _ zd). exists (b +o z) => //;apply /setU2_P; right; apply /funI_P; ex_tac. Qed. Lemma oprodD a b c: ordinalp a -> ordinalp b -> ordinalp c -> c *o (a +o b) = (c *o a) +o (c *o b). Proof. move => oa ob oc. case: (least_ordinal6 (fun b => c *o (a +o b) = (c *o a) +o (c *o b)) ob) => //. set d := least_ordinal _ _; move => [od H]; case. move: (OS_prod2 oc oa) (OS_prod2 oc od) => oca ocd. rewrite (oprod_rec_def oc (OS_sum2 oa od)) (osum_rec_def oa od). rewrite (osum_rec_def oca ocd) {1}(oprod_rec_def oc oa)(oprod_rec_def oc od). set_extens t. move/funI_P => [z /setX_P[pz Pz /setU2_P Qz] ->];case: Qz => h; apply/setU2_P. left; apply /funI_P; exists (J (P z) (Q z)); aw;fprops. right; move/funI_P:h => [u ud ->]; rewrite (H _ ud). rewrite - (osumA oca (OS_prod2 oc (ordinal_hi od ud)) (ordinal_hi oc Pz)). apply/funI_P; exists (c *o u +o P z) => //; apply/funI_P. exists (J (P z) u); aw; fprops. case /setU2_P; move/funI_P=> [z za ->]; apply/funI_P. move/setX_P: za => [pr pa pb]; exists z => //;apply /setX_P; split;fprops. move/funI_P: za => [w /setX_P [pr pa pb] ->]. rewrite (osumA oca (OS_prod2 oc (ordinal_hi od pb)) (ordinal_hi oc pa)). rewrite - (H _ pb); exists (J (P w) ( a +o Q w)); aw;apply:setXp_i => //. apply /setU2_P; right; apply /funI_P; ex_tac. Qed. Lemma oprodA a b c: ordinalp a -> ordinalp b -> ordinalp c -> a *o (b *o c) = (a *o b) *o c. Proof. move => oa ob oc. case: (least_ordinal6 (fun c => a *o (b *o c) = (a *o b) *o c) oc) => //. set d := least_ordinal _ _; move => [od H]; case. rewrite (oprod_rec_def oa (OS_prod2 ob od)) (oprod_rec_def ob od). rewrite (oprod_rec_def (OS_prod2 oa ob) od) {1} (oprod_rec_def oa ob). set_extens t; case /funI_P => [z za ->]; apply /funI_P. move /setX_P:za=> [pz p1z /funI_P [u /setX_P [ppz p2z p3z] ->]]. move:(ordinal_hi ob p2z)(ordinal_hi od p3z)(ordinal_hi oa p1z)=> opu oqu opz. have obqu:= (OS_prod2 ob oqu). rewrite (oprodD obqu opu oa). rewrite - (osumA (OS_prod2 oa obqu) (OS_prod2 oa opu)opz) (H _ p3z). exists (J (a *o P u +o P z) (Q u)); aw;apply: setXp_i => //. by apply/funI_P; exists (J (P z) (P u)); aw;apply: setXp_i. move /setX_P:za=> [pz /funI_P [u /setX_P [pu p1 p2] ->] qzd]. move:(ordinal_hi oa p1)(ordinal_hi ob p2)(ordinal_hi od qzd)=> opu oqu oqz. rewrite (osumA (OS_prod2 (OS_prod2 oa ob) oqz) (OS_prod2 oa oqu) opu). rewrite -(H _ qzd) - (oprodD (OS_prod2 ob oqz) oqu oa). exists (J (P u) (b *o Q z +o Q u)); aw; apply: setXp_i => //. by apply /funI_P;exists (J (Q u) (Q z)); aw; apply: setXp_i. Qed. (** Utilitaries for the Cantor Normal Form *) Definition osum_expansion f := induction_term (fun n v => f n +o v) \0o. Definition oprod_expansion f := induction_term (fun n v => v *o f n) \1o. Lemma osum_expansion0 f: osum_expansion f \0c = \0o. Proof. exact: induction_term0. Qed. Lemma oprod_expansion0 f: oprod_expansion f \0c = \1o. Proof. exact: induction_term0. Qed. Lemma osum_expansion_succ n f: natp n -> osum_expansion f (csucc n) = f n +o (osum_expansion f n). Proof. move => nb; exact: induction_terms. Qed. Lemma oprod_expansion_succ n f: natp n -> oprod_expansion f (csucc n) = (oprod_expansion f n) *o (f n). Proof. move => nb; exact: induction_terms. Qed. Lemma osum_expansion1 f: ordinalp (f \0c) -> osum_expansion f \1c = f \0c. Proof. move => h; rewrite - succ_zero (osum_expansion_succ _ NS0) osum_expansion0. by rewrite osum0r. Qed. Lemma oprod_expansion1 f: ordinalp (f \0c) -> oprod_expansion f \1c = f \0c. Proof. move => h; rewrite - succ_zero (oprod_expansion_succ _ NS0) oprod_expansion0. by rewrite oprod1l. Qed. Definition ord_below_n f n := (forall k, k ordinalp (f k)). Definition same_below (e e': fterm) n:= (forall i, i e i = e' i). Lemma OS_osum_expansion n f: natp n -> ord_below_n f n -> ordinalp (osum_expansion f n). Proof. move: n;apply: Nat_induction. by move => _; rewrite osum_expansion0; fprops. move => n nN Hrec h1; rewrite (osum_expansion_succ _ nN); apply: OS_sum2. by apply: h1; apply: cltS. apply: Hrec => k kn; apply: h1; exact:(clt_leT kn (cleS nN)). Qed. Lemma OS_oprod_expansion n f: natp n -> ord_below_n f n -> ordinalp (oprod_expansion f n). Proof. move: n;apply: Nat_induction. by move => _; rewrite oprod_expansion0; fprops. move => n nN Hrec h1; rewrite (oprod_expansion_succ _ nN); apply: OS_prod2. apply: Hrec => k kn; apply: h1;exact:(clt_leT kn (cleS nN)). by apply: h1; apply: cltS. Qed. Lemma osum_expansion_exten f g n: natp n -> same_below f g n -> osum_expansion f n = osum_expansion g n. Proof. move: n; apply: Nat_induction. by move => _; rewrite ! osum_expansion0. move => n nN Hrec sv;rewrite !(osum_expansion_succ _ nN). move: (cltS nN) => pa. rewrite (sv _ pa) Hrec // => i lin; apply: sv; apply:clt_ltT lin pa. Qed. Lemma oprod_expansion_exten f g n: natp n -> same_below f g n -> oprod_expansion f n = oprod_expansion g n. Proof. move: n; apply: Nat_induction. by move => _; rewrite ! oprod_expansion0. move => n nN Hrec sv;rewrite !(oprod_expansion_succ _ nN). move: (cltS nN) => pa. rewrite (sv _ pa) Hrec // => i lin; apply: sv; exact:clt_ltT lin pa. Qed. Lemma osum_expansionA n m f: natp n -> natp m -> ord_below_n f (n +c m) -> osum_expansion f (n +c m) = (osum_expansion (fun z => f (z +c n)) m) +o (osum_expansion f n). Proof. move => nN mN; move: m mN n nN; apply: Nat_induction. move => n nN; rewrite (Nsum0r nN) (osum_expansion0) => fo. rewrite osum0l //; apply:OS_osum_expansion => //. move => m mN Hrec n nN. have nmN:= NS_sum nN mN. have lt1:=(cltS nmN). rewrite (csum_nS _ mN) (osum_expansion_succ _ nmN) => fo. have pa:forall k, k ordinalp (f k). move => k [kp _]; apply: fo; exact:cle_ltT kp lt1. have pb: ordinalp (f (n +c m)) by apply: fo. have pc: ordinalp (osum_expansion (fun z => f (z +c n)) m). apply: OS_osum_expansion => // k km; apply: fo. move: (csum_Mlteq nN km); rewrite csumC (csumC m) => h. exact: clt_ltT h lt1. have pd: ordinalp (osum_expansion f n). apply: OS_osum_expansion => // k km; apply: fo. exact: (clt_ltT km (cle_ltT (csum_M0le m (CS_nat nN)) lt1)). by rewrite Hrec // (osumA pb pc pd) (osum_expansion_succ _ mN) csumC. Qed. Lemma oprod_expansionA n m f: natp n -> natp m -> ord_below_n f (n +c m) -> oprod_expansion f (n +c m) = (oprod_expansion f n) *o (oprod_expansion (fun z => f (z +c n)) m). Proof. move => nN mN; move: m mN n nN; apply: Nat_induction. move => n nN; rewrite (Nsum0r nN) (oprod_expansion0) => fo. rewrite oprod1r //; apply:OS_oprod_expansion => //. move => m mN Hrec n nN. have nmN:= NS_sum nN mN. have lt1 :=(cltS nmN). rewrite (csum_nS _ mN) (oprod_expansion_succ _ nmN) => fo. have pa:forall k, k ordinalp (f k). move => k [kp _]; apply: fo; exact :cle_ltT kp lt1. have pb: ordinalp (f (n +c m)) by apply: fo. have pc: ordinalp (oprod_expansion (fun z => f (z +c n)) m). apply: OS_oprod_expansion => // k km; apply: fo. move: (csum_Mlteq nN km); rewrite csumC (csumC m) => h. exact:(clt_ltT h lt1). have pd: ordinalp (oprod_expansion f n). apply: OS_oprod_expansion => // k km; apply: fo. exact:clt_ltT km (cle_ltT (csum_M0le m (CS_nat nN)) lt1). by rewrite Hrec // - (oprodA pd pc pb) (oprod_expansion_succ _ mN) csumC. Qed. (** ** Properties of ordering *) Lemma olt_01: \0o //; rewrite / \1o/card_one; fprops. Qed. Lemma olt_12: \1o /oltSSP; rewrite osucc_zero osucc_one. Qed. Lemma olt_02: \0o p1; exact:olt_ltT. Qed. Lemma olt0S x: ordinalp x -> \0o ox; apply /oltSleP; apply: ozero_least. Qed. Lemma oge2P x: \2o <=o x <-> \1o [\/ x = \0o, x = \1o | \2o <=o x]. Proof. move=> ox. case :(equal_or_not x \0o); first by constructor 1. move=> xe;case: (equal_or_not \1o x); first by constructor 2. by move=> xxe; constructor 3; apply /oge2P; split =>//; apply: oge1. Qed. Lemma ord2_trichotomy1 x: \2o <=o x -> (x <> \0o /\ x <> \1o). Proof. move=> h; split; first exact: (nesym (proj2 (olt_leT olt_02 h))). exact: (nesym (proj2 (olt_leT olt_12 h))). Qed. Lemma osum_Meqlt a b c: a ordinalp c -> (c +o a) /oltP0 [oa ob ab] oc; apply /oltP; fprops. rewrite (osum_rec_def oc ob); apply /setU2_P; right; apply/funI_P; ex_tac. Qed. Lemma oprod_Meqlt a b c: a \0o (c *o a) /oltP0 [oa ob ab] /oltP0 [oz oc zc]. apply /oltP; fprops; rewrite (oprod_rec_def oc ob); apply /funI_P. exists (J \0o a); aw; fprops; rewrite osum0r; fprops. Qed. Lemma osum_Meqler a b c: ordinalp a -> ordinalp b -> ordinalp c -> c +o a <=o c +o b -> a <=o b. Proof. move => oa ob oc h. case: (oleT_el oa ob) => // h1; case: (oleNgt h (osum_Meqlt h1 oc)). Qed. Lemma oprod_Meqler a b c: ordinalp a -> ordinalp b -> \0o c *o a <=o c *o b -> a <=o b. Proof. move => oa ob oc h. case: (oleT_el oa ob) => // h1;case: (oleNgt h (oprod_Meqlt h1 oc)). Qed. Lemma oprod2_pos a b: \0o \0o \0o oa ob; move: (oprod_Meqlt ob oa); rewrite oprod0r. Qed. Lemma oprod2_nz a b: ordinalp a -> ordinalp b -> a <> \0o -> b <> \0o -> a *o b <> \0o. Proof. move=> oa ob anz bnz. exact:(nesym (proj2(oprod2_pos (ord_ne0_pos oa anz) (ord_ne0_pos ob bnz)))). Qed. Lemma osum_Meqle a b c: a <=o b -> ordinalp c -> (c +o a) <=o (c +o b). Proof. move => ab oc. case: (equal_or_not a b) => nab. by rewrite nab; apply: oleR; apply: (OS_sum2 oc (proj32 ab)). exact: (proj1 (osum_Meqlt (conj ab nab) oc)). Qed. Lemma oprod_Meqle a b c: a <=o b -> ordinalp c -> (c *o a) <=o (c *o b). Proof. move => ab oc. case: (ozero_dichot oc) => cz. rewrite cz oprod0l oprod0l; apply: (oleR OS0). case: (equal_or_not a b) => nab. by rewrite nab; apply: oleR; apply: (OS_prod2 oc (proj32 ab)). exact: (proj1 (oprod_Meqlt (conj ab nab) cz)). Qed. Lemma ole_ltT_s a b c: ordinalp c -> a <=o b -> inc b c -> inc a c. Proof. by move => oc ab /(oltP oc) /(ole_ltT ab) bc; apply /(oltP oc). Qed. Lemma osum_Mleeq a b c: a <=o b -> ordinalp c -> (a +o c) <=o (b +o c). Proof. move => ab oc. case: (least_ordinal6 (fun c => (a +o c) <=o (b +o c)) oc) => //. set d := least_ordinal _ _; move => [od H]; case. move: (ab) => [oa ob sab]. split; fprops. rewrite (osum_rec_def oa od) => t;case /setU2_P. by move => ta; rewrite (osum_rec_def ob od); apply/setU2_P; left; apply: sab. move /funI_P => [z zd ->]; apply:(ole_ltT_s (OS_sum2 ob od) (H _ zd)). rewrite (osum_rec_def ob od). apply/setU2_P; right; apply /funI_P; ex_tac. Qed. Lemma osum_Mle0 a b: ordinalp a -> ordinalp b -> a <=o (a +o b). Proof. move=> oa ob. rewrite - {1} (osum0r oa); apply: osum_Meqle => //; apply:(ozero_least ob). Qed. Lemma osum_M0le a b: ordinalp a -> ordinalp b -> b <=o (a +o b). Proof. move=> oa ob;rewrite - {1} (osum0l ob); apply: osum_Mleeq (ozero_least oa) ob. Qed. Lemma osum_Mlele a b c d: a <=o b -> c <=o d -> (a +o c) <=o (b +o d). Proof. move=> le1 le2; apply: (@oleT (a +o d)). apply:(osum_Meqle le2 (proj31 le1)). apply:(osum_Mleeq le1 (proj32 le2)). Qed. Lemma oprod_Mleeq a b c: a <=o b -> ordinalp c -> (a *o c) <=o (b *o c). Proof. move => [oa ob sab] oc. case: (least_ordinal6 (fun c => (a *o c) <=o (b *o c)) oc) => //. set d := least_ordinal _ _ => [] [od H] []. split; fprops. rewrite (oprod_rec_def oa od) => t /funI_P [z /setX_P [_ p2 p3] ->]. have la:= (osum_Mleeq (H _ p3) (ordinal_hi oa p2)). apply: (ole_ltT_s (OS_prod2 ob od) la). rewrite (oprod_rec_def ob od); apply /funI_P; exists (J (P z) (Q z));aw; fprops. Qed. Lemma oprod_Mlele a b c d: a <=o b -> c <=o d -> (a *o c) <=o (b *o d). Proof. move=> le1 le2; apply: (@oleT (a *o d)). apply:oprod_Meqle le2 (proj31 le1). apply:oprod_Mleeq le1 (proj32 le2). Qed. Lemma oprod_Mle1 a b: ordinalp a -> \0o a <=o (a *o b). Proof. move=> oa /oge1P ba. rewrite - {1} (oprod1r oa);exact: oprod_Mlele (oleR oa) ba. Qed. Lemma oprod_M1le a b: \0o ordinalp b-> b <=o (a *o b). Proof. move=> /oge1P oa ob. rewrite - {1} (oprod1l ob); exact: oprod_Mlele oa (oleR ob). Qed. Lemma oprod_Meq1lt b c: \1o \0o c lt1b cz. rewrite - {1} (oprod1r (proj32_1 cz)); apply: (oprod_Meqlt lt1b cz). Qed. Lemma osum_Meqltr a b c: ordinalp a -> ordinalp b -> ordinalp c -> (c +o a) a oa ob oc olt. case: (oleT_el ob oa) => // oba. case:(oltNge olt); exact: (osum_Mlele (oleR oc) oba). Qed. Lemma osum_Mlteqr a b c: ordinalp a -> ordinalp b -> ordinalp c -> (a +o c) a oa ob oc olt. case: (oleT_el ob oa) => // oba. case: (oltNge olt); exact: (osum_Mlele oba (oleR oc)). Qed. Lemma oprod_Meqltr a b c: ordinalp a -> ordinalp b -> ordinalp c -> (c *o a) a oa ob oc olt. case: (oleT_el ob oa) => // oba. case: (oltNge olt); exact: (oprod_Mlele (oleR oc) oba). Qed. Lemma oprod_Mlteqr a b c: ordinalp a -> ordinalp b -> ordinalp c -> (a *o c) a oa ob oc olt. case: (oleT_el ob oa) => // oba. case: (oltNge olt); exact: (oprod_Mlele oba (oleR oc)). Qed. Lemma osum2_simpl a b c: ordinalp a -> ordinalp b -> ordinalp c -> c +o a = c +o b -> a = b. Proof. move=> oa ob oc so. by case: (oleT_ell oa ob) => h //; move: (osum_Meqlt h oc); rewrite so; move=> [_]; case. Qed. Lemma oprod2_simpl a b c: ordinalp a -> ordinalp b -> \0o c *o a = c *o b -> a = b. Proof. move=> oa ob oc eq. by case: (oleT_ell oa ob) => h //; move: (oprod_Meqlt h oc); rewrite eq; move=> [_]; case. Qed. Lemma oprod2_simpl1 a c: ordinalp a -> \0o c *o a = c -> a = \1o. Proof. move => sa sb. rewrite -{2} (oprod1r (proj32_1 sb)) => sc. by rewrite (oprod2_simpl sa OS1 sb sc). Qed. Lemma osum_a_ab a b: ordinalp a -> ordinalp b -> a +o b = a -> b = \0o. Proof. move => oa ob; rewrite - {2}(osum0r oa); apply: osum2_simpl => //; fprops. Qed. Lemma osum2_zero x y: ordinalp x -> ordinalp y -> x +o y = \0o -> (x = \0o /\ y = \0o). Proof. move=> ox oy s0; case: (ozero_dichot ox) => xz. by move: s0; rewrite xz (osum0l oy) => yz. by move: (olt_leT xz (osum_Mle0 ox oy)) => [];rewrite s0. Qed. Lemma oprod_a_ab a b: \0o ordinalp b -> a *o b = a -> b = \1o. Proof. move=> az ob; rewrite -{2} (oprod1r (proj32_1 az)). apply: (oprod2_simpl ob OS1 az). Qed. Lemma oprod2_one a b: ordinalp a -> ordinalp b -> a *o b = \1o -> (a = \1o /\ b = \1o). Proof. move=> oa ob ab1. case: (equal_or_not a \1o) => h. by move: ab1; rewrite h oprod1l. case: (equal_or_not b \0c) => bz. by move: ab1; rewrite bz (oprod0r) => bad; case: card1_nz. move: (ord_ne0_pos ob bz) => b1. move: (oprod_Mle1 oa b1); rewrite ab1 => la2. by move: ab1; rewrite (olt1 (conj la2 h)) oprod0l => bad; case:card1_nz. Qed. Lemma oprod2_two a b: ordinalp a -> ordinalp b -> a *o b = \2o -> (a = \1o \/ b = \1o). Proof. move=> oa ob ab1. case: (equal_or_not b \0c) => bz. by move: ab1; rewrite bz (oprod0r) => bad; case: card2_nz. have b1:= (ord_ne0_pos ob bz). move: (oprod_Mle1 oa b1); rewrite ab1 => la2. case: (equal_or_not a \2o) => a2. move: ab1; rewrite a2 -{2} (oprod1r OS2) => sv. right; exact:(oprod2_simpl ob OS1 olt_02 sv). have /oltSleP: a az. by move: ab1; rewrite az (oprod0l) => bad; case: card2_nz. by move/(oleA (oge1 oa az)) => a3;left. Qed. Lemma osum_x_xy x y: ordinalp x -> ordinalp y -> x +o (x *o y) = x*o (\1o +o y). Proof. move: OS1=> o1 ox oy; rewrite oprodD // oprod1r //. Qed. Lemma osum2_succ x y: ordinalp x -> ordinalp y -> osucc (x +o y) = x +o (osucc y). Proof. move=> oa ob. rewrite -(osucc_pr ob) (osumA oa ob OS1) osucc_pr ;fprops. Qed. Lemma oprod2_succ x y: ordinalp x -> ordinalp y -> x *o (osucc y) = (x *o y) +o x. Proof. move=> ox oy. rewrite -(osucc_pr oy) (oprodD oy OS1 ox); rewrite oprod1r //. Qed. Lemma osum2_2int a b: natp a -> natp b -> a +o b = a +c b. Proof. move=> aN bN;move: b bN. have oa:= OS_nat aN. apply: Nat_induction; first by rewrite (Nsum0r aN) (osum0r oa). move=> n nN hrec. rewrite (csum_nS _ nN) (succ_of_Nat nN) (succ_of_Nat (NS_sum aN nN)). by rewrite - (osum2_succ oa (OS_cardinal (CS_nat nN))) hrec. Qed. Lemma oprod2_2int a b: natp a -> natp b -> a *o b = a *c b. Proof. move=> aN bN;move: b bN. have oa:= OS_nat aN. apply: Nat_induction; first by rewrite cprod0r oprod0r. move=> n nN hrec. rewrite (cprod_nS _ nN) (succ_of_Nat nN) - (osum2_2int (NS_prod aN nN) aN). by rewrite (oprod2_succ oa (OS_cardinal (CS_nat nN))) hrec. Qed. Lemma osum2_lt_omega a b: a b (a +o b) aN /olt_omegaP bN; apply /olt_omegaP. rewrite osum2_2int; fprops. Qed. Lemma oprod2_lt_omega a b: a b (a *o b) aN /olt_omegaP bN;apply /olt_omegaP. rewrite oprod2_2int; fprops. Qed. Lemma osum_11_2: \1o +o \1o = \2o. Proof. by move:(osum2_2int NS1 NS1); rewrite card_two_pr. Qed. Lemma ord_double x: ordinalp x -> x *o \2o = x +o x. Proof. by move=> ox; rewrite - osum_11_2 (oprodD OS1 OS1 ox) (oprod1r ox). Qed. Lemma osum_int_omega n: n n +o omega0 = omega0. Proof. move => no; move: (no) => [[on oo son] _]. set_extens t; last by apply: (proj33 (osum_M0le on oo)). rewrite (osum_rec_def on oo); case /setU2_P; first by apply: son. move => /funI_P [z zo ->]; apply /(oltP oo) /(osum2_lt_omega no). by apply/(oltP oo). Qed. Lemma oprod_int_omega n: n \0c n *o omega0 = omega0. Proof. move => no np; move: (no) => [[on oo son] _]. set_extens t; last by apply: (proj33 (oprod_M1le np oo)). rewrite (oprod_rec_def on oo) => /funI_P [z /setX_P [z1 z2 z3] ->]. apply /(oltP oo) /(osum2_lt_omega). by apply (oprod2_lt_omega no); apply/(oltP oo). by apply/(oltP oo); apply: son. Qed. Lemma osum2_nc (x := \1o) (y := omega0): x +o y <> y +o x. Proof. rewrite (osum_int_omega olt_1omega) /y=> h. symmetry in h; move: (osum_a_ab OS_omega OS1 h);apply:card1_nz. Qed. Lemma oprod2_nc (x := \2o) (y := omega0): x *o y <> y *o x. Proof. rewrite (oprod_int_omega olt_2omega olt_02). rewrite (ord_double OS_omega) => h. symmetry in h;move: (osum_a_ab OS_omega OS_omega h); apply: omega_nz. Qed. Lemma osum2_nD (a:= \1o) (b:= \1o) (c:= omega0): (a +o b) *o c <> (a *o c) +o (b *o c). Proof. rewrite (oprod_int_omega olt_1omega olt_01) (osum2_2int NS1 NS1). rewrite card_two_pr (oprod_int_omega olt_2omega olt_02) => /esym h. move: (osum_a_ab OS_omega OS_omega h). apply: omega_nz. Qed. Lemma cardinal_of_ordinal r: worder r -> cardinal (ordinal r) = cardinal (substrate r). Proof. move=> wor. move: (ordinal_o_is wor) => [f [o1 o2 [bf pa pb] pc]]. symmetry;apply /card_eqP. by exists f; split => //; rewrite pb ordinal_o_sr. Qed. Lemma osum_cardinal x y: ordinalp x -> ordinalp y -> cardinal (x +o y) = (cardinal x) +c (cardinal y). Proof. move => ox oy; symmetry. rewrite /osum2. set w := order_sum2 _ _. have w1: worder w by rewrite /w;fprops. have pa:= (OS_ordinal w1). move: (ordinal_o_is w1) => [F [_ _ [bf sf tf] _]]. have : source F \Eq target F by exists F. rewrite tf (ordinal_o_sr (ordinal w)) sf {1} /w orsum2_sr; fprops. rewrite (ordinal_o_sr x)(ordinal_o_sr y). have paa: fgraph (variantLc x y) by rewrite /variantLc; fprops. move /card_eqP; rewrite /canonical_du2 csum_pr //. move => <-; apply: csum2_pr; bw. set f := fun a:Set => _. move: (doubleton_fam_canon f); rewrite /f;bw. Qed. (* deplacer et noter *) Lemma oprod_cardinal x y: ordinalp x -> ordinalp y -> cardinal (x *o y) = (cardinal x) *c (cardinal y). Proof. move => xo yo. have wox:= (ordinal_o_wor xo). have woy:= (ordinal_o_wor yo). have orx := (ordinal_o_or x). have ory := (ordinal_o_or y). have pa: worder (order_prod2 (ordinal_o x) (ordinal_o y)) by fprops. rewrite /oprod2 (cardinal_of_ordinal pa) (orprod2_sr orx ory). rewrite (ordinal_o_sr x) (ordinal_o_sr y) cprod2cl cprod2cr cprodC. symmetry;rewrite cprod2_pr1; apply /card_eqP. exists (product2_canon y x); split => //. - apply: product2_canon_fb. - rewrite /product2_canon; aw. - rewrite /product2_canon; aw. Qed. Lemma osum_cardinal_gen r X: worder_on r (domain X) -> ordinal_fam X -> cardinal (osum r X) = csumb (domain X) (fun z => cardinal (Vg X z)). Proof. move => sa sb. set Y := (Lg (domain X) (fun z => ordinal_o (Vg X z))). have hb: worder_fam Y. rewrite /Y /worder_fam /allf Lg_domain. move => i idx; bw; apply: ordinal_o_wor; apply:(sb _ idx). have hc:worder (order_sum r Y) by apply:orsum_wor; rewrite /Y; bw. have hd:orsum_ax r Y. move: sa => [[or _]dr]. have sr:substrate r = domain Y by rewrite /Y; bw. by split => // i /hb []. rewrite /osum -/Y (cardinal_of_ordinal hc) (orsum_sr hd). rewrite /sum_of_substrates csum_pr /fam_of_substrates /Y !Lg_domain. by apply: csumb_exten => i idx; bw; rewrite ordinal_o_sr. Qed. Lemma finite_rems c: ordinalp c -> finite_set (Zo (osucc c) (fun b => exists2 a, ordinalp a & c = a +o b)). Proof. move => oc; set E := Zo _ _. pose p b a := ordinalp a /\ c = a +o b. pose f b := (choose (p b)). have CP: forall b, inc b E -> p b (f b). by move => b /Zo_P [_ [a aa ab]]; apply:(choose_pr); exists a. have ci: forall a b, inc a E -> inc b E -> a f b a b /CP [ofa s1] /CP [ofb s2] lab. case: (oleT_el ofa ofb) => // la. move: (osum_Meqlt lab ofa); rewrite - s1 => /oltNge; case. by move:(osum_Mleeq la (proj32_1 lab)); rewrite - s2. have ose: ordinal_set E by move => t /Zo_S /(ordinal_hi (OS_succ oc)). pose F := fun_image E f. have osf: ordinal_set F by move => t /funI_P [z /CP [osf _] -> ]. move:(wordering_ole_pr ose) => [ha hb]. move:(wordering_ole_pr osf) => [hc hd]. have he: forall i, inc i (substrate (ole_on E)) -> inc (f i) (substrate (ole_on F)). move =>i; rewrite hb hd => ie; apply/funI_P; ex_tac. have hf:forall i j, glt (ole_on E) i j -> glt (ole_on F) (f j) (f i). move => i j [/graph_on_P1 [ie je lij] nij]. move: (ci _ _ ie je (conj lij nij)) => [lfij nfij]. split => //; apply/graph_on_P1; split => //; apply/funI_P; first by exists j. by exists i. by move: (worder_decreasing_finite ha hc he hf); rewrite hb. Qed. Section InfiniteNormal. Variable C: Set. Hypothesis iC: infinite_c C. Let E := (cnext C). Lemma cnext_sum x y: inc x E -> inc y E -> inc (x +o y) E. Proof. move: iC => [cc _]. move=> /(cnextP cc) [xo cx] /(cnextP cc) [yo cy]. apply /(cnextP cc);split; first by fprops. rewrite osum_cardinal //. move: (csum_Mlele cx cy); rewrite csum_inf1 //; apply /infinite_setP. Qed. Lemma cnext_prod x y: inc x E -> inc y E -> inc (x *o y) E. Proof. move: iC => [cc _]. move=> /(cnextP cc) [xo cx] /(cnextP cc) [yo cy]. apply /(cnextP cc);split; first by fprops. move: (cprod_Mlele cx cy); rewrite oprod_cardinal // csquare_inf //. Qed. Lemma cnext_leomega x: x <=o omega0 -> inc x E. Proof. move: iC => [cc _]. move => [ox oo xo]; apply /(cnextP cc); split => //. have: cardinal x <=c cardinal Nat by apply: sub_smaller. rewrite cardinal_Nat;move /infinite_c_P2: iC => h1 h2; apply: cleT h2 h1. Qed. Lemma cnext_zero: inc \0o E. Proof. apply: cnext_leomega; apply: ozero_least; fprops. Qed. Lemma cnext_succ x: inc x E -> inc (osucc x) E. Proof. move=> cx; move/(cnextP (proj1 iC)):(cx) => [ox _]. rewrite - (osucc_pr ox); move: olt_1omega => [h _]. by apply: cnext_sum => //; apply:cnext_leomega. Qed. Lemma cnext_sup F: cardinal F <=c C -> sub F E -> inc (\osup F) E. Proof. move: (iC) => [cc _]. move => pa pb; apply/(cnextP cc); split. by apply: OS_sup => t/pb /cnextP []. rewrite - setUb_identity. move: (csum_pr1 (identity_g F)); rewrite identity_d /csumb;set f := Lg _ _. have cdf: cardinal (domain f) <=c C by rewrite /f; bw. have etc: forall i, inc i (domain f) -> Vg f i <=c C. rewrite /f; bw; move => i idf; bw;rewrite identity_ev //. by move /cnextP: (pb _ idf) => []. move: (notbig_family_sum iC cdf etc) => ha hb; exact :cleT hb ha. Qed. End InfiniteNormal. Lemma cnext_pred c: cardinalp c -> c = \csup (Zo (cnext c) cardinalp). Proof. move => cc. have oc:= (proj1 cc). set E := (Zo (cnext c) cardinalp). have cse: (cardinal_set E) by move => t /Zo_P []. have pa: inc c E. apply /Zo_P; split=> //; apply /(cnextP cc) => //. rewrite card_card //; split; fprops. apply:(cleA (card_sup_ub cse pa)). apply:(card_ub_sup cc). by move => x /Zo_P [ /(cnextP cc) [ox h]] /card_card <-. Qed. Lemma cnext_pred_more E (c:= \csup (Zo E cardinalp)): (exists2 C, infinite_c C & E = cnext C) -> infinite_c c /\ E = cnext c. Proof. move => [C pa pb]. by move:(cnext_pred (proj1 pa)); rewrite - pb -/c => <-. Qed. Definition aleph_one := cnext omega0. Definition countable_ordinal x := ordinalp x /\ countable_set x. Lemma aleph_oneP z: (inc z aleph_one <-> countable_ordinal z). Proof. move:(cnextP CS_omega) => h. split; first by move/h => [ha /countableP hb]; split => //. move => [ha /countableP hb]; apply/h;split => //. Qed. Lemma osum2_countable x y: countable_ordinal x -> countable_ordinal y -> countable_ordinal (x +o y). Proof. move: CIS_omega aleph_oneP => h T. by move => /T xa /T xn; apply /T;apply:cnext_sum. Qed. Lemma oprod2_countable x y: countable_ordinal x -> countable_ordinal y -> countable_ordinal (x *o y). Proof. move: CIS_omega aleph_oneP => h T. by move => /T xa /T xn; apply /T;apply:cnext_prod. Qed. Lemma countable_ordinal_sup E: countable_set E -> (alls E countable_ordinal)-> countable_ordinal (\osup E). Proof. move: CIS_omega aleph_oneP => h T. move => /countableP pa pb. have se:sub E aleph_one by move => t /pb /T. by move: (cnext_sup h pa se) => /T. Qed. Lemma countable_leomega x: x <=o omega0 -> countable_ordinal x. Proof. move => [ox oo /countable_sub_Nat xo]; split => //. Qed. Lemma countable_one: countable_ordinal \1o. Proof. move: olt_1omega => [o1 _]; by apply: countable_leomega. Qed. Lemma countable_succ x: countable_ordinal x -> countable_ordinal (osucc x). Proof. move=> cx; move: (cx) => [ox _]; rewrite - (osucc_pr ox). apply: osum2_countable => //; apply: countable_one. Qed. Lemma cardinal_omega2: cardinal omega0 = cardinal (omega0 +o omega0). Proof. move: OS_omega => o_o. rewrite osum_cardinal // csum_inf1 // (card_card CS_omega). exact:CIS_omega. Qed. (** ** Least upper bound *) Definition ord_cofinal a b := sub a b /\ forall x, inc x b -> exists2 y, inc y a & x <=o y. Definition mutually_cofinal x y := (forall a, inc a x -> exists2 b, inc b y & a <=o b) /\ (forall a, inc a y -> exists2 b, inc b x & a <=o b). Lemma ord_ub_sup1 a X: ordinalp a -> sub X a -> \osup X <=o a. Proof. move => pa pb; apply: ord_ub_sup => // t /pb h. by move/ (oltP pa): h => []. Qed. Lemma ord_sup_ordinal a (b:= \osup a): ordinalp a -> a = b \/ a = osucc b. Proof. move=> oa. case:(proj1 (osuccVidpred oa)); last by left. by move=> yp; right; symmetry; apply: predo_K. Qed. Lemma ord_sup_sub X: ordinal_set X -> ~ (inc (\osup X) X) -> forall x, inc x X -> x h1 h2 x xX; split; [apply: ord_sup_ub | dneg xs; rewrite -xs ]. Qed. Lemma ord_sup_inVlimit X: ordinal_set X -> nonempty X -> inc (\osup X) X \/ limit_ordinal (\osup X). Proof. move=> alo [a aX]. case: (p_or_not_p (inc (union X) X)) => nsX; [ by left | right]. have asu:= (ord_sup_ub alo aX). have so:= proj32 asu. case: (ordinal_trichot so) => //. move=> h; rewrite h in nsX asu; case: nsX. by rewrite - (ole0 asu). case => // [y oy h]. have aiy: (forall i, inc i X -> i <=o y). move=> i iX; apply /oltSleP. by rewrite -h; apply: ord_sup_sub. move: (ord_ub_sup oy aiy); rewrite h. by move /oleSltP => [_ ?]. Qed. Lemma ord_sup_M x y: sub x y -> ordinal_set y -> (\osup x) <=o (\osup y). Proof. move=> xy al1. apply:ord_ub_sup => //; first by apply: OS_sup. by move=> i ix; apply: ord_sup_ub => //; apply: xy. Qed. Lemma ord_sup_2cofinal x y: mutually_cofinal x y -> \osup x = \osup y. Proof. move=> [p3 p4]. have osx: ordinal_set x by move => a ax; move: (p3 _ ax) => [b _ []]. have osy: ordinal_set y by move => a ay; move: (p4 _ ay) => [b _ []]. apply: oleA. apply: ord_ub_sup => //; first by apply: OS_sup. move=> i ix; move: (p3 _ ix) => [j jy lij]. apply: (oleT lij);apply ord_sup_ub => //. apply: ord_ub_sup => //; first by apply: OS_sup. move=> i ix; move: (p4 _ ix) => [j jy lij]. apply: (oleT lij);apply: ord_sup_ub => //. Qed. Lemma ord_sup_2funI X f g: {inc X, f =1 g} -> \osup (fun_image X f) = \osup (fun_image X g). Proof. move=> h; have -> //: (fun_image X f = fun_image X g). set_extens t; move /funI_P => [z zX ->]; apply /funI_P;ex_tac. by symmetry; apply: h. Qed. Lemma ord_sup_1cofinal x y: ord_cofinal x y -> ordinal_set y -> \osup x = \osup y. Proof. move=> [h1 h2] h3; apply: ord_sup_2cofinal; split => // a ay;exists a;fprops. Qed. Lemma olt_sup A x: ordinal_set A -> x exists2 z, inc z A & x osA h. have ox:= proj31_1 h. case: (p_or_not_p (forall z, inc z A -> z <=o x)) => pc. case: (oltNge h (ord_ub_sup ox pc)). ex_middle bad; case: pc => z zA. case: (oleT_el (osA _ zA) ox) => //. by move => xz; case: bad; ex_tac. Qed. Lemma clt_sup A x: cardinal_set A -> x exists2 z, inc z A & x <=c z. Proof. move => p1 p2. have q1: ordinal_set A by move => t tA; exact (proj1 (p1 _ tA)). move: (oclt p2) => q2. move: (olt_sup q1 q2) => [z zA [zle _]]; ex_tac. exact (ocle3 (proj31_1 p2) (p1 _ zA) zle). Qed. Lemma ord_cofinal_p1 a b: ordinal_set b -> (ord_cofinal a b <-> cofinal (ole_on b) a). Proof. move => h. have pa: (substrate (ole_on b)) = b. rewrite graph_on_sr // => c /h oc; fprops. split. move => [sa sb]; hnf; rewrite pa; split => //. move => x xb; move: (sb _ xb) => [y ya xy]; exists y => //. by apply /graph_on_P1; split => //; apply: sa. rewrite /cofinal pa; move => [sa sb]; split => // x xb. move:(sb _ xb) => [y ya /graph_on_P1 [_ yb yx]]; ex_tac. Qed. Lemma ord_cofinal_p2 a b: limit_ordinal b -> sub a b -> (ord_cofinal a b <-> \osup a = \osup b). Proof. move => pa pb; move: (pa) => [ob _ _]; split. by move => [_ pc]; apply: ord_sup_1cofinal => // x /(ordinal_hi ob). move => pc; split => // x xb. have ox:=(ordinal_hi ob xb). have osa: ordinal_set a by move => y /pb /(ordinal_hi ob). ex_middle h. have pd: forall y, inc y a -> y y ya. case (oleT_el ox (osa _ ya)) => // pe; case h; ex_tac. have sb: \osup b <=o x by rewrite - pc; apply: ord_ub_sup => // i /pd []. move: xb sb. by rewrite -[union b](limit_nonsucc pa); move /(oltP ob) => ua /(oltNge ua). Qed. Lemma ord_cofinal_p3 a: limit_ordinal a -> (\osup a = \osup (osucc a) /\ ~(ord_cofinal a (osucc a))). Proof. move => la; move: (la) => [oa _ _]. rewrite - [union a](limit_nonsucc la). split; first by rewrite [union _] succo_K. move => [h1 h2]. have: inc a (osucc a) by rewrite /osucc; fprops. by move/h2 => [y /(oltP oa) ya] /(oltNge ya). Qed. Lemma ord_cofinal_p4 a C (E:= cnext C): infinite_c C -> ord_cofinal a E -> cardinal a = E. Proof. move => sa [sb sc]. have [pa pb pc] := (cnext_pr1 (proj1 sa)). have ose: ordinal_set E. move => t; move: (proj1 pa); rewrite -/E; exact:ordinal_hi. case: (cleT_el (CS_cardinal a) (proj1 sa)); last first. move /pc; move: (sub_smaller sb);rewrite (card_card pa);exact:cleA. move => cyc; move: (cnext_sup sa cyc sb)=> xsb. have sse:= (ord_sup_1cofinal (conj sb sc) ose). have hy:= (infinite_card_limit2(ge_infinite_infinite sa (proj1 pb))). have ue:=(limit_nonsucc hy). by move: (ordinal_irreflexive (proj1 pa)); rewrite {1} ue -[opred _] sse. Qed. Lemma ord_cofinal_p5 a C (E:= cnext C): infinite_c C -> ord_cofinal a E -> ordinal (ole_on a) = E. Proof. move => pa pc; move: (proj1 pc) => pb. have ca:= (ord_cofinal_p4 pa pc). set x := ordinal (ole_on a). have [sa sb sc] := (cnext_pr1 (proj1 pa)). have ose: ordinal_set E by apply: (ordinal_set_ordinal (proj1 sa)). have osa: ordinal_set a by move => t /pb; apply: ose. have [pe pf]:=(wordering_ole_pr osa). move: (cardinal_of_ordinal pe); rewrite pf -/x ca => cc. have [oe hh] : cardinalp E by exact: (proj32_1 sb). have ox: ordinalp x by apply: OS_ordinal. have cc2: E \Eq x by apply /card_eqP; symmetry; rewrite cc -/E card_card. apply: oleA; last by split => //;exact: (hh _ ox cc2). apply/ordinal_le_P0; split=> //. move: (the_ordinal_iso1 pe); rewrite -/x. have o1 :=(proj1 (ordinal_o_wor oe)). have o2 := (proj1 pe). have o3:order (ordinal_o x) by fprops. set f := (the_ordinal_iso _) => ff. rewrite /order_le; split => //; rewrite ordinal_o_sr; exists f, a; split => //. have -> //: (induced_order (ordinal_o E) a = (ole_on a)). have aso :sub a (substrate (ordinal_o E)) by rewrite ordinal_o_sr. have [sd se]:= (iorder_osr o1 aso). apply: order_exten => // u v; split. move /iorder_gle5P => [ua va /ordo_leP [_ _ ha]]; apply /graph_on_P1. split => //; split => //; fprops. move => /graph_on_P1[ua ub [_ _ uv]]; apply /iorder_gle5P; split => //. apply/ordo_leP;split => //; fprops. Qed. (** ** Subtraction *) Definition odiff b a := Zo b (fun z => inc (a +o z) b). Notation "x -o y" := (odiff x y) (at level 50). Lemma OS_diff a b: ordinalp a -> ordinalp b -> ordinalp (b -o a). Proof. move => oa ob. apply: ordinal_pr; last by move => t /Zo_S /(ordinal_hi ob). move => u /Zo_P [ub /(oltP ob) ss] t tu. apply: (Zo_i (ordinal_transitive ob ub tu)). apply /(oltP ob); apply: ole_ltT ss; apply:osum_Meqle => //. by move/(oltP (ordinal_hi ob ub)): tu => []. Qed. Lemma odiff_wrong a b: b <=o a -> b -o a = \0o. Proof. move => ba; move: (ba) => [ob oa _]; apply /set0_P. move => t /Zo_P [tb /(oltP ob) s1]. exact: (oltNge (olt_leT s1 ba) (osum_Mle0 oa (ordinal_hi ob tb))). Qed. Lemma odiff_Mle a b: ordinalp a -> ordinalp b -> (b -o a) <=o b. Proof. move => oa ob; split; [ exact:(OS_diff oa ob) | exact | apply: Zo_S]. Qed. Lemma odiff_pr a b: a <=o b -> (ordinalp (b -o a) /\ b = a +o (b -o a)). Proof. move => ab;move: (ab) => [oa ob sab]; split; first exact: (OS_diff oa ob). case:(least_ordinal6 (fun b => sub a b -> b = a +o (b -o a)) ob);first by apply. set d := least_ordinal _ _ => [] [od H] [] sad. rewrite (osum_rec_def oa (OS_diff oa od)); set_extens t; last first. case/setU2_P; [ apply: sad | by move /funI_P => [z /Zo_hi za ->]]. move => td; apply/setU2_P; case: (oleT_el oa (ordinal_hi od td)). move => [_ _ /(H _ td)] => h. right; apply /funI_P; exists (t -o a) => //;apply:Zo_i; last by ue. exact:(ole_ltT_s od (odiff_Mle oa (ordinal_hi od td)) td). by move /(oltP oa); left. Qed. Lemma odiff_pr2 a b c: ordinalp a -> ordinalp b -> ordinalp c -> (a +o c = b) -> c = b -o a. Proof. move => oa ob oc h. have lab: a<=o b by rewrite -h; exact :(osum_Mle0 oa oc). have [pa pb]:= (odiff_pr lab). rewrite pb in h; exact: (osum2_simpl oc pa oa h). Qed. Lemma odiff_pos a b: a \0o [leab bab]; move: (odiff_pr leab) => [xx eq]. by apply :ord_ne0_pos => // h; case: bab; rewrite eq h (osum0r (proj31 leab)). Qed. Lemma odiff_pr1 a b: ordinalp a -> ordinalp b -> (a +o b) -o a = b. Proof. move=> oa ob. have [so sp] := (odiff_pr (osum_Mle0 oa ob)). by move: (osum2_simpl ob so oa sp). Qed. Lemma osum_1inf x: omega0 <=o x -> \1o +o x = x. Proof. move => pa; move: (odiff_pr pa) => [pb pc]; rewrite pc. by rewrite (osumA OS1 OS_omega pb) (osum_int_omega olt_1omega). Qed. Lemma oadd1_fix x: ordinalp x -> (\1o +o x = x <-> omega0 <=o x). Proof. move => ox; split; last by apply:osum_1inf. move => h; case: (oleT_el OS_omega ox) => // /olt_omegaP xN. move: (osum2_2int NS1 xN); rewrite h csumC - (Nsucc_rw xN). by move: xN => /NatP /finite_cP [_]. Qed. Lemma odiff_1inf x: omega0 <=o x -> x -o \1o = x. Proof. move => h; rewrite -{1} (osum_1inf h) odiff_pr1;fprops; exact: (proj32 h). Qed. Lemma odiff_pr1_wrong x: omega0 <=o x -> (x +o \1o) -o \1o <> x. Proof. move => h. have op:= proj32 h. move: (oltS op) => [l1 /nesym l2]. by rewrite (osucc_pr op) (odiff_1inf (oleT h l1)). Qed. Lemma oprec_nat x: \0o x x = osucc (x -o \1o). Proof. move => xnz xo. have pa: \1o <=o x by apply/ oge1P. have [sa sb]:= (odiff_pr pa). move: (osum_M0le OS1 sa); rewrite - sb => sc; move: (ole_ltT sc xo) => yo. have sd: inc (x -o \1o) omega0 by case/oltP0: yo. rewrite - (osucc_pr sa) {1} sb. by rewrite (osum2_2int NS1 sd) (osum2_2int sd NS1) csumC. Qed. Lemma oprec_nat2 x: \0o x (osucc x -o \1o) = osucc (x -o \1o). Proof. move => xz cox. have ox:= proj32_1 xz. have xb: inc x omega0 by case/oltP0: cox. rewrite -(oprec_nat xz cox);symmetry;apply:(odiff_pr2 OS1 (OS_succ ox) ox). by rewrite (osum2_2int NS1 xb) csumC -(osum2_2int xb NS1) (osucc_pr ox). Qed. Lemma oprec_Mlt a b: \0o a (a -o \1o) ap ab. have [[oa ob _] _ ] := ab. case: (oleT_el OS_omega oa) => af. by rewrite (odiff_1inf af) (odiff_1inf (oleT af (proj1 ab))). case: (oleT_el OS_omega ob) => bf. rewrite (odiff_1inf bf); apply: olt_leT bf. exact: (ole_ltT (odiff_Mle OS1 oa) af). apply /oltSSP. by rewrite - (oprec_nat ap af) - (oprec_nat (olt_leT ap (proj1 ab)) bf). Qed. (** ** Ordinal division *) Definition sincr_ofs (f: fterm) := (forall x y, x (f x) ordinalp y -> ordinalp y' -> (h y) <=o a -> a (h y') <=o a -> a y = y'. Proof. move=> oih oy oy' le1 le2 le3 le4. wlog: y y' oy oy' le1 le2 le3 le4 / y // ll; first by apply. by move=> aux;symmetry; apply: aux. have lt2:=(ole_ltT le3 le2). move /oleSltP => h2. case: (equal_or_not (osucc y) y'). by move=> h3; move: lt2=> [_]; rewrite h3. move=> h3; have h4: (osucc y) [/(oltNge lt2) []]. Qed. Definition odiv_pr0 a b q r := [/\ ordinalp q, ordinalp r, a = (b *o q) +o r & r ordinalp b -> odiv_pr0 a b q r -> odiv_pr0 a b q' r' -> (q = q' /\ r = r'). Proof. move => oa ob pa pb. have aux: forall q r, odiv_pr0 a b q r -> (b *o q <=o a /\ a q1 r1 [oq or -> rb]; rewrite (oprod2_succ ob oq). split; first by apply:(osum_Mle0 (OS_prod2 ob oq) or). apply:(osum_Meqlt rb (OS_prod2 ob oq)). move: (aux _ _ pa) (aux _ _ pb) => [s1 s2] [s3 s4]. pose h y := b *o y. move: pa pb => [oq or e1 rb] [oq' or' e2 _]. have bp: \0o u v uv; apply: oprod_Meqlt. move: (sincr_bounded_unique sii oq oq' s1 s2 s3 s4). move => sq; split => //; rewrite e1 sq in e2. exact: (osum2_simpl or or' (OS_prod2 ob oq') e2). Qed. Lemma odivision_exists a b c: ordinalp b -> ordinalp c -> a exists q r, odiv_pr1 a b c q r. Proof. move => ob oc. move /(oltP (OS_prod2 ob oc)); rewrite (oprod_rec_def ob oc). move => /funI_P [z /setX_P [za /(oltP ob) zb /(oltP oc) zc] ->]. by move: (proj31_1 zb)(proj31_1 zc) => op oq; exists (Q z), (P z). Qed. Lemma odivision_exists1 a b: ordinalp a -> \0o exists q r, odiv_pr0 a b q r. Proof. move => oa bp. have: a [q [r [h _]]]; exists q,r. Qed. Definition oquorem a b := select (fun z => a = b *o (P z) +o (Q z)) ((osucc a) \times b). Lemma oquoremP a b: ordinalp a -> \0o odiv_pr0 a b (P (oquorem a b)) (Q (oquorem a b)). Proof. move => oa bp. set E := (osucc a) \times b. pose p z := a = b *o (P z) +o (Q z). have osa := (OS_succ oa). have ob := (proj32_1 bp). have: a H. have pa: (exists2 x, inc x E & p x). move: H => [q [r [[oq or eq rb] h2]]]; exists (J q r); last by rewrite /p;aw. apply/setX_P; split;[fprops | by aw; apply/(oltP osa) | aw]. by apply /(oltP ob). have pb:singl_val2 (inc^~ E) p. move => u v /setX_P [pu /(oltP osa) oq /(oltP ob) or] vu. move => /setX_P [pv /(oltP osa) oq' /(oltP ob) or'] vv. move: (proj31_1 or)(proj31_1 oq) => r1 r2. move: (proj31_1 or')(proj31_1 oq') => r1' r2'. have ha: odiv_pr0 a b (P u) (Q u) by []. have hb: odiv_pr0 a b (P v) (Q v) by []. by move: (odivision_unique oa ob ha hb) => [hc hd]; apply/pair_exten. move: (select_pr pa pb) => [pc /setX_P [_ /(oltP osa) oq /(oltP ob) or]]. move: (proj31_1 or)(proj31_1 oq) => r1 r2. done. Qed. Lemma oquoremP2 a b q r: ordinalp a -> \0o odiv_pr0 a b q r -> q = (P (oquorem a b)) /\ r = (Q (oquorem a b)). Proof. move => pa pb pc. move:(oquoremP pa pb) => pd. exact (odivision_unique pa (proj32_1 pb) pc pd). Qed. End Ordinals1. Export Ordinals1.