Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset10.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Ordinals1.

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.

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.

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.