Library sset11

Theory of Sets : Ordinals

Copyright INRIA (2009-2013 Apics; Marelle Team (Jose Grimm).

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

Disjoint union of families of substrates
ordinal sum of a family of orders g indexed by the substrate of r

Lemma order_prod_pr r r': order r -> order r' ->
 (order_prod2 r r') \Is (order_sum r' (cst_graph (substrate r') r)).
Proof.
move => or or'.
have oa: (orsum_ax r' (cst_graph (substrate r') r)).
  split => //;hnf; bw;move=> i isr; bw.
set fo:=order_sum r' _.
have odf: order fo by rewrite /fo; fprops.
have s1:= (orsum_sr oa).
move: (orprod2_or or odf) (orprod2_sr or or').
set io := order_prod2 r r'; move => o2 s2.
pose f x := J (Vg x C1) (Vg x C0).
have ta: lf_axiom f (substrate io) (substrate fo).
  move=> t; rewrite /fo s1 s2; move /setX2_P => [fgt dt va vb].
  apply: disjointU_pi; bw.
have bf: bijection (Lf f (substrate io) (substrate fo)).
  apply: lf_bijective =>//.
    move=> u v;rewrite s2 /f; move=> ud vd eq.
    move: (pr2_def eq)(pr1_def eq) => p1 p2.
    apply: (setXf_exten ud vd) => i itp; try_lvariant itp.
  rewrite s1 /fam_of_substrates /cst_graph.
  move=> y ys; move:(du_index_pr1 ys); rewrite Lg_domain.
  move=> [Qsr]; bw => Psr py.
  exists (variantLc (Q y) (P y)).
    rewrite s2; apply /setX2_P;split; bw; fprops.
  by rewrite /f; bw; aw; rewrite py.
exists (Lf f (substrate io) (substrate fo));split; aw.
    rewrite /io; fprops.
  red; split;aw.
hnf; aw;move=> x y xs ys; aw.
move : (ta _ xs) (ta _ ys) => qa qb.
have p1: inc (Vg x C0) (substrate r').
  by move: xs; rewrite s2; move /setX2_P => [_ _].
apply (iff_trans (orprod2_gleP or or' _ _)); rewrite - s2.
symmetry; apply (iff_trans (orsum_gleP _ _ _ _)).
have ->: sum_of_substrates (cst_graph (substrate r') r) = substrate fo by aw.
split; move => [_ _ xx]; split => //; move: xx;
 rewrite /f /order_sum_r !pr1_pair !pr2_pair; bw; case; fprops.
Qed.

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 => //; move => i ie; exact (proj1 (alw _ ie)).
move h: (cardinal (substrate r)) => n.
have nB: inc n Bnat by move: fs;rewrite - h; move /BnatP.
clear wor sr fs; move:n nB r g lea alw h.
apply: cardinal_c_induction.
  move=> r g lea alw cr.
  move:(orprod_osr lea) => [lo].
  rewrite /prod_of_substrates /fam_of_substrates.
  move: lea => [_ <- _];rewrite (cardinal_nonemptyset cr) setXb_0' => s1.
  exact:(worder_set1 (conj lo s1)).
move=> n nB hrec r g lea alwo csr.
have lo: (order (order_prod r g)) by fprops.
split =>//.
move: (lea) => [[or wor] sr alo].
case: (emptyset_dichot (substrate r)) => nesr.
  rewrite nesr cardinal_set0 in csr.
  symmetry in csr; case:(succ_nz csr).
move: (worder_least (proj31 lea) nesr) => [i []]; rewrite {1} sr => isr ilsr.
bw => x xsr [x0 x0x].
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: (alwo _ isr) => [or' wor']; move: (wor' _ sYs neY) => [z []]; aw.
move => zY zl {wor wor'}.
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: (iorder_gle1 (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 rewrite /I1; 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 _ _]; rewrite /r1;apply: induced_wor => //.
    symmetry; rewrite /r1; aw.
  rewrite /g1; hnf.
  move=> 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 /r1; aw; move: (card_succ_pr1 (substrate r) i).
  rewrite - sr in isr.
  rewrite setC1_K // -/I1 csr => h.
  symmetry; apply: succ_injective1; fprops.
move: (hrec _ _ la1 alw cs) =>[or1 wo1].
set X2 := fun_image X1 (fun z => restr z I1).
have X2s: sub X2 (substrate (order_prod r1 g1)).
  bw;rewrite /prod_of_substrates /fam_of_substrates.
  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].
  have aa: sub I1 (domain u) by rewrite du - sr.
  have ->: domain (restr u I1) = I1 by bw.
  bw; rewrite dg1; split;fprops; move => j jI1; bw.
  rewrite /g1; bw; apply: iVV; ue.
have neX2: (nonempty X2).
  move: zY => /funI_P [z0 z0x pz0]; exists (restr z0 I1).
  by apply /funI_P; exists z0 => //; apply: Zo_i.
move: (wo1 _ X2s neX2)=> [w []]; aw; move=> wX2 wle.
move: wX2 => /funI_P [v vX1 rv].
have vx: inc v x by move: vX1 => /Zo_P [].
have sxs: sub x (substrate (order_prod r g)) by bw.
exists v; red; aw; split =>//.
move=> u ux1; apply /iorder_gleP => //.
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: (iorder_gle1 (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: (xsr _ vx) => /prod_of_substratesP [fgv dv vp].
move: (xsr _ ux1) => /prod_of_substratesP [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.
  red; 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: forall r r',
  worder r -> worder r' -> worder (order_prod2 r r').
Proof.
move: cdo_wor => [pa pb] r r' wor wor'; apply: orprod_wor => //.
- split => //; bw.
- hnf; bw; move=> i ind; try_lvariant ind.
- apply: finite_set_scdo.
Qed.

Lemma orsum2_wor: forall r r',
  worder r -> worder r' -> worder (order_sum2 r r').
Proof.
move: cdo_wor => [pa pb] r r' wor wor'; apply: orsum_wor => //; 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 ->
  graph_on ordinal_le a = ordinal_o a.
Proof.
move => oa.
have [p2 p1]:= (wordering_ordinal_le_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 => //; ord_tac0.
Qed.

Lemma set_ord_lt_prop3 a: ordinalp a ->
  ordinal (graph_on ordinal_le a) = a.
Proof.
move=> oa; rewrite (set_ord_lt_prop3a oa); apply: (ordinal_o_o oa).
Qed.

Lemma finite_ordinal1 n: inc n Bnat ->
  n = ordinal (Bint_co n).
Proof.
move=> nB.
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 red; rewrite cnn; apply /BnatP.
have w1 := (Bintco_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 : equipotent (source f) (target f) by exists f;split => //.
  rewrite tf sf; rewrite (proj2 w1).
set S := substrate _ => aux.
have p3: equipotent (substrate (ordinal_o n)) S.
   rewrite pa; eqtrans (Bint n).
   by apply /card_eqP; rewrite card_Bint.
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 finite_ordinal2 n: inc n Bnat ->
   n = Bint n.
Proof.
move=> nB.
have cn: cardinalp n by fprops.
have on:=(OS_cardinal cn).
set_extens t.
  move => tn; apply/(BintP nB).
  move /BnatP: nB => fn; move: (finite_o_increasing tn fn)=> /BnatP tB.
  apply:ordinal_cardinal_lt3 => //; [ fprops | by apply /(ord_ltP on)].
move /(BintP nB) => /(ordinal_cardinal_lt) => h1.
by apply /(ord_ltP on).
Qed.

Lemma ord_omega_pr: omega0 = ordinal Bnat_order.
Proof.
move: Bnat_order_wor => [bwo _].
suff: (ordinal_o omega0 = Bnat_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 Bnat_order_leP.
 split => //;split => //; fprops.
by move/Bnat_order_leP => [pa pb [_ _ pc]];apply /graph_on_P1.
Qed.

Lemma cardinal_Bnat: cardinal Bnat = Bnat.
Proof. apply: card_card; apply: CS_omega. Qed.

Lemma olt_omegaP x: (x <o omega0) <-> inc x Bnat.
Proof. apply: (ord_ltP OS_omega). Qed.

Lemma clt_omegaP x: (x <c omega0) <-> inc x Bnat.
Proof.
split => h; first by move: (ordinal_cardinal_lt h) => /olt_omegaP.
by apply: ordinal_cardinal_lt3; [fprops| apply: CS_omega | apply /olt_omegaP].
Qed.

Lemma omega_nz: omega0 <> \0o.
Proof. by move: BS0 => /olt_omegaP [_ ?]; apply: nesym. Qed.

Lemma ord_lt_0omega: \0o <o omega0.
Proof. apply /olt_omegaP; apply: BS0. Qed.

Lemma ord_lt_1omega: \1o <o omega0.
Proof. apply /olt_omegaP; apply: BS1. Qed.

Lemma ord_le_2omega: \2o <=o omega0.
Proof. by move: BS2 => /olt_omegaP; case. Qed.

Lemma ord_lt_2omega: \2o <o omega0.
Proof. apply /olt_omegaP; apply: BS2. Qed.

Properties of zero

Lemma ordinal_o_set0: ordinal_o emptyset = emptyset.
Proof. by apply: empty_substrate_zero; rewrite ordinal_o_sr. Qed.

Lemma ordinal0_pr: ordinal emptyset = \0o.
Proof. rewrite - ordinal_o_set0; exact (ordinal_o_o OS0). Qed.

Lemma ordinal0_pr1 x: order x -> 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 succo_nz x : succ_o x <> \0o.
Proof.
move => h; case: (@in_set0 x); rewrite -/ord_zero - h /succ_o; fprops.
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 xy].
by rewrite xy ordinal1_pr.
Qed.

ordinal sum and product


Definition ord_sum r g :=
   ordinal (order_sum r (Lg (domain g) (fun z => (ordinal_o (Vg g z))))).
Definition ord_prod r g :=
   ordinal (order_prod r (Lg (domain g) (fun z => (ordinal_o (Vg g z))))).
Definition ord_sum2 a b := ordinal (order_sum2 (ordinal_o a) (ordinal_o b)).
Definition ord_prod2 a b := ordinal (order_prod2 (ordinal_o a) (ordinal_o b)).

Notation "x +o y" := (ord_sum2 x y) (at level 50).
Notation "x *o y" := (ord_prod2 x y) (at level 40).

Lemma OS_sum r g: worder_on r (domain g) -> ordinal_fam g ->
  ordinalp (ord_sum r g).
Proof.
move=> [or sr] alo ; apply: OS_ordinal.
apply: orsum_wor ;[ exact | 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 (ord_prod 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 = ord_sum canonical_doubleton_order (variantLc a b).
Proof. by rewrite /ord_sum2 /ord_sum /order_sum2 variantLc_comp. Qed.

Lemma oprod2_rw a b:
  a *o b = ord_prod canonical_doubleton_order (variantLc b a).
Proof. by rewrite /ord_prod2 /ord_prod /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.
red; 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.
right;split => //; apply /ojj => //; by 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) =
    ord_sum r (Lg (substrate r) (fun i => ordinal (Vg g i))).
Proof.
move => [wor sr] alo.
have or: order r by fprops.
rewrite /ord_sum; apply: ordinal_o_isu1.
- by apply: orsum_wor.
- apply: orsum_wor; [ exact | 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.
move: (worder_invariance aux wor) => 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').
  red; 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 | red; 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: (order r) by move: wor => [or _].
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) =
    ord_prod r (Lg (substrate r) (fun i => ordinal (Vg g i))).
Proof.
move => [wor sr] alo fsr.
have or: order r by fprops.
rewrite /ord_prod; 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 /ord_prod2 /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 /ord_sum2; 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 /ord_prod2; 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 = ord_sum 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 /ord_prod2 /ord_sum.
have ->: domain (cst_graph (substrate c) a) = substrate c.
   rewrite /cst_graph; bw.
apply: ordinal_o_isu1.
  by apply: orprod2_wor; apply: ordinal_o_wor.
  apply: orsum_wor; [exact | 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 ->
  ord_sum r x = \0o.
Proof.
move=> sre.
rewrite /ord_sum 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 -> ord_prod 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 /ord_prod 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) ->
  ord_sum 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 /ord_sum.
set g := Lg _ _.
have osa: orsum_ax r g.
   rewrite /g; red; bw;split => //;hnf; bw.
   rewrite dxe => i /set1_P ->; bw ; fprops.
have wos: worder (order_sum r g).
  rewrite /g;apply: orsum_wor=> //; bw; fprops.
  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 (red;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.
red; 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.
   move /orsum_gleP => [_ _]; case; first by move => [_]; rewrite Qu Qv.
   by move => [_].
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) ->
  ord_prod 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 /ord_prod.
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).
red;rewrite /bijection_prop lf_source lf_target; split;fprops.
  split; aw;apply: lf_bijective =>//.
  move=> y ys; exists (Lg (singleton e) (fun _:Set => y)); bw; fprops.
  rewrite slo' dg; bw; apply /setXb_P; fprops;split;fprops; bw.
  by move=> i /set1_P ->; bw; fprops; rewrite - Hf'.
red; 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).
  red; 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).
red; 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.
red; 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) ->
  ord_sum r g = ord_sum (induced_order r j) (restr g j).
Proof.
move => [wor sr] odf sj alne.
have or: order r by fprops.
apply: ordinal_o_isu1.
    apply: orsum_wor; [ exact | bw | hnf; bw => i idg; bw; fprops].
  apply: orsum_wor; [ apply: induced_wor => //; ue |bw; aw; ue | ].
  hnf; bw; move=> i idg; bw; fprops.
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)).
     rewrite /g1; apply: fgraph_exten;[ fprops | fprops | bw;fprops | red; bw ].
    move => x xd; bw; by 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).
  red; 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).
red; 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.
red; 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) ->
  ord_prod r g = ord_prod (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 /ord_prod; 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)).
  rewrite /g1; apply: fgraph_exten;bw; fprops.
  by move => 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)).
  red; 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;red; split; fprops; first split; aw; bw.
red; 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.
  red; 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.
   red; 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.
  red; 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; apply: f_equal; apply: Lg_exten.
  move=> i idg; rewrite /F;bw; last by apply: la1 =>//.
  rewrite /prod_of_substrates /fam_of_substrates; bw.
  apply: 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 => //.
red; 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 red; 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 =>
    ord_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in
  ord_sum r g = ord_sum r' (Lg (domain g') (order_sum_assoc_aux)).
Proof.
move=> [wor sr] [wor' sr'] alB alw oal osa.
rewrite /ord_sum.
have oa': orsum_ax r' g'.
   split;fprops; move => j jd; exact (proj1 (alw _ jd)).
apply: ordinal_o_isu1.
    apply: orsum_wor => //;hnf; bw => i idg /=; bw; fprops.
  apply: orsum_wor => //;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'';red; 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 /ord_sum; bw.
set s:= order_sum _ _.
have -> : (aux' i = s).
  rewrite /aux' /s; apply: 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.
rewrite /s.
apply: orsum_wor; [by apply: alw | bw | 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 =>
    ord_prod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in
  ord_prod r g = ord_prod r' (Lg (domain g') order_prod_assoc_aux).
Proof.
move=> [wor sr] [wor' sr'] alB alw oal fs fs' alfs osa.
rewrite /ord_prod.
have oa': orsum_ax r' g'.
  split;fprops; red; move => j jd; exact (proj1 (alw _ jd)).
apply: ordinal_o_isu1; bw.
    apply: orprod_wor; red; bw => //; hnf; bw;move=> i idg; bw; fprops.
  apply: orprod_wor; red; 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'';red; 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 /ord_prod; bw.
set s:= order_prod _ _.
have -> : (ax' i = s).
  rewrite /ax' /s; apply: 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.
rewrite /s.
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 (ord_sum2 a).
Proof.
move => oa ob.
case: (least_ordinal6 (fun b => a +o b = a \cup fun_image b (ord_sum2 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: TP_ne TP_ne1 => 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.
    move:(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.
    set x := J w C0.
    have xsr: inc x (substrate r) by rewrite sr; apply: candu2_pra.
    move: (transdef_tg3 woc (substrate_segment o1) h xsr).
    rewrite /f {1 2}/x; aw; Ytac0 => ->; rewrite -/ff;Wtac.
  move /funI_P: wt1 => [z zc ->]; set x := J z C1.
  have xsr: inc x (substrate r) by rewrite sr; apply: candu2_prb.
  move: (transdef_tg3 woc (substrate_segment o1) h xsr).
  rewrite /f {1 3}/x; 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: ordinalp u by ord_tac.
have ov: ordinalp v by ord_tac.
rewrite (osum_rec_def (OS_prod2 oa ou) ov).
set_extens t.
  have xca:inc x (product2 c a) by 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: inc (Q z) c by ord_tac0.
    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: inc z a by ord_tac0.
  apply/segmentP; split; last first.
      move => sv; move: (f_equal (Vg ^~C1) sv); bw.
      by move => s;apply: (ordinal_irreflexive ov); rewrite {1} /v - 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.
apply :setXp_i => //; apply /ord_ltP; [ord_tac | split => //; split => //].
ord_tac.
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 /ord_prod2 /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 /ord_prod2 /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 ord_succ_pr x: ordinalp x -> x +o \1o = succ_o 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 //; ord_tac.
move => tc; apply/funI_P; ex_tac; rewrite prc //; ord_tac.
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 //; ord_tac.
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 //; ord_tac.
move => tx; apply /funI_P; exists (J \0o t).
  by apply:setXp_i; fprops; apply/set1_P.
aw; rewrite H // osum0r //; ord_tac.
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 osum_prodD 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] ->]].
  have opu: ordinalp (P u) by ord_tac.
  have oqu: ordinalp (Q u) by ord_tac.
  have opz: ordinalp (P z) by ord_tac.
  have obqu:= (OS_prod2 ob oqu).
  rewrite (osum_prodD 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].
have opu: ordinalp (P u) by ord_tac.
have oqu: ordinalp (Q u) by ord_tac.
have oqz: ordinalp (Q z) by ord_tac.
rewrite (osumA (OS_prod2 (OS_prod2 oa ob) oqz) (OS_prod2 oa oqu) opu).
rewrite -(H _ qzd) - (osum_prodD (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

Hint Rewrite card_Bint : bw.

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: inc n Bnat ->
  osum_expansion f (succ n) = f n +o (osum_expansion f n).
Proof. move => nb; exact: induction_terms. Qed.

Lemma oprod_expansion_succ n f: inc n Bnat ->
  oprod_expansion f (succ 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 _ BS0) 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 _ BS0) oprod_expansion0.
by rewrite oprod1l.
Qed.

Definition ord_below_n f n := (forall k, k<c n -> ordinalp (f k)).
Definition same_below (e e': fterm) n:= (forall i, i <c n -> e i = e' i).

Lemma OS_osum_expansion n f:
  inc n Bnat -> ord_below_n f n ->
  ordinalp (osum_expansion f n).
Proof.
move: n;apply: cardinal_c_induction.
  by move => _; rewrite osum_expansion0; fprops.
move => n nB Hrec h1; rewrite (osum_expansion_succ _ nB); apply: OS_sum2.
  by apply: h1; apply: card_lt_succ.
apply: Hrec => k kn; apply: h1; move: (card_le_succ nB) => h2; co_tac.
Qed.

Lemma OS_oprod_expansion n f:
  inc n Bnat -> ord_below_n f n ->
  ordinalp (oprod_expansion f n).
Proof.
move: n;apply: cardinal_c_induction.
  by move => _; rewrite oprod_expansion0; fprops.
move => n nB Hrec h1; rewrite (oprod_expansion_succ _ nB); apply: OS_prod2.
  apply: Hrec => k kn; apply: h1; move: (card_le_succ nB) => h2; co_tac.
by apply: h1; apply: card_lt_succ.
Qed.

Lemma osum_expansion_exten f g n:
  inc n Bnat -> same_below f g n ->
  osum_expansion f n = osum_expansion g n.
Proof.
move: n; apply: cardinal_c_induction.
  by move => _; rewrite ! osum_expansion0.
move => n nB Hrec sv;rewrite !(osum_expansion_succ _ nB).
move: (card_lt_succ nB) => pa.
rewrite (sv _ pa) Hrec // => i lin; apply: sv;co_tac.
Qed.

Lemma oprod_expansion_exten f g n:
  inc n Bnat -> same_below f g n ->
  oprod_expansion f n = oprod_expansion g n.
Proof.
move: n; apply: cardinal_c_induction.
  by move => _; rewrite ! oprod_expansion0.
move => n nB Hrec sv;rewrite !(oprod_expansion_succ _ nB).
move: (card_lt_succ nB) => pa.
rewrite (sv _ pa) Hrec // => i lin; apply: sv;co_tac.
Qed.

Lemma osum_expansionA n m f:
  inc n Bnat -> inc m Bnat -> 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 => nB mB; move: m mB n nB f; apply: cardinal_c_induction.
  move => n nB f; rewrite (bsum0r nB) (osum_expansion0) => fo.
  rewrite osum0l //; apply:OS_osum_expansion => //.
move => m mB Hrec n nB f.
have nmB: inc (n +c m) Bnat by fprops.
move:(card_lt_succ nmB) => lt1.
rewrite (csum_via_succ _ mB) (osum_expansion_succ _ nmB) => fo.
have pa:forall k, k <c n +c m -> ordinalp (f k).
  move => k [kp _]; apply: fo; co_tac.
have pb: ordinalp (f (n +c m)) by apply: fo.
have pc: ordinalp (osum_expansion (fun z : Set => f (z +c n)) m).
  apply: OS_osum_expansion => // k km; apply: fo.
  move: (csum_Mlteq nB mB km); rewrite csumC (csumC m) => h; co_tac.
have pd: ordinalp (osum_expansion f n).
  apply: OS_osum_expansion => // k km; apply: fo.
  move: (card_le_ltT (csum_M0le m (CS_Bnat nB)) lt1) => le1; co_tac.
by rewrite Hrec // (osumA pb pc pd) (osum_expansion_succ _ mB) csumC.
Qed.

Lemma oprod_expansionA n m f:
  inc n Bnat -> inc m Bnat -> 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 => nB mB; move: m mB n nB f; apply: cardinal_c_induction.
  move => n nB f; rewrite (bsum0r nB) (oprod_expansion0) => fo.
  rewrite oprod1r //; apply:OS_oprod_expansion => //.
move => m mB Hrec n nB f.
have nmB: inc (n +c m) Bnat by fprops.
move:(card_lt_succ nmB) => lt1.
rewrite (csum_via_succ _ mB) (oprod_expansion_succ _ nmB) => fo.
have pa:forall k, k <c n +c m -> ordinalp (f k).
  move => k [kp _]; apply: fo; co_tac.
have pb: ordinalp (f (n +c m)) by apply: fo.
have pc: ordinalp (oprod_expansion (fun z : Set => f (z +c n)) m).
  apply: OS_oprod_expansion => // k km; apply: fo.
  move: (csum_Mlteq nB mB km); rewrite csumC (csumC m) => h; co_tac.
have pd: ordinalp (oprod_expansion f n).
  apply: OS_oprod_expansion => // k km; apply: fo.
  move: (card_le_ltT (csum_M0le m (CS_Bnat nB)) lt1) => le1; co_tac.
by rewrite Hrec // - (oprodA pd pc pb) (oprod_expansion_succ _ mB) csumC.
Qed.

Properties of ordering


Lemma ord_lt_01: \0o <o \1o.
Proof.
apply /ord_ltP0; split => //; rewrite / \1o/card_one; fprops.
Qed.

Lemma ord_lt_12: \1o <o \2o.
Proof.
by move: ord_lt_01 => /ord_lt_succ_succP; rewrite succ_o_zero succ_o_one.
Qed.

Lemma ord_lt_02: \0o <o \2o.
Proof. move: ord_lt_01 ord_lt_12 => p1 [p2 _]; ord_tac. Qed.

Lemma ord_lt0_succ x: ordinalp x -> \0o <o (succ_o x).
Proof. by move => ox; apply /ord_lt_succP; apply: ozero_least. Qed.

Lemma ord2_lt_P x: \2o <=o x <-> \1o <o x.
Proof. rewrite - succ_o_one; symmetry; exact:ord_succ_ltP. Qed.

Lemma ord2_trichotomy x: ordinalp x ->
  [\/ 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 /ord2_lt_P; split =>//; apply: ord_ge1.
Qed.

Lemma ord2_trichotomy1 x: \2o <=o x -> (x <> \0o /\ x <> \1o).
Proof.
move=> h; split.
    move=> xz; rewrite xz in h; move: (ord_le0 h).
    apply: card2_nz.
  move => xz; move: h; rewrite xz; apply/ord2_lt_P; by move=> [_].
Qed.

Lemma limit_positive x: limit_ordinal x -> \0o <o x.
Proof. move=> [ox xne _]; apply: ord_ne_pos => //; ex_tac. Qed.

Lemma limit_nz x: limit_ordinal x -> x <> \0o.
Proof. move /limit_positive => h; ord_tac1. Qed.

Lemma osum_Meqlt a b c:
  a <o b -> ordinalp c -> (c +o a) <o (c +o b).
Proof.
move => /ord_ltP0 [oa ob ab] oc; apply /ord_ltP; fprops.
rewrite (osum_rec_def oc ob); apply /setU2_P; right; apply/funI_P; ex_tac.
Qed.

Lemma oprod_Meqlt a b c:
  a <o b -> \0o <o c -> (c *o a) <o (c *o b).
Proof.
move => /ord_ltP0 [oa ob ab] /ord_ltP0 [oz oc zc].
apply /ord_ltP; 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: (ord_le_to_el oa ob) => // h1; move: (osum_Meqlt h1 oc) => h2; ord_tac.
Qed.

Lemma oprod_Meqler a b c: ordinalp a -> ordinalp b -> \0o <o c ->
   c *o a <=o c *o b -> a <=o b.
Proof.
move => oa ob oc h.
case: (ord_le_to_el oa ob) => // h1; move: (oprod_Meqlt h1 oc) => h2; ord_tac.
Qed.

Lemma oprod2_pos a b: \0o <o a -> \0o <o b -> \0o <o a *o b.
Proof. by move => 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: ord_leR; 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: (ord_zero_dichot oc) => cz.
   rewrite cz oprod0l oprod0l; apply: (ord_leR OS0).
case: (equal_or_not a b) => nab.
  by rewrite nab; apply: ord_leR; apply: (OS_prod2 oc (proj32 ab)).
exact: (proj1 (oprod_Meqlt (conj ab nab) cz)).
Qed.

Lemma ord_le_ltT_s a b c: ordinalp c -> a <=o b -> inc b c -> inc a c.
Proof.
move => oc ab /(ord_ltP oc) bc; apply /(ord_ltP oc); ord_tac.
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:(ord_le_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 => //; ord_tac1.
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 => //; ord_tac1.
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: (ord_leT (y:= a +o d)).
apply:osum_Meqle => //; ord_tac.
apply:osum_Mleeq => //; ord_tac.
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: (ord_le_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: (ord_leT (y:= a *o d)).
apply:oprod_Meqle => //; ord_tac.
apply:oprod_Mleeq => //; ord_tac.
Qed.

Lemma oprod_Mle1 a b:
  ordinalp a -> \0o <o b -> a <=o (a *o b).
Proof.
move=> oa /ord_ge1P ba.
rewrite - {1} (oprod1r oa); apply: oprod_Mlele => //; ord_tac.
Qed.

Lemma oprod_M1le a b:
  \0o <o a -> ordinalp b-> b <=o (a *o b).
Proof.
move=> /ord_ge1P oa ob.
rewrite - {1} (oprod1l ob); apply: oprod_Mlele => //; ord_tac.
Qed.

Lemma oprod_Meq1lt b c:
  \1o <o b -> \0o <o c -> c <o (c *o b).
Proof.
move => 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) <o (c +o b) -> a <o b.
Proof.
move => oa ob oc olt.
case: (ord_le_to_el ob oa) => // oba.
suff aux: (c +o b) <=o (c +o a) by ord_tac.
apply: osum_Mlele => //; ord_tac.
Qed.

Lemma osum_Mlteqr a b c:
  ordinalp a -> ordinalp b -> ordinalp c ->
  (a +o c) <o (b +o c) -> a <o b.
Proof.
move => oa ob oc olt.
case: (ord_le_to_el ob oa) => // oba.
suff aux: (b +o c) <=o (a +o c) by ord_tac.
apply: osum_Mlele => //; ord_tac.
Qed.

Lemma oprod_Meqltr a b c:
  ordinalp a -> ordinalp b -> ordinalp c ->
  (c *o a) <o (c *o b) -> a <o b.
Proof.
move => oa ob oc olt.
case: (ord_le_to_el ob oa) => // oba.
suff aux: (c *o b) <=o (c *o a) by ord_tac.
apply: oprod_Mlele => //; ord_tac.
Qed.

Lemma oprod_Mlteqr a b c:
  ordinalp a -> ordinalp b -> ordinalp c ->
  (a *o c) <o (b *o c) -> a <o b.
Proof.
move => oa ob oc olt.
case: (ord_le_to_el ob oa) => // oba.
suff aux: (b *o c) <=o (a *o c) by ord_tac.
apply: oprod_Mlele => //; ord_tac.
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: (ord_le_to_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 <o c ->
  c *o a = c *o b -> a = b.
Proof.
move=> oa ob oc eq.
by case: (ord_le_to_ell oa ob) => h //;
   move: (oprod_Meqlt h oc); rewrite eq; move=> [_]; case.
Qed.

Lemma oprod2_simpl1 a c: ordinalp a -> \0o <o c -> 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: (ord_zero_dichot ox) => xz.
  by move: s0; rewrite xz (osum0l oy) => yz.
by move: (ord_lt_leT xz (osum_Mle0 ox oy)) => [];rewrite s0.
Qed.

Lemma oprod_a_ab a b: \0o <o a -> 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 (ord_lt1 (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.
move: (ord_ne0_pos ob bz) => b1.
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 ord_lt_02 sv).
have: a <o (succ_o \1o) by rewrite succ_o_one; split.
move /ord_lt_succP.
case: (equal_or_not a \0c) => az.
  by move: ab1; rewrite az (oprod0l) => bad; case: card2_nz.
move: (ord_ge1 oa az)=> a4 a3; left; ord_tac.
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 osum_prodD // oprod1r //. Qed.

Lemma osum2_succ x y:
   ordinalp x -> ordinalp y -> succ_o (x +o y) = x +o (succ_o y).
Proof.
move=> oa ob.
rewrite -(ord_succ_pr ob) (osumA oa ob OS1) ord_succ_pr ;fprops.
Qed.

Lemma oprod2_succ x y: ordinalp x -> ordinalp y ->
   x *o (succ_o y) = (x *o y) +o x.
Proof.
move=> ox oy.
rewrite -(ord_succ_pr oy) (osum_prodD oy OS1 ox); rewrite oprod1r //.
Qed.

Lemma osum2_2int a b:
  inc a Bnat -> inc b Bnat -> a +o b = a +c b.
Proof.
move=> aB bB;move: b bB.
have oa: ordinalp a by apply: OS_cardinal; fprops.
apply: cardinal_c_induction.
  by rewrite (bsum0r aB) (osum0r oa).
move=> n nB hrec.
have p1: ordinalp n by apply: OS_cardinal; fprops.
have p2: finite_c n by apply /BnatP.
have p3: finite_c (a +c n) by apply /BnatP; fprops.
rewrite (csum_via_succ _ nB) (succ_of_finite p2) (succ_of_finite p3).
by rewrite - hrec - (osum2_succ oa p1).
Qed.

Lemma oprod2_2int a b:
  inc a Bnat -> inc b Bnat -> a *o b = a *c b.
Proof.
move=> aB bB;move: b bB.
have oa: ordinalp a by apply: OS_cardinal; fprops.
apply: cardinal_c_induction.
  rewrite cprod0r oprod0r //.
move=> n nB hrec.
have p1: inc (a *c n) Bnat by fprops.
have p2: finite_c n by apply /BnatP.
rewrite (cprod_via_sum a nB) - (osum2_2int p1 aB) (succ_of_finite p2) - hrec.
apply: oprod2_succ => //; apply: OS_cardinal; fprops.
Qed.

Lemma osum2_lt_omega a b:
   a <o omega0 -> b <o omega0 -> (a +o b) <o omega0.
Proof.
move /olt_omegaP => aB /olt_omegaP bB; apply /olt_omegaP.
rewrite osum2_2int //; fprops.
Qed.

Lemma oprod2_lt_omega a b:
   a <o omega0 -> b <o omega0 -> (a *o b) <o omega0.
Proof.
move /olt_omegaP => aB /olt_omegaP bB;apply /olt_omegaP.
rewrite oprod2_2int //; fprops.
Qed.

Lemma osum_11_2: \1o +o \1o = \2o.
Proof. by move:(osum2_2int BS1 BS1); rewrite card_two_pr. Qed.

Lemma ord_double x:
  ordinalp x -> x *o \2o = x +o x.
Proof.
by move=> Bx; rewrite - osum_11_2 (osum_prodD OS1 OS1 Bx) (oprod1r Bx).
Qed.

Lemma osum_int_omega n:
  n <o omega0 -> 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 /(ord_ltP oo) /(osum2_lt_omega no); ord_tac.
Qed.

Lemma oprod_int_omega n:
  n <o omega0 -> \0c <o n -> 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 /(ord_ltP oo) /(osum2_lt_omega).
  apply (oprod2_lt_omega no); ord_tac.
by apply/(ord_ltP oo); apply: son.
Qed.

Lemma osum2_nc (x := \1o) (y := omega0):
   x +o y <> y +o x.
Proof.
rewrite (osum_int_omega ord_lt_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 ord_lt_2omega ord_lt_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 ord_lt_1omega ord_lt_01) (osum2_2int BS1 BS1).
rewrite card_two_pr (oprod_int_omega ord_lt_2omega ord_lt_02) => h.
symmetry in 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 /ord_sum2.
set w := order_sum2 _ _.
have w1: worder w by rewrite /w;fprops.
move: (OS_ordinal w1) =>pa.
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.

Lemma oprod_cardinal x y:
  ordinalp x -> ordinalp y ->
  cardinal (x *o y) = (cardinal x) *c (cardinal y).
Proof.
move => xo yo.
move: (ordinal_o_wor xo) => wox.
move: (ordinal_o_wor yo) => woy.
move: (ordinal_o_or x) => orx.
move: (ordinal_o_or y) => ory.
have pa: worder (order_prod2 (ordinal_o x) (ordinal_o y)) by fprops.
rewrite /ord_prod2 (cardinal_of_ordinal pa) (orprod2_sr orx ory).
rewrite (ordinal_o_sr x) (ordinal_o_sr y) cprod2_pr2a cprod2_pr2b 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.

Section InfiniteNormal.
Variable C: Set.
Hypothesis iC: infinite_c C.
Let E := (succ_c C).

Lemma succ_c_sum x y: inc x E -> inc y E -> inc (x +o y) E.
Proof.
move: iC => [cc _].
move=> /(succ_cP cc) [xo cx] /(succ_cP cc) [yo cy].
apply /(succ_cP cc);split; first by fprops.
rewrite osum_cardinal //.
move: (csum_Mlele cx cy); rewrite sum2_infinite1 //; apply /infinite_setP.
Qed.

Lemma succ_c_prod x y: inc x E -> inc y E -> inc (x *o y) E.
Proof.
move: iC => [cc _].
move=> /(succ_cP cc) [xo cx] /(succ_cP cc) [yo cy].
apply /(succ_cP cc);split; first by fprops.
rewrite oprod_cardinal //.
move: (cprod_Mlele cx cy); rewrite square_of_infinite //.
Qed.

Lemma succ_c_leomega x: x <=o omega0 -> inc x E.
Proof.
move: iC => [cc _].
move => [ox oo xo]; apply /(succ_cP cc); split => //.
have: cardinal x <=c cardinal Bnat by apply: sub_smaller.
rewrite cardinal_Bnat;move /infinite_c_P2: iC => pa pb; co_tac.
Qed.

Lemma succ_c_zero: inc \0o E.
Proof. apply: succ_c_leomega; apply: ozero_least; fprops. Qed.

Lemma succ_c_succ x: inc x E -> inc (succ_o x) E.
Proof.
move=> cx; move/(succ_cP (proj1 iC)):(cx) => [ox _].
rewrite - (ord_succ_pr ox); move: ord_lt_1omega => [h _].
by apply: succ_c_sum => //; apply:succ_c_leomega.
Qed.

Lemma succ_c_sup F: cardinal F <=c C -> sub F E -> inc (\osup F) E.
Proof.
move: (iC) => [cc _].
move => pa pb; apply/(succ_cP cc); split.
  by apply: OS_sup => t/pb /succ_cP [].
rewrite - setUb_identity.
move: (csum_pr1 (identity_g F)); rewrite identity_d /card_sumb;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 /succ_cP: (pb _ idf) => [].
move: (notbig_family_sum iC cdf etc) => ha hb; co_tac.
Qed.

End InfiniteNormal.

Lemma succ_c_pred c (E:= succ_c c):
  cardinalp c -> c = \csup (Zo E cardinalp).
Proof.
move => cc.
move: (proj1 cc) => oc.
have cse: (cardinal_set (Zo E cardinalp)) by move => t /Zo_P [].
have pa: inc c (Zo E cardinalp).
   apply /Zo_P; split=> //; apply /(succ_cP cc) => //.
   rewrite card_card //; split; fprops.
move: (card_sup_ub cse pa) => sa.
suff pb: union (Zo E cardinalp) <=c c by co_tac.
apply:(card_ub_sup cse (proj31 sa)).
move => x /Zo_P [ /(succ_cP cc) [ox h] cx].
by rewrite card_card in h.
Qed.

Lemma succ_c_pred_more E (c:= \csup (Zo E cardinalp)):
  (exists2 C, infinite_c C & E = succ_c C) ->
  infinite_c c /\ E = succ_c c.
Proof.
move => [C pa pb].
by move:(succ_c_pred (proj1 pa)); rewrite - pb -/c => <-.
Qed.

Definition aleph_one := succ_c omega0.

Definition countable_ordinal x := ordinalp x /\ cardinal x <=c cardinal Bnat.

Lemma aleph_oneP z: (inc z aleph_one <-> countable_ordinal z).
Proof.
rewrite /aleph_one - /Bnat - cardinal_Bnat;apply: (succ_cP); fprops.
Qed.

Lemma osum2_countable x y:
  countable_ordinal x -> countable_ordinal y -> countable_ordinal (x +o y).
Proof.
move: omega_infinitec aleph_oneP => h T.
by move => /T xa /T xn; apply /T;apply:succ_c_sum.
Qed.

Lemma oprod2_countable x y:
   countable_ordinal x -> countable_ordinal y -> countable_ordinal (x *o y).
Proof.
move: omega_infinitec aleph_oneP => h T.
by move => /T xa /T xn; apply /T;apply:succ_c_prod.
Qed.

Lemma countable_ordinal_sup E:
  countable_set E -> (alls E countable_ordinal)->
  countable_ordinal (\osup E).
Proof.
move: omega_infinitec aleph_oneP => h T.
move => /countableP; rewrite cardinal_Bnat => pa pb.
have se:sub E aleph_one by move => t /pb /T.
by move: (succ_c_sup h pa se) => /T.
Qed.

Lemma countable_leomega x:
  x <=o omega0 -> countable_ordinal x.
Proof.
move => [ox oo xo]; split => //; by apply: sub_smaller.
Qed.

Lemma countable_one: countable_ordinal \1o.
Proof. move: ord_lt_1omega => [o1 _]; by apply: countable_leomega. Qed.

Lemma countable_succ x:
   countable_ordinal x -> countable_ordinal (succ_o x).
Proof.
move=> cx; move: (cx) => [ox _]; rewrite - (ord_succ_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 // sum2_infinite1 // (card_card CS_omega).
exact:omega_infinitec.
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 => //.
  move => t /pb h; ord_tac.
move => t /pb h; ord_tac.
Qed.

Lemma ord_sup_ordinal a (b:= \osup a): ordinalp a ->
  a = b \/ a = succ_o b.
Proof.
move=> oa.
have [p1 _]:= (osuccVidpred oa).
case: p1; 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 <o (\osup X).
Proof.
by move=> 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; first by left.
have asu:= (ord_sup_ub alo aX).
have so: (ordinalp (union X)) by move: asu => [_ ? _].
right.
case: (limit_ordinal_pr2 so) => //.
  move=> h; rewrite h in nsX asu; case: nsX.
  rewrite - (ord_le0 asu) //.
case => // [y oy h].
have aiy: (forall i, inc i X -> i <=o y).
  move=> i iX; apply /ord_lt_succP.
  rewrite -h; apply: ord_sup_sub => //.
move: (ord_ub_sup alo oy aiy); rewrite h.
by move /ord_succ_ltP => [_ ?].
Qed.

Lemma ord_sup_M x y:
  sub x y -> ordinal_set y -> (\osup x) <=o (\osup y).
Proof.
move=> xy al1.
have al2: ordinal_set x by move=> z zx; apply: (al1 _ (xy _ zx)).
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 _ ab]; ord_tac.
have osy: ordinal_set y by move => a ay; move: (p4 _ ay) => [b _ ab]; ord_tac.
apply: ord_leA.
  apply: ord_ub_sup => //; first by apply: OS_sup.
  move=> i ix; move: (p3 _ ix) => [j jy lij].
  apply: (ord_leT lij);apply ord_sup_ub => //.
apply: ord_ub_sup => //; first by apply: OS_sup.
move=> i ix; move: (p4 _ ix) => [j jy lij].
apply: (ord_leT 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; suff : (fun_image X f = fun_image X g) by move ->.
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.
move:(h3 _ (h1 _ ay)) => ox; ord_tac.
Qed.

Lemma ord_lt_sup