Require Import ssreflect ssrbool eqtype ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Export sset10.

Module Ordinals1.

Definition order_prod := lexicographic_order.
Definition order_prod_a := lexicographic_order_axioms.

Lemma order_prod_order: forall r g,
  order_prod_a r g -> order (order_prod r g).
Proof. move=> r g oa; apply lexorder_order => //. Qed.

Lemma order_prod_substrate: forall r g,
  order_prod_a r g ->
  substrate(order_prod r g) = prod_of_substrates g.
Proof. rewrite /order_prod_a/order_prod; move=> r g oa; bw. Qed.

Lemma prod_of_substrates_pr: forall i z g,
  inc i (domain g) -> inc z (prod_of_substrates g) ->
  inc (V i z) (substrate (V i g)).
Proof.
move=> i z g idg; rewrite /prod_of_substrates /fam_of_substrates; aw.
  bw; move=> [fgz [dz iVV]]; rewrite dz in iVV; move: (iVV _ idg); bw.
gprops.
Qed.

Lemma order_prod_gle: forall r g x x',
  order_prod_a r g ->
  gle (order_prod r g) x x' =
  (inc x (prod_of_substrates g) & inc x' (prod_of_substrates g) &
    (x= x' \/ exists j, inc j (substrate r) &
      glt (V j g) (V j x) (V j x') &
      forall i, glt r i j -> V i x = V i x')).
Proof.
move=> r g x x' la; rewrite /gle /order_prod lexorder_gle //.
have He: domain (fam_of_substrates g) = domain g.
  by rewrite /fam_of_substrates; bw.
have Hf: fgraph(fam_of_substrates g) by rewrite /fam_of_substrates; gprops.
apply iff_eq; move=> [xp [x'p aux]]; ee.
  set (s := (Zo (domain g) (fun i : Set => V i x <> V i x'))) in aux.
  have ssr: sub s (substrate r).
    by move: la => [_ [dg _]]; rewrite dg; apply Z_sub.
  case (emptyset_dichot s)=> nse.
    left; apply (productb_exten Hf xp x'p).
    move=> i idf; ex_middle h; empty_tac1 i.
    by rewrite /s; apply Z_inc; move: idf; rewrite /fam_of_substrates; bw.
    move: (la) => [[or wor] _]; move: (wor _ ssr nse)=> [j jle].
    move: (aux _ jle) => jp.
    move: jle => []; aw;move=> js jmin.
    have jsr: inc j (substrate r) by apply ssr.
    have dg: substrate r = domain g by move: la => [_ [res _]].
    right; ex_tac; ee; move=> i ij; ex_middle v.
    have iis : (inc i s) by rewrite /s; apply Z_inc =>//;rewrite -dg;order_tac.
    move: (iorder_gle1 (jmin _ iis)) => aux'; order_tac.
move: la => [wor [sr [fgg alo]]].
have Ha : order r by move: wor => [ok _].
set (s := (Zo (domain g) (fun i => V i x <> V i x'))).
have ssr: (sub s (substrate r)) by rewrite sr; apply Z_sub.
move=> j []; aw; move => js jmin.
move: js;rewrite /s Z_rw; move => [jdg Vj].
case aux => haux.
  rewrite haux in Vj;move: Vj; intuition.
move: haux => [i [isr [lti aeq]]].
have iis: inc i s by move:lti => [_ ok];rewrite /s; apply Z_inc =>//; ue.
move: (iorder_gle1 (jmin _ iis)) => ij.
case (equal_or_not j i) => ji; first by ue.
have ltji: glt r j i by split.
by elim Vj; apply aeq.
Qed.

Definition sum_of_substrates g := disjoint_union (fam_of_substrates g).

Lemma du_index_pr1: forall g x, inc x (sum_of_substrates g) ->
  (inc (Q x) (domain g) & inc (P x) (substrate (V (Q x) g)) & is_pair x).
Proof.
move=> g x; rewrite /sum_of_substrates /fam_of_substrates.
move=> xdu; move: (du_index_pr xdu); rewrite L_domain.
move=> [qd];bw; ee.
Qed.

Lemma inc_disjoint_union1: forall g x y,
  inc y (domain g) -> inc x (substrate (V y g)) ->
  inc (J x y) (sum_of_substrates g).
Proof.
move=> g x y ydg xsv; rewrite /sum_of_substrates/fam_of_substrates.
apply inc_disjoint_union; bw.
Qed.

Definition order_sum_a r g:=
  order r & substrate r = domain g & fgraph g &
  (forall i, inc i (domain g) -> order (V i g)).

Definition order_sum_r r g x x' :=
    (glt r (Q x) (Q x') \/ (Q x = Q x' & gle (V (Q x) g) (P x) (P x'))).

Definition order_sum r g :=
  graph_on (order_sum_r r g) (sum_of_substrates g).

Lemma order_sum_order: forall r g,
  order_sum_a r g -> order (order_sum r g).
Proof.
move=> r g [or [sr [fgg alo]]].
rewrite /order_sum.
set (s := order_sum_r r g).
set (x:= sum_of_substrates g).
have ->: (graph_on s x = graph_on (fun a b => inc a x & inc b x & s a b) x).
  rewrite /graph_on; set_extens t; rewrite Z_rw Z_rw; last by intuition.
  aw;move=> [tp sp]; ee.
apply order_from_rel;red; ee.
      rewrite /s /order_sum_r;move=> u v w [ux [vx suv]] [_ [xw suw]]; ee.
      case suv; case suw.
            left; order_tac.
          move=> [sq leq]; rewrite sq; intuition.
        move=> h [sq leq]; rewrite sq; intuition.
      move=> [sq1 le1][sq2 le2]; right; split; first by ue.
     move: (du_index_pr1 ux) => [qdg _].
     rewrite -sq2 in le1; move: (alo _ qdg)=> ov; order_tac.
   rewrite /s /order_sum_r;move=> u v [ux [vx suv]] [_ [_ svu]]; ee.
   move: (du_index_pr1 ux) => [qudg [puv pu]].
   move: (du_index_pr1 vx) => [qvdg [pvv pv]].
   case suv; case svu.
        move=> lt1 lt2; order_tac.
      move => [eq _] [_ lt1]; elim lt1; intuition.
    move => [_ lt1] [eq _]; elim lt1; intuition.
  move=> [eq le1][_ le2]; rewrite eq in le1; move: (alo _ qudg) => ou.
  apply pair_exten =>//;order_tac.
rewrite /s /order_sum_r; move=> u v [ux [vx suv]].
move: (du_index_pr1 ux) => [qudg [puv pu]].
move: (du_index_pr1 vx) => [qvdg [pvv pv]].
ee; right; ee.
  move: (alo _ qudg) => ou; order_tac.
move: (alo _ qvdg) => ou; order_tac.
Qed.

Lemma order_sum_substrate: forall r g, order_sum_a r g ->
  substrate(order_sum r g) = (sum_of_substrates g).
Proof.
move=> r g oa; rewrite /order_sum substrate_graph_on //.
move => a asg;rewrite /order_sum_r.
move: (du_index_pr1 asg) => [qudg [puv pu]].
right; ee.
move: oa =>[_[_[_ alo]]]; move: (alo _ qudg) => ou; order_tac.
Qed.

Lemma order_sum_gle: forall r g , order_sum_a r g ->
  forall x x', gle (order_sum r g) x x' =
  (inc x (sum_of_substrates g) & inc x' (sum_of_substrates g) &
    order_sum_r r g x x').
Proof. move=> r g oa x x'; rewrite /gle/order_sum graph_on_rw1 //. Qed.

Hint Resolve order_sum_order order_prod_order: fprops.

Lemma order_sum_gle1: forall r g x x',
  order_sum_a r g -> gle (order_sum r g) x x' ->
  (glt r (Q x) (Q x') \/ (Q x = Q x' & gle (V (Q x) g) (P x) (P x'))).
Proof. move=> r g x x' oa; rewrite order_sum_gle; ee. Qed.

Lemma order_sum_gle2: forall r g a b a' b',
  order_sum_a r g -> gle (order_sum r g) (J a b)(J a' b') ->
  (glt r b b' \/ (b = b' & gle (V b g) a a')).
Proof. move=> r g a b a' b' h1 h2; move:(order_sum_gle1 h1 h2); aw. Qed.

Lemma order_sum_gle_id: forall r g x x', order_sum_a r g ->
  gle (order_sum r g) x x' -> gle r (Q x) (Q x').
Proof.
move=> r g x x' oa; rewrite order_sum_gle//; move=> [_ [xs h]]; case h.
  by move=>[ok _].
move=> [eq _]; rewrite eq.
move: (du_index_pr1 xs)=> [qd _].
move: oa => [or [srdg _]]; order_tac; ue.
Qed.

Hint Rewrite order_sum_substrate order_prod_substrate : bw.

Definition order_prod2 r r' :=
  order_prod canonical_doubleton_order (variantLc r' r).

Definition order_sum2 r r' :=
  order_sum canonical_doubleton_order (variantLc r r').

Lemma order_sum2_axioms: forall r r', order r -> order r' ->
  order_sum_a canonical_doubleton_order (variantLc r r').
Proof.
move=> r r' or or'; red; ee.
by move: worder_canonical_doubleton_order => [ord _].
rewrite substrate_canonical_doubleton_order; bw.
bw; move=> i itp; try_lvariant itp.
Qed.

Lemma order_prod2_axioms: forall r r', order r -> order r' ->
  order_prod_a canonical_doubleton_order (variantLc r' r).
Proof.
move=> r r' or or'; red; red;ee.
by apply worder_canonical_doubleton_order.
rewrite substrate_canonical_doubleton_order; bw.
bw; move=> i itp; try_lvariant itp.
Qed.

Lemma order_sum2_order: forall r r', order r -> order r' ->
  order (order_sum2 r r').
Proof.
move=> r r' or or'; apply order_sum_order; apply order_sum2_axioms =>//.
Qed.

Lemma order_prod2_order: forall r r', order r -> order r' ->
  order (order_prod2 r r').
Proof.
move=> r r' or or'; apply lexorder_order; apply order_prod2_axioms =>//.
Qed.

Hint Resolve order_sum2_order order_prod2_order: fprops.

Lemma canonical2_substrate: forall r r',
  fam_of_substrates (variantLc r r') = variantLc (substrate r) (substrate r').
Proof.
move=> r r'; rewrite /fam_of_substrates /variantLc.
 apply fgraph_exten; gprops; fprops; bw.
move=> x xtp; try_lvariant xtp; fprops.
Qed.

Definition canonical_du2 a b :=
  disjoint_union (variantLc a b).

Lemma canonical_du2_rw: forall a b,
  canonical_du2 a b =
  union2 (product a (singleton TPa)) (product b (singleton TPb)).
Proof. by move=> a b ; rewrite /canonical_du2 disjoint_union2_rw1. Qed.

Lemma canonical_du2_pr: forall a b x,
  inc x (canonical_du2 a b) = (is_pair x &
  ((inc (P x) a & Q x = TPa) \/ (inc (P x) b & Q x = TPb))).
Proof.
move=> a b x; rewrite canonical_du2_rw; apply iff_eq; aw; intuition.
Qed.

Lemma canonical_du2_pr1: forall a b x,
  inc x (canonical_du2 a b) ->
  ((inc (P x) a & Q x = TPa) \/ (inc (P x) b & Q x = TPb)).
Proof.
by move=> a b x; rewrite canonical_du2_pr; move=> [_].
Qed.

Lemma canonical_du2_pr2: forall a b x,
  inc x (canonical_du2 a b) -> (Q x = TPa \/ Q x = TPb).
Proof.
by move=> a b x xc; case (canonical_du2_pr1 xc); move=> [_]; auto.
Qed.

Lemma canonical_du2_pra: forall a b x,
  inc x a -> inc (J x TPa) (canonical_du2 a b).
Proof. move=> a b x xa; rewrite canonical_du2_pr; ee; left; aw;ee. Qed.

Lemma canonical_du2_prb: forall a b x,
  inc x b -> inc (J x TPb) (canonical_du2 a b).
Proof. move=> a b x xa; rewrite canonical_du2_pr; ee; right; aw;ee. Qed.

Lemma order_sum2_substrate: forall r r', order r -> order r' ->
  substrate (order_sum2 r r') = canonical_du2 (substrate r) (substrate r').
Proof.
move=> r r' or or'; rewrite /canonical_du2 /order_sum2 order_sum_substrate.
  rewrite / sum_of_substrates canonical2_substrate //.
apply (order_sum2_axioms or or').
Qed.

Lemma order_prod2_substrate: forall r r',
  order r -> order r' ->
  substrate (order_prod2 r r') = product2 (substrate r') (substrate r).
Proof.
move=> r r' or or'; rewrite /order_prod2 lexorder_substrate.
 rewrite /prod_of_substrates canonical2_substrate /product2 /productf.
  rewrite /variantLc /variantL two_points_pr2 //.
apply order_prod2_axioms =>//.
Qed.

Lemma order_sum2_gle: forall r r' x x', order r -> order r' ->
  gle (order_sum2 r r') x x' =
  (inc x (canonical_du2 (substrate r) (substrate r')) &
    inc x' (canonical_du2 (substrate r) (substrate r')) &
    ((Q x = TPa & Q x' = TPa & gle r (P x) (P x'))
      \/ (Q x <> TPa & Q x' <> TPa & gle r' (P x) (P x'))
      \/ (Q x = TPa & Q x' <> TPa))).
Proof.
move=> r r' x x' or or'.
have Ha: TPb <> TPa by fprops.
have oa: order_sum_a canonical_doubleton_order (variantLc r r').
  by apply order_sum2_axioms.
set S1:= (canonical_du2 (substrate r) (substrate r')).
have S1p: S1 = (sum_of_substrates (variantLc r r')).
  by rewrite /sum_of_substrates canonical2_substrate.
rewrite /order_sum2; apply iff_eq; rewrite (order_sum_gle oa); rewrite -S1p.
  move=> [xs [xs' osr]]; ee.
  move: osr; rewrite /order_sum_r /glt {1} /gle canonical_doubleton_order_pr.
  case.
    move=> [aux nsQ]; case aux.
      by move=> [e1 e2]; rewrite e1 e2 in nsQ; elim nsQ.
    case; first by move=> [e1 e2]; rewrite e1 e2 in nsQ; elim nsQ.
    move=> [e1 e2]; right; right; rewrite e2; ee.
  move=> [sq].
  case (canonical_du2_pr2 xs) =>Qx; rewrite -sq Qx; bw; [left| right;left]; ee.
move=> [xs1 [x's1 etc]]; ee.
red; rewrite /glt/gle canonical_doubleton_order_pr.
case etc.
  move=> [qxa [qx'a lrxx']]; rewrite qxa qx'a; bw;right;ee.
case.
  move=> [qxa [qx'a lrxx']].
  have ->: (Q x' = TPb) by case (canonical_du2_pr2 x's1) => //.
  have ->: (Q x = TPb) by case (canonical_du2_pr2 xs1) => //.
  right; bw; ee.
move=> [qxa qx'a]; rewrite qxa.
have ->: (Q x' = TPb) by case (canonical_du2_pr2 x's1) => //.
intuition.
Qed.

Lemma order_sum2_gle_spec: forall r r' x x', order r -> order r' ->
  inc x (substrate r) -> inc x' (substrate r') ->
  glt (order_sum2 r r') (J x TPa) (J x' TPb).
Proof.
move=> r r' x x' or or' xsr xsr'.
rewrite /glt (order_sum2_gle _ _ or or').
split.
  split; first by apply canonical_du2_pra.
  split; first by apply canonical_du2_prb.
  right; right. aw. ee.
by move => h; move: (pr2_def h); apply two_points_distinct.
Qed.

Lemma order_prod2_gle: forall r r' a b,
  order r -> order r' ->
  gle (order_prod2 r r') a b =
  (inc a (product2 (substrate r') (substrate r))
    & inc b (product2 (substrate r') (substrate r))
    & ( (V TPa a = V TPa b & gle r (V TPb a) (V TPb b))
      \/ (glt r' (V TPa a)(V TPa b)))).
Proof.
move=> r r' a b or or'.
rewrite /order_prod2.
move: (order_prod2_axioms or or') => la.
rewrite order_prod_gle // substrate_canonical_doubleton_order.
have -> :prod_of_substrates (variantLc r' r) =
    (product2 (substrate r') (substrate r)).
  rewrite -order_prod2_substrate // /order_prod2; bw.
apply iff_eq; move => [ap2 [bp2 h]]; ee.
  case h.
     move => <-; left;ee; order_tac.
     by move: ap2; rewrite product2_rw; move => [_ [_ [_]]].
  move=> [j []]; rewrite two_points_rw; case => h'; rewrite h'; bw.
    intuition.
  move=> [p1 p2].
  have p3: (glt canonical_doubleton_order TPa TPb).
    split; [ rewrite /gle canonical_doubleton_order_pr; auto | fprops].
  move: (p2 _ p3) => p4; move: p1 => [p1 _]; auto.
case h.
  move=> [p1 p2]; case (equal_or_not (V TPb a) (V TPb b)).
    move:ap2 bp2; rewrite ! product2_rw.
    move => [fga [da [Vaa VBa]]][fgb [db [Vab VBb]]].
    move=> VV; left; apply fgraph_exten =>//; first by ue.
    rewrite da; move=> ix xda;try_lvariant xda.
  move => nVV; right; exists TPb; ee; bw; first by split.
  move=> i; rewrite /glt/gle canonical_doubleton_order_pr.
  move=> [p3 p4]; case p3.
     by move=> [r1 r2]; rewrite -r2 in r1; contradiction.
  case; first by move=> [r1 _]; contradiction.
  by move=> [ia _]; rewrite ia.
move=> [_ ne];right; exists TPa; bw;ee.
move=> i; rewrite /glt/gle canonical_doubleton_order_pr.
move=> [aux ineA]; case aux.
   move=> [p _]; contradiction.
case; by move=> [_ p]; elim two_points_distinct.
Qed.

Lemma order_sum_worder : forall r g,
  worder r -> substrate r = domain g -> fgraph g ->
  (forall i, inc i (domain g) -> worder (V i g)) ->
  worder (order_sum r g).
Proof.
move=> r g [or wor] sr fg alw.
have oa: order_sum_a r g by red;ee.
split; first by apply order_sum_order.
move=> x; bw => xs [x0 x0x].
set (A := fun_image x Q).
have Asr: (sub A (substrate r)).
  move=> t; rewrite /A; aw; move=> [z [zx]] <-.
  rewrite sr;move: (du_index_pr1 (xs _ zx)); intuition.
have neA: nonempty A by exists (Q x0); rewrite /A; aw; ex_tac.
move: (wor _ Asr neA)=> [a []]; aw; move=> aA ale.
set (B:= Zo x (fun z => Q z = a)).
set (C := fun_image B P).
move: (Asr _ aA); rewrite sr => adg.
have Cs: (sub C (substrate (V a g))).
  move=> t; rewrite /C; aw; move=> [z [zB]] <-.
  move: zB; rewrite /B Z_rw; move => [zx] <-.
  by move: (du_index_pr1 (xs _ zx)) => [_ [ok _]].
have neC: nonempty C.
  move: aA; rewrite /A; aw; move=> [z [zx qz]].
  exists (P z); rewrite /C; aw; exists z; ee; rewrite /B; apply Z_inc =>//.
move: (alw _ adg)=> [or' wor']; move: (wor' _ Cs neC) => [b []].
rewrite (substrate_induced_order or' Cs).
move=> bC leB.
have Jx: inc (J b a) x.
   move: bC; rewrite /C; aw; move=> [z [zB]] <-.
   move: zB; rewrite /B Z_rw; move=> [zx] <-; aw.
   by move: (du_index_pr1 (xs _ zx)) => [_ [_]] ->.
have ors: order (order_sum r g) by apply order_sum_order.
have xso: sub x (substrate (order_sum r g)) by bw.
exists (J b a); red; rewrite (substrate_induced_order ors xso).
split; first (by exact); move=> c cx.
move: (du_index_pr1 (xs _ cx))=> [Qc [Pc pc]].
rewrite (iorder_gle _ Jx cx) (order_sum_gle oa); ee.
red; rewrite pr1_pair pr2_pair.
have QcA: (inc (Q c) A) by rewrite /A;aw; ex_tac.
move: (ale _ QcA); aw => leac.
case (equal_or_not a (Q c)).
  move=> aQc; right;ee.
  have Pcb: (inc (P c) C).
     rewrite /C; aw; exists c; ee ; rewrite /B; apply Z_inc =>//.
  move: (leB _ Pcb); aw.
by move => nac; left; split.
Qed.

Lemma order_prod_worder: forall r g,
  worder r -> substrate r = domain g -> fgraph g ->
  (forall i, inc i (domain g) -> worder (V i g)) ->
  finite_set (substrate r) ->
  worder (order_prod r g).
Proof.
move=> r g wor sr fg alw fs.
have lea:order_prod_a r g by red; red;ee.
set n := cardinal (substrate r).
have: cardinal (substrate r) = n by [].
move: lea alw.
generalize r g.
have: inc n Bnat by move: fs; rewrite /finite_set inc_Bnat.
generalize n.
clear n fs wor sr fg r g.
apply: cardinal_c_induction.
  move=> r g lea alw cr.
  have lo: order (order_prod r g) by fprops.
  move: (cardinal_nonemptyset cr) => se; split; first by fprops.
  move=> x xsr; move: (xsr).
  bw; rewrite /prod_of_substrates /fam_of_substrates.
  move: lea => [wor [sr [fgg alo]]].
  rewrite -sr se product2_trivial.
  move=> sxs nex; exists emptyset; red; aw.
  move: nex=> [w wx]; move: (sxs _ wx); aw; move=> h; rewrite h in wx.
  ee; move=> t tx; rewrite iorder_gle =>//.
  have ->: t = emptyset by move: (sxs _ tx); aw.
  by order_tac; apply xsr.
move=> n nB hrec r g lea alwo csr.
have lo: (order (order_prod r g)) by fprops.
split =>//.
move: (lea) => [[or wor] [sr [fgg alo]]].
have [i [isr ilsr]]: exists i,
   inc i (domain g) & forall j, inc j (substrate r) -> gle r i j.
  case (emptyset_dichot (substrate r)).
    move=> se; rewrite se cardinal_emptyset in csr.
    symmetry in csr; elim (succ_nonzero csr).
  move=> nsr.
  move: (wor _ (@sub_refl (substrate r)) nsr) => [y []]; aw; last by fprops.
  rewrite -sr; move=> ysr aux; exists y; ee; move=> j jsr.
  apply (iorder_gle1 (aux _ jsr)).
bw.
move => x xsr [x0 x0x].
set (Y := fun_image x (fun z => V i z)).
have sYs: (sub Y (substrate (V i g))).
  move=> t; rewrite /Y; aw; move=> [z [zx]] <-.
  by move: (xsr _ zx); apply prod_of_substrates_pr.
have neY: (nonempty Y) by exists (V i x0); rewrite /Y; aw; ex_tac.
move: (alwo _ isr) => [or' wor']; move: (wor' _ sYs neY) => [z []]; aw.
clear wor wor'.
move => zY zl.
set (X1 := Zo x (fun t => V i t = 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.
    rewrite order_prod_gle =>//; ee.
    right; exists i; ee; first by ue.
      move: aX1; rewrite /X1 Z_rw; move=> [_ eq1]; rewrite eq1.
      have ib: z <> V i b.
        by move=> eq2; move: bX1; rewrite /X1 Z_rw; apply; ee.
      split =>//.
      have vbY: (inc (V i b) Y)by rewrite /Y; aw; exists b; auto.
      apply (iorder_gle1 (zl _ vbY)).
    move=> j rj.
    have jsr: (inc j (substrate r)) by order_tac.
    move: (ilsr _ jsr) => le2; order_tac.
  by dneg ab; rewrite -ab.
set (I1:= complement (substrate r) (singleton i)).
set (r1 := induced_order r I1).
set (g1 := restr g I1).
have I1sr: (sub I1 (substrate r)) by rewrite /I1; apply sub_complement.
have dg1: domain g1 = I1 by rewrite /g1 restr_domain1 //; ue.
have sdg1g: sub (domain g1) (domain g) by rewrite dg1; ue.
have la1: order_prod_a r1 g1.
  red; red;ee.
        move: lea => [WO _]; rewrite /r1; apply worder_restriction => //.
      symmetry; rewrite /r1; aw.
    rewrite /g1; fprops.
  move=> j j1; move: (alo _ (sdg1g _ j1)) => og1.
   rewrite /g1 restr_ev //; ue.
have alw: (forall i, inc i (domain g1) -> worder (V i g1)).
  move=> j jdg; rewrite /g1 restr_ev; [by apply alwo;apply sdg1g|exact| ue| ue].
have cs: (cardinal (substrate r1) = n).
  rewrite /r1; aw; move: (cardinal_succ_pr1 (substrate r) i).
  rewrite -sr in isr.
  rewrite -tack_on_complement // -/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; rewrite /X2; aw; last (by gprops); move=> [u [uX1]] <-.
  have ux: (inc u x) by move: uX1; rewrite /X1 Z_rw; move=> [ok _].
  move: (xsr _ ux).
  rewrite /prod_of_substrates /fam_of_substrates; aw; bw; last by gprops.
  move=> [fgfu [du iVV]].
  have aa: sub I1 (domain u) by rewrite du -sr.
  have ->: domain (restr u I1) = I1 by rewrite restr_domain1 //.
  ee; move=> j jI1; bw; last by ue.
  move: (iVV _ (aa _ jI1)); bw; [ rewrite /g1 restr_ev //; ue | ue].
have neX2: (nonempty X2).
  move: zY; rewrite /Y; aw; move => [z0 [z0x pz0]]; exists (restr z0 I1).
  rewrite /X2; aw; exists z0; ee; rewrite /X1; apply Z_inc =>//.
move: (wo1 _ X2s neX2)=> [w []]; aw; move=> wX2 wle.
move: wX2; rewrite /X2; aw; move=> [v [vX1 rv]].
have vx: inc v x by move: vX1; rewrite /X1 Z_rw; intuition.
have sxs: sub x (substrate (order_prod r g)) by bw.
exists v; red; aw; split =>//.
move=> u ux1.
rewrite iorder_gle //.
case (equal_or_not (V i u) z)=> Vu; last first.
  have nv: (~ inc u X1) by rewrite /X1 Z_rw; dneg ww; intuition.
  by move: (p1 _ _ vx ux1 vX1 nv)=> [le _].
have uX1: (inc u X1) by rewrite /X1; apply Z_inc.
have rX2: (inc (restr u I1) X2) by rewrite /X2; aw; ex_tac.
move: (iorder_gle1 (wle _ rX2)).
rewrite /gle lexorder_gle // lexorder_gle //.
set T:= Zo _ _.
have aa:sub (Zo (domain g) (fun i0 : Set => V i0 v <> V i0 u)) (substrate r).
  by rewrite sr; apply Z_sub.
move=> [wp [rp op]]; ee; move=> j []; rewrite (substrate_induced_order or aa).
rewrite Z_rw; move=> [jd nsv] aux.
have jI1: inc j I1.
  rewrite /I1; srw; split; first (by ue); aw; dneg ij; rewrite ij Vu.
  move:vX1; rewrite /X1 Z_rw; intuition.
have aux1: product_order_axioms g by red; ee.
move: (xsr _ vx) (xsr _ ux1).
rewrite ! (prod_of_substrates_rw _ aux1); move=> [fgv [dv vp]][fgu [du up]].
have jT: inc j T.
   rewrite /T; apply Z_inc; first by ue.
   rewrite -rv ! restr_ev //; [ by rewrite du -sr | by rewrite dv -sr].
have lej: (least_element (induced_order r1 T) j).
  have or1': order r1 by rewrite /r1; fprops.
  have sT: sub T (substrate r1) by rewrite /T /r1; aw;rewrite -dg1; apply Z_sub.
  red; aw; split =>//.
  move=> x1 aux2; rewrite (iorder_gle _ jT aux2).
  move: aux2; rewrite Z_rw dg1; move=> [xdg1].
  rewrite -rv ! restr_ev =>//; try (rewrite ? du ? dv -sr; apply I1sr).
  move=> VV.
  have aux3: (inc x1 (Zo (domain g) (fun i : Set => V i v <> V i u))).
    by apply Z_inc =>//;rewrite -sr; apply I1sr.
  move: (iorder_gle1 (aux _ aux3)).
  rewrite /r1 (iorder_gle _ jI1 xdg1) //.
move: (op _ lej).
rewrite -rv ! restr_ev =>//; try (rewrite ? du ? dv -sr; apply I1sr).
Qed.

Lemma order_prod2_worder: forall r r',
  worder r -> worder r' -> worder (order_prod2 r r').
Proof.
move=> r r' wor wor'; rewrite/ order_prod2; apply order_prod_worder.
- apply worder_canonical_doubleton_order.
- rewrite substrate_canonical_doubleton_order; bw.
- fprops.
- bw; move=> i ind; try_lvariant ind.
- rewrite substrate_canonical_doubleton_order -two_points_pr2.
  apply doubleton_finite.
Qed.

Lemma order_sum2_worder: forall r r',
  worder r -> worder r' -> worder (order_sum2 r r').
Proof.
move=> r r' wor wor'; apply order_sum_worder.
- apply worder_canonical_doubleton_order.
- rewrite substrate_canonical_doubleton_order; bw.
- fprops.
- bw; move=> i ind; try_lvariant ind.
Qed.

Lemma order_sum2_totalorder: forall r r',
  total_order r -> total_order r' -> total_order (order_sum2 r r').
Proof.
move=> r r' [or tor][or' tor'].
split; first by fprops.
rewrite order_sum2_substrate// /gge.
move=> x y xc yc.
move: (xc)(yc); rewrite ! canonical_du2_pr; move=> [px p1][py p2].
rewrite ! (order_sum2_gle _ _ or or').
have ba: TPb <> TPa by fprops.
case p1; case p2; move=> [Py Qy][Px Qx]; rewrite Qx Qy.
      case (tor _ _ Px Py); [ left | rewrite /gge; right]; eee; left; ee.
    left; split; eee; right;right; ee.
  right; split; eee; right;right; ee.
case (tor' _ _ Px Py); [ left | rewrite /gge; right]; eee; right; left; eee.
Qed.

Lemma order_prod_pr: forall r r',
  order r -> order r' ->
 (order_prod2 r r') \Is (order_sum r' (cst_graph (substrate r') r)).
Proof.
move=>r r' or or'.
have oa: (order_sum_a r' (cst_graph (substrate r') r)).
  red; rewrite /cst_graph; ee; bw; move=> i isr; bw.
set (fo:=order_sum r' (cst_graph (substrate r') r)).
have odf: order fo by rewrite /fo; apply order_sum_order.
move: (order_sum_substrate oa) => s1.
move: (order_prod2_order or odf).
move: (order_prod2_substrate or or').
set (io := order_prod2 r r'); move => s2 o2.
set (f := fun x => J (V TPb x) (V TPa x)).
have ta: (transf_axioms f (substrate io) (substrate fo)).
  move=> t; rewrite /fo s1 s2 /sum_of_substrates /fam_of_substrates /cst_graph.
  rewrite product2_rw /f; move=> [fgt [dt [va vb]]].
  apply inc_disjoint_union; bw.
have bf: bijection (BL f (substrate io) (substrate fo)).
  apply bl_bijective =>//.
    move=> u v;rewrite s2 /f; move=> ud vd eq.
    move: (pr2_def eq)(pr1_def eq) => p1 p2.
    apply (productf_exten ud vd); move=> i itp; try_lvariant itp.
  rewrite s1 /fam_of_substrates /cst_graph.
  move=> y ys; move:(du_index_pr1 ys); rewrite L_domain.
  move=> [Qsr]; bw; move=> [Psr py].
  exists (variantLc (Q y) (P y)); split.
    rewrite s2 product2_rw; ee; bw.
  rewrite /f; bw; aw.
exists (BL f (substrate io) (substrate fo));red; ee; [ | aw | aw | aw].
  rewrite /io; apply order_prod2_order =>//.
move=> x y xs ys; rewrite /io order_prod2_gle // -s2.
have p1: inc (V TPa x) (substrate r').
    move: xs; rewrite s2 product2_rw; intuition.
rewrite bl_W // bl_W// /fo order_sum_gle // /order_sum_r.
apply iff_eq.
  have ->: sum_of_substrates (cst_graph (substrate r') r) = substrate fo by aw.
  move=> [xp [yp aux]]. ee;rewrite /f /cst_graph; bw; aw; case aux;auto.
move=> [xp [yp aux]]; eee;move: aux.
rewrite/f /cst_graph; aw; bw; case; auto.
Qed.

Lemma ordinal_p8: forall r r', worder r -> worder r' ->
  r \Is r' -> ordinal r = ordinal r'.
Proof.
move=> r r' w1 w2 or.
move: (ordinal_p1 w1)(ordinal_p1 w2) => o1 o2.
move: (ordinal_p2 w1)(ordinal_p2 w2) => i1 i2.
apply (ordinal_p4 o1 o2 (orderIT (orderIT (orderIS i1) or) i2)).
Qed.

Lemma ordinal_p9: forall r E, worder r -> is_ordinal E ->
  r \Is (ordinal_o E) -> ordinal r = E.
Proof.
move=> r E wo bo oi.
by rewrite (ordinal_p8 wo (ordinal_worder2 bo) oi) (ordinal_p3 bo).
Qed.

Lemma ordinal_p10: forall x, is_ordinal x -> worder (ordinal_o x).
Proof. exact ordinal_worder2. Qed.

Lemma ordinal_p11: forall x, is_ordinal x -> order (ordinal_o x).
Proof. by move=> x xB; apply worder_is_order; apply ordinal_p10. Qed.

Lemma worder_invariance: forall r r',
  r \Is r' -> worder r -> worder r'.
Proof.
move=> r r' [f [or [or' [bf [sf [tf sif]]]]]] [_ wor].
split =>//.
move=> x xsr [y yx].
set (A := image_by_fun (inverse_fun f) x).
move: (inverse_bij_is_bij bf) => bif.
have fi: is_function (inverse_fun f) by fct_tac.
have sxt: (sub x (target f)) by rewrite -tf.
have sxs: (sub x (source (inverse_fun f))) by aw.
have sx :source f = (target (inverse_fun f)) by aw.
have Asx: sub A (substrate r).
  rewrite /A sf; move=> t; aw; move=> [u [ux]] <-.
  by rewrite sx;apply inc_W_target =>//; apply sxs.
have neA: (nonempty A) .
  by exists (W y (inverse_fun f)); rewrite /A; aw; ex_tac.
move: (wor _ Asx neA) => [z []]; aw.
move=> zA zle; move: (zA).
rewrite /A; aw; move=> [u [ux Wu]].
have utx: (inc u (target f)) by apply sxt.
symmetry in Wu; move: (W_inverse bf utx Wu) => uW.
exists u; red; aw; split =>//.
move=> v vx; aw.
set v':= W v (inverse_fun f).
have vt: (inc v (target f)) by apply sxt.
move: (W_inverse bf vt (refl_equal v')).
rewrite uW; move=> ->.
have vA: inc v' A by rewrite /A; aw; ex_tac.
 move: (iorder_gle1 (zle _ vA)).
by rewrite sif //; rewrite -sf; apply Asx.
Qed.

Lemma ordinal_pr51: forall x, is_ordinal x -> order (ordinal_o x).
Proof. by move=> t or; move: (ordinal_p10 or) => [res _]. Qed.

Lemma ordinal_pr52: forall x, is_ordinal x -> total_order (ordinal_o x).
Proof. by move=> t or; apply (worder_total (ordinal_p10 or)). Qed.

Lemma order_le_reflexive: forall x, order x -> order_le x x.
Proof.
move=> x ox; red; ee; exists (identity (substrate x)); exists (substrate x).
split; first by fprops.
red; aw;ee; first by apply identity_bijective.
move=> z y xsr ysr; rewrite ! identity_W //; aw.
Qed.

Lemma set_ord_le_prop: forall a x, is_ordinal a ->
  inc x (succ_o a) = x <=o a.
Proof.
move=> a x oa;rewrite ordinal_le_pr0.
apply iff_eq.
  move=> xo; ee.
    apply (elt_of_ordinal (ordinal_succ oa) xo).
  apply (ordinal_sub3 oa xo).
by move=> [ox [_ s]]; rewrite - (ordinal_sub4 ox oa).
Qed.

Lemma set_ord_lt_prop: forall a x, is_ordinal a ->
  inc x a = x <o a.
Proof.
move=> a x oa;rewrite ordinal_lt_pr0.
apply iff_eq; last by intuition.
move=> xa;ee; ord_tac.
Qed.

Lemma set_ord_lt_prop3: forall a, is_ordinal a ->
  ordinal (graph_on ordinal_le a) = a.
Proof.
move=> a oa.
have [p1 p2]: (substrate (graph_on ordinal_le a) = a &
  worder (graph_on ordinal_le a)).
  apply wordering_pr; first by apply wordering_ordinal_le.
  move=> b bx; apply (ordinal_le_reflexive (elt_of_ordinal oa bx)).
have o1: order (graph_on ordinal_le a) by fprops.
have -> : graph_on ordinal_le a = ordinal_o a.
  rewrite graph_exten ; try apply order_is_graph; fprops.
  move=> u v.
  rewrite graph_on_rw1 ordinal_le_pr0; aw.
  apply iff_eq; first by intuition.
  by move=> [ua [va uv]]; ee; apply (elt_of_ordinal oa).
apply (ordinal_p3 oa).
Qed.

Lemma finite_ordinal1: forall n, inc n Bnat ->
   n = ordinal (interval_Bnatco n).
Proof.
move=> n nB.
have cn: is_cardinal n by fprops.
have ox: is_ordinal n by apply cardinal_ordinal.
have cnn: cardinal n = n by apply cardinal_of_cardinal.
have fs: finite_set n by red; rewrite cnn -inc_Bnat.
move: (interval_Bnatco_worder nB) => w1.
move: (ordinal_p1 w1) => on.
apply (ordinal_p4 ox on).
move: (worder_total (ordinal_p10 ox)) => p1.
move: (worder_total (ordinal_p10 on)) => p2.
have p3: equipotent (substrate (ordinal_o n))
    (substrate (ordinal_o (ordinal (interval_Bnatco n)))).
  eqtrans (substrate (interval_Bnatco n)).
    rewrite - cardinal_equipotent interval_Bnatco_substrate //.
    rewrite cardinal_interval_co_0a1 // (ordinal_p7 ox) //.
  move: (ordinal_p2 w1) => [f [_ [_ [bf [sf [tf p]]]]]].
  rewrite sf tf; exists f; ee.
have fs1: finite_set (substrate (ordinal_o n)) by rewrite (ordinal_p7 ox).
move: (isomorphism_worder_finite p1 p2 fs1 p3) => [[f fiso] _].
exists f; ee.
Qed.

Lemma finite_ordinal2: forall n, inc n Bnat ->
   n = interval_co_0a n.
Proof.
move=> n nB.
have cn: is_cardinal n by fprops.
move: (cardinal_ordinal cn) => on.
set_extens t; rewrite (interval_co_0a_pr2 _ nB) /cardinal_lt /cardinal_le.
  move => tn; split.
    have fn: finite_o n by move: nB; rewrite inc_Bnat.
    move: (finite_o_increasing tn fn) => [ot ft].
    move: (ordinal_transitive on tn) => stn.
    ee; apply finite_cardinal_pr1; red; ee.
  by move => nt; rewrite nt in tn; elim (ordinal_decent on tn).
move => [[ct [_ tn]] nt].
apply (on _ tn (ordinal_transitive (cardinal_ordinal ct)) nt).
Qed.

Definition ord_zero := card_zero.
Definition ord_one := card_one.
Definition ord_two := card_two.
Definition ord_omega := omega0.

Notation "0 'o'" := ord_zero.
Notation "1 'o'" := ord_one.
Notation "2 'o'" := ord_two.
Notation "\omega" := ord_omega.

Lemma ordinal_0: is_ordinal 0o.
Proof. apply ordinal_zero. Qed.

Lemma ordinal_1: is_ordinal 1o.
Proof. apply ordinal_one. Qed.

Lemma ordinal_2: is_ordinal 2o.
Proof. apply ordinal_two. Qed.

Lemma ordinal_omega: is_ordinal \omega.
Proof. apply omega0_ordinal. Qed.

Lemma ord_omega_pr: \omega = ordinal Bnat_order.
Proof.
move: Bnat_order_worder => bwo.
have <-: (ordinal_o \omega = Bnat_order).
  rewrite graph_exten; try apply order_is_graph; fprops.
  move=> u v;rewrite -[related]/gle.
  rewrite Bnat_order_le /Bnat_le /cardinal_le; aw; apply iff_eq.
    move=> [p1 [p2 p3]]; ee.
  move=> [p1 [p2 [p3 [p4 p5]]]]; ee.
symmetry;apply ordinal_p3; apply ordinal_omega.
Qed.

Lemma ordinal_finite1: forall x, is_ordinal x ->
  finite_set x -> finite_o x.
Proof.
move=> c ox fsx;red; ee.
move=> infc; rewrite (omega0_pr1 ox) in infc.
move: (sub_finite_set infc fsx).
move: infinite_Bnat.
rewrite /Bnat /finite_set => h1 h2; elim (infinite_dichot2 h2 h1).
Qed.

Lemma ordinal_finite2: forall x, is_ordinal x ->
  infinite_set x -> infinite_o x.
Proof.
move=> x bx ifs; ex_middle fo.
have fx: finite_o x by split.
move: (finite_cardinal_pr1 fx) => cx.
by red in ifs;move: ifs; rewrite (cardinal_of_cardinal cx).
Qed.

Lemma ordinal_finite3: forall x, is_ordinal x ->
  finite_set x -> x <o \omega.
Proof.
move=> x Bx ifs.
rewrite ordinal_lt_pr0; ee;first by apply omega0_ordinal.
by rewrite omega0_pr2 => //; apply ordinal_finite1.
Qed.

Lemma ordinal_finite4: forall x, is_ordinal x ->
  infinite_set x -> \omega <=o x.
Proof.
move=> x Bx ifs.
rewrite ordinal_le_pr0; ee;first by apply omega0_ordinal.
by rewrite -omega0_pr1 => //; apply ordinal_finite2.
Qed.

Lemma cardinal_Bnat: cardinal Bnat = Bnat.
Proof. apply cardinal_of_cardinal; apply omega0_cardinal. Qed.

Lemma emptyset_order: order emptyset.
Proof.
have <-: (inclusion_suborder emptyset=emptyset).
  apply is_emptyset;move=> y; rewrite /inclusion_suborder /graph_on Z_rw.
  aw; move=> [[_ [pe _]] _]; elim (emptyset_pr pe).
fprops.
Qed.

Lemma emptyset_substrate : substrate emptyset = emptyset.
Proof.
apply is_emptyset; move: emptyset_order => eo y ys.
have pe: (inc (J y y) emptyset) by order_tac.
elim (emptyset_pr pe).
Qed.

Lemma emptyset_worder: worder emptyset.
Proof.
split; first by apply emptyset_order.
rewrite emptyset_substrate.
move=> x xs [y yx]; elim (emptyset_pr (xs _ yx)).
Qed.

Lemma empty_substrate_zero: forall x, order x -> substrate x = emptyset ->
   x = emptyset.
Proof.
move=> x ox sx; apply is_emptyset;move=> y yx.
have gx : is_graph x by fprops.
have yp: y = J (P y) (Q y) by aw; rewrite gx.
rewrite yp in yx.
empty_tac1 (P y); substr_tac.
Qed.

Lemma ordinal_o_emptyset: ordinal_o emptyset = emptyset.
Proof. rewrite /ordinal_o; apply empty_substrate_zero; [fprops | aw ]. Qed.

Lemma ordinal0_emptyset: 0o = emptyset.
Proof. trivial. Qed.

Lemma ordinal0_pr: ordinal emptyset = 0o.
Proof.
have <-: ordinal_o emptyset = emptyset.
  rewrite /ordinal_o; apply empty_substrate_zero; [fprops| aw].
by rewrite (ordinal_p3 ordinal_0).
Qed.

Lemma ordinal0_pr1: forall x, order x -> substrate x = emptyset ->
  ordinal x = 0o.
Proof.
move=> x ox sx.
rewrite (empty_substrate_zero ox sx) ordinal0_pr //.
Qed.

Lemma singleton_worder: forall x,
  let E := singleton (J x x) in
   substrate E = singleton x & worder E.
Proof.
move=> x E.
have Ei: (E = identity_g (singleton x)).
  rewrite /identity_g /E /L.
  set_extens t; aw; [ move=> ->;ex_tac | move=> [z [zs]] <-; awi zs; ue].
have oE: (order E) by rewrite Ei; apply diagonal_order.
have sE: (substrate E = singleton x).
  set_extens y;aw.
    move => ys.
    have: (related E y y) by order_tac.
    rewrite /related /E; aw; apply pr1_def.
  move=> ->; have JE: (inc (J x x) E) by rewrite /E; fprops.
  substr_tac.
split =>//; split =>//.
move=> y yE [z zy]; exists z; red; aw;split => //.
move=> t ty; aw.
rewrite sE in yE; move: (yE _ zy)(yE _ ty); aw; move=> -> ->.
red; red; rewrite /E; fprops.
Qed.

Lemma singleton_order_isomorphic: forall x y,
  (singleton (J x x)) \Is (singleton (J y y)).
Proof.
move=> x y;set (f := fun _: Set => y).
move: (singleton_worder x) => [s1 [o1 _]].
move: (singleton_worder y) => [s2 [o2 _]].
have ta: transf_axioms f (singleton x) (singleton y) by move=> t;aw.
exists (BL f (singleton x) (singleton y)).
red; ee; aw.
  apply bl_bijective => //.
    by move=> u v; aw; move => -> ->.
  move=> t; aw; move=> ->; exists x; aw; rewrite /f; ee.
move=> a b; rewrite ! singleton_rw; move=> -> ->; aw.
rewrite /f/ gle/related;aw; apply iff_eq; intuition.
Qed.

Lemma singleton_order_isomorphic1: forall x,
  order x -> is_singleton (substrate x) ->
  exists v, x = singleton (J v v).
Proof.
move=> x or [u sxsu]; exists u; set_extens v.
  move=> vx; aw.
  have gx: (is_graph x) by fprops.
  have p: (v = J (P v) (Q v)) by rewrite (gx _ vx).
  rewrite p in vx.
  have : (inc (P v) (substrate x)) by substr_tac.
  have : (inc (Q v) (substrate x)) by substr_tac.
  rewrite sxsu; aw => p1 p2.
  by rewrite -{2} p1 -p2.
aw; move=> ->; order_tac; rewrite sxsu; fprops.
Qed.

Lemma singleton_order_isomorphic2: forall x y,
  order x -> order y ->
  is_singleton (substrate x) -> is_singleton (substrate y)
  -> x \Is y.
Proof.
move=> x y ox oy ssx ssy;
move: (singleton_order_isomorphic1 ox ssx)=> [u] ->.
move: (singleton_order_isomorphic1 oy ssy)=> [v] ->.
apply singleton_order_isomorphic.
Qed.

Lemma ordinal1_pr: forall x, ordinal (singleton (J x x)) = 1o.
Proof.
move=> x; move: (singleton_worder x) => [p1 p2].
apply (ordinal_p9 p2 ordinal_1).
apply singleton_order_isomorphic2; fprops.
  by rewrite p1; exists x.
by rewrite /ordinal_o /1o /card_one; aw; exists emptyset.
Qed.

Lemma singleton_ordinal: forall x,
  order x -> is_singleton (substrate x) ->
  ordinal x = 1o.
Proof.
move=> x ox sx; move: (singleton_order_isomorphic1 ox sx) => [y xy].
by rewrite xy ordinal1_pr.
Qed.

Definition ord_sum r g :=
   ordinal (order_sum r (L (domain g) (fun z => (ordinal_o (V z g))))).
Definition ord_prod r g :=
   ordinal (order_prod r (L (domain g) (fun z => (ordinal_o (V z g))))).
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 50).

Lemma variantLc_comp: forall a b f,
 (variantLc (f a) (f b)) = (L (domain (variantLc a b))
    (fun z => f (V z (variantLc a b)))).
Proof.
move=> a b f; apply fgraph_exten; gprops; fprops; bw.
move=> x xtp; try_lvariant xtp; fprops.
Qed.

Lemma ord_sum2_pr: forall a b,
  a +o b = ord_sum canonical_doubleton_order (variantLc a b).
Proof.
move=> a b; rewrite /ord_sum2 /ord_sum /order_sum2.
by rewrite variantLc_comp.
Qed.

Lemma ord_prod2_pr: forall a b,
  a *o b = ord_prod canonical_doubleton_order (variantLc b a).
Proof.
move=> a b; rewrite /ord_prod2 /ord_prod /order_prod2.
by rewrite variantLc_comp.
Qed.

Lemma ord_sum_ordinal: forall r g,
  worder r -> substrate r = domain g -> fgraph g ->
  (forall i, inc i (domain g) -> is_ordinal (V i g))
  -> is_ordinal (ord_sum r g).
Proof.
move=> r g or sr dg alo; rewrite /ord_sum; apply ordinal_p1.
apply order_sum_worder=>//; bw.
  gprops.
move=> i idg; bw; apply ordinal_p10; apply (alo _ idg).
Qed.

Lemma ord_prod_ordinal: forall r g,
  worder r -> substrate r = domain g -> fgraph g ->
  (forall i, inc i (domain g) -> is_ordinal (V i g))
  -> finite_set (substrate r)
  -> is_ordinal (ord_prod r g).
Proof.
move=> r g or sr dg alo fs; rewrite /ord_prod; apply ordinal_p1.
apply order_prod_worder =>//; bw.
  gprops.
move=> i idg; bw; apply ordinal_p10; apply (alo _ idg).
Qed.

Lemma ord_sum2_ordinal: forall a b, is_ordinal a -> is_ordinal b ->
  is_ordinal (a +o b).
Proof.
move=> a b wo1 wo2;rewrite /ord_sum2; apply ordinal_p1.
by apply order_sum2_worder; apply ordinal_p10.
Qed.

Lemma ord_prod2_ordinal: forall a b, is_ordinal a -> is_ordinal b ->
  is_ordinal (a *o b).
Proof.
move=> a b wo1 wo2;rewrite /ord_sum2; apply ordinal_p1.
by apply order_prod2_worder; apply ordinal_p10.
Qed.

Lemma ord_sum_invariant1: forall r r' f g g',
  order r -> substrate r = domain g -> fgraph g ->
  order r' -> substrate r' = domain g' -> fgraph g' ->
  order_isomorphism f r r' ->
  (forall i, inc i (substrate r) -> (V i g) \Is (V (W i f) g'))
  -> (order_sum r g) \Is (order_sum r' g').
Proof.
move=> r r' f g g' or sr fgg or' sr' fgf' oi ali.
have oa: (order_sum_a r g).
  by red;ee; rewrite -sr=> i idg; move: (ali _ idg)=> [h [o1 [o2 _]]].
move: oi => [_ [_ [[[ff ijf] sjf] [srf [tgf oif]]]]].
have oa': order_sum_a r' g'.
  red;ee; rewrite -sr' tgf=> i idg.
  move: (surjective_pr2 sjf idg) => [x [xsf]] <-.
  by rewrite -srf in xsf; move: (ali _ xsf)=> [h [o1 [o2 _]]].
move: (order_sum_order oa) (order_sum_order oa') => h1 h2; aw.
set (fa := fam_of_substrates g).
set (fb := fam_of_substrates g').
set (oj := fun i =>
    choose (fun z => order_isomorphism z (V i g) (V (W i f) g'))).
have ojp: (forall i, inc i (substrate r) ->
    order_isomorphism (oj i) (V i g) (V (W i f) g')).
  by move=> i isr; rewrite /oj; apply choose_pr; move: (ali _ isr).
set (h := fun x=> J (W (P x) (oj (Q x))) (W (Q x) f)).
have ta: (forall x, inc x (disjoint_union fa) -> inc (h x) (disjoint_union fb)).
  move=> x xd; move: (du_index_pr xd); rewrite /fa/fam_of_substrates.
  rewrite L_domain; move=> [qd]; bw; move => [ps px].
  rewrite /h.
  have wq: (inc (W (Q x) f) (domain g')).
    rewrite -sr' tgf. by apply inc_W_target; [ fct_tac | rewrite -srf sr].
  rewrite /fb /fam_of_substrates.
  apply inc_disjoint_union; bw.
  rewrite sr in ojp;move: (ojp _ qd) => [_ [_ [fx [sx [tx _]]]]].
  by rewrite tx; apply inc_W_target; [ fct_tac | ue].
have ta1: (transf_axioms h (substrate (order_sum r g))
    (substrate(order_sum r' g'))) by bw.
exists (BL h (substrate (order_sum r g)) (substrate (order_sum r' g'))).
red; rewrite bl_source bl_target; ee; bw.
  apply bl_bijective =>//.
    rewrite /h;move=> 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) .
      apply ijf; [rewrite -srf;ue | rewrite -srf;ue | exact ].
    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 :(surjective_pr2 sjf Qy) =>[x [xsf Wx]].
  rewrite -srf in xsf; move: (ojp _ xsf) => [_ [_ [[_ sjj] [sfj [tjj _]]]]].
  rewrite -Wx tjj in Py; move: (surjective_pr2 sjj Py)=> [x0 [x0s x0w]].
  exists (J x0 x); ee.
    apply inc_disjoint_union1; ue.
  rewrite /h; aw; rewrite Wx x0w; aw.
move=> x y xs ys; aw; move: ta1; bw => ta2.
rewrite (order_sum_gle oa) (order_sum_gle oa').
move: (ta2 _ xs)(ta2 _ ys).
set (q1:= inc (h x) (sum_of_substrates g')).
set (q2:= inc (h y) (sum_of_substrates g')).
move => q1t q2t.
rewrite /h.
move: (du_index_pr1 xs) (du_index_pr1 ys) => [Qx [Px px]][Qy [Py py]].
have aux: (glt r' (W (Q x) f) (W (Q y) f) = glt r (Q x) (Q y)).
  rewrite -sr srf in Qx Qy.
  rewrite /glt; rewrite oif //; apply iff_eq; move=> [p1 p2]; ee.
    by dneg xy; rewrite xy.
rewrite /order_sum_r ! pr1_pair ! pr2_pair aux.
rewrite -srf sr in ijf; move: (ijf _ _ Qx Qy) => p0.
rewrite -sr in Qx; move: (ojp _ Qx) => [_ [_ [_ [sfj [tjj ojj]]]]].
rewrite -sfj in ojj.
apply iff_eq; move=> [xs1 [ys1 lep]]; ee; case lep.
      move=> qlt; auto.
    move=> [p1 p2]; rewrite -p1 in Py |- *.
    right; ee; rewrite -ojj //.
   move=> qlt; auto.
   move=> [p1 p2].
move:(p0 p1) => sq; right; split => //.
rewrite -sq in Py p2 ojj.
rewrite ojj //.
Qed.

Lemma ord_sum_invariant2: forall r g g',
  order r -> substrate r = domain g -> fgraph g ->
  substrate r = domain g' -> fgraph g' ->
  (forall i, inc i (substrate r) -> (V i g) \Is (V i g'))
  -> (order_sum r g) \Is (order_sum r g').
Proof.
move=> r g g' or sr fgg sr' fgg' ai.
apply (ord_sum_invariant1 or sr fgg or sr' fgg' (identity_isomorphism or)).
move => i isr; rewrite identity_W //; apply ai =>//.
Qed.

Lemma ord_sum_invariant3: forall r g,
  worder r -> substrate r = domain g -> fgraph g ->
  (forall i, inc i (domain g) -> worder (V i g)) ->
  ordinal (order_sum r g) =
    ord_sum r (L (substrate r) (fun i => ordinal (V i g))).
Proof.
move => r g wor sr fgg alo.
have or: order r by fprops.
rewrite /ord_sum; apply ordinal_p8.
  apply order_sum_worder => //.
  apply order_sum_worder; [ exact | bw | gprops | ].
    bw; move=> i isr; bw.
    rewrite sr in isr; apply (ordinal_p10 (ordinal_p1 (alo _ isr))).
apply ord_sum_invariant2; ee; [ bw | bw].
rewrite sr;move=> i isr ; bw; apply (ordinal_p2 (alo _ isr)).
Qed.

Lemma ord_sum_invariant4: forall r1 r2 r3 r4,
  r1 \Is r3 -> r2 \Is r4 ->
  (order_sum2 r1 r2) \Is (order_sum2 r3 r4).
Proof.
move=> r1 r2 r3 r4 h1 h2; rewrite /order_sum2.
apply ord_sum_invariant2; rewrite ?substrate_canonical_doubleton_order; bw.
      by move: worder_canonical_doubleton_order => [res _].
    fprops.
   fprops.
move=> i itp; try_lvariant itp.
Qed.

Lemma ord_prod_invariant1: forall r r' f g g',
  worder r -> substrate r = domain g -> fgraph g ->
  order r' -> substrate r' = domain g' -> fgraph g' ->
  order_isomorphism f r r' ->
  (forall i, inc i (substrate r) -> (V i g) \Is (V (W i f) g'))
  -> (order_prod r g) \Is (order_prod r' g').
Proof.
move=> r r' f g g' wor sr fgg or' sr' fgf' oif ali.
have aux: (order_isomorphic r r') by 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: (lexicographic_order_axioms r g).
  by red;ee; rewrite -sr=> i idg; move: (ali _ idg)=> [h [o1 [o2 _]]].
have oa': lexicographic_order_axioms r' g'.
  red;ee. rewrite -sr' tgf=> i idg.
  move: (surjective_pr2 sjf idg) => [x [xsf]] <-.
  by rewrite -srf in xsf; move: (ali _ xsf)=> [h [o1 [o2 _]]].
move: (lexorder_order oa)(lexorder_order oa') => o1 o2; aw.
set (fa := fam_of_substrates g).
set (fb := fam_of_substrates g').
set (oi := fun i =>
    choose (fun z => order_isomorphism z(V i g) (V (W i f) g'))).
have oip: (forall i, inc i (substrate r) ->
    order_isomorphism (oi i) (V i g) (V (W i f) g')).
  by move=> i isr; apply choose_pr; by move:(ali _ isr).
set (fi := fun i => W i (inverse_fun f)).
have fip: (forall i, inc i (substrate r') -> W (fi i) f = i).
   move=> i isr; symmetry; apply W_inverse =>//; ue.
have fis: (forall i, inc i (substrate r') -> inc (fi i) (substrate r)).
  rewrite tgf srf; move=> i isf; apply W_inverse3 =>//.
set (fj := fun i => W i 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; symmetry;apply W_inverse2 =>//.
set (h := fun z=> L (substrate r') (fun i => W (V (fi i) z) (oi (fi i)))).
set (A := substrate(lexicographic_order r g)).
set (B := substrate(lexicographic_order r' g')).
have HA : A = (prod_of_substrates g) by rewrite /A lexorder_substrate.
have HB : B = (prod_of_substrates g') by rewrite /B lexorder_substrate.
have ta: (forall z, inc z A -> inc (h z) B).
  rewrite HA HB /prod_of_substrates /fam_of_substrates /h.
  move => z; rewrite productb_rw; try apply L_fgraph; move=> [fgf [dz iVV]].
  rewrite productb_rw; try apply L_fgraph; ee; first by bw.
  bw; move=> i isr; bw; try ue.
  move: (fis _ isr) => fisr.
  move: (oip _ fisr) => [_ [_ [boi [soi [toi _ ]]]]].
  move: dz; bw; move=> dz; rewrite dz -sr in iVV.
  rewrite (fip _ isr) in toi; rewrite toi;apply inc_W_target; first by fct_tac. move: (iVV _ fisr); bw; ue.
have ta': (forall w, inc w B -> exists z, inc z A & h z = w).
  rewrite HA HB /prod_of_substrates /fam_of_substrates /h => w.
  rewrite productb_rw; try apply L_fgraph; move=> [fgf [dz iVV]].
  exists (L (substrate r) (fun i => W (V (fj i) w) (inverse_fun (oi i)))).
  move: dz; bw => dz.
  split.
    aw; last (by gprops); ee; bw.
    move=> i isr.
    have idg: inc i (domain g) by ue.
    bw;move: (oip _ isr) => [_ [_ [boi [soi [toi _ ]]]]].
    rewrite soi; apply W_inverse3 =>//; rewrite -toi.
    move: (fjs _ isr) => fjsr.
    rewrite dz -sr' in iVV; move: (iVV _ fjsr); bw.
  symmetry; apply fgraph_exten; [exact | gprops | bw; ue | ].
  move=> x xdw.
  have xsr: inc x (substrate r') by rewrite sr' -dz.
  have fisr: inc (fi x) (substrate r) by apply fis.
  bw; rewrite /fj fip //.
  move: (oip _ fisr) => [_ [_ [boi [soi [toi _ ]]]]].
  move: (iVV _ xdw); bw; try ue; move => p1.
  by apply W_inverse =>//; rewrite -toi fip.
have hi: (forall z z', inc z A -> inc z' A -> h z = h z' -> z = z').
  have fgf: (fgraph (fam_of_substrates g)).
    rewrite /fam_of_substrates; gprops.
  rewrite HA => z z' zA zA';move: (zA) (zA'); rewrite/ prod_of_substrates.
  move=> p1 p2 p3; apply (productb_exten fgf p1 p2).
  rewrite /fam_of_substrates; bw.
  move=> i idg; move: (prod_of_substrates_pr idg p1) =>p4.
  move: (prod_of_substrates_pr idg p2)=> p5.
  rewrite -sr in idg; move: (fij _ idg)(fjs _ idg) => p6 p7.
  move: (f_equal (V (fj i)) p3); rewrite /h; bw; rewrite p6.
  move: (oip _ idg) => [_ [_ [[[_ ioi] _] [soi [toi _ ]]]]].
  apply ioi; ue.
have ta2: (transf_axioms h A B) by [].
exists (BL h A B).
red; ee;aw; first by apply bl_bijective.
move=> x y xA yA; rewrite bl_W // bl_W //.
rewrite /h.
rewrite ! order_prod_gle //.
rewrite -HA -HB.
move: (ta _ xA) (ta _ yA); rewrite /h.
set xv:= L _ _; set yv:= L _ _.
move=> xvB yvB.
apply iff_eq; move=> [_ [_ hyp]]; split; try exact; split; try exact.
   rewrite /xv /yv;case hyp=> aux; first by left; rewrite aux.
   move: aux => [j [jst [jlt ieq]]]; right.
   move: (fjs _ jst)(fij _ jst) => fjst fijt; ex_tac.
   split.
     bw; rewrite fijt; apply (order_isomorphism_pr2 (oip _ jst)) => //.
   move=> i ifj.
   have isr: inc i (substrate r') by order_tac.
   bw;rewrite (ieq (fi i)) // (order_isomorphism_pr0 oif) //.
      rewrite fip //.
   apply fis =>//.
case hyp=> aux; first by left; apply hi =>//.
right; move: aux => [j [jsr [jlt jle]]].
move: (fip _ jsr)(fis _ jsr) => fipa fisa.
ex_tac; split.
  move: jlt ; rewrite /xv /yv; bw.
  set a:= (V (fi j) x); set b:= (V (fi j) y).
  have ais: inc a (substrate (V (fi j) g)) by apply prod_of_substrates_pr; ue.
  have bis: inc b (substrate (V (fi j) g)) by apply prod_of_substrates_pr; ue.
  rewrite (order_isomorphism_pr0 (oip _ fisa) ais bis) fipa //.
move=> i lti.
move: (order_isomorphism_pr2 oif lti) => aux.
have fis': (inc (W i f) (substrate r')) by order_tac.
move: aux; rewrite fipa=> aux.
move: (jle _ aux); rewrite /xv /yv; bw.
have isr: inc i (substrate r) by order_tac.
rewrite fij //.
move: (oip _ isr) => [_ [_ [[[_ ioi] _] [soi [toi _ ]]]]].
apply ioi;rewrite -soi.
  move: xA; rewrite HA; apply prod_of_substrates_pr; ue.
  move: yA; rewrite HA; apply prod_of_substrates_pr; ue.
Qed.

Lemma ord_prod_invariant2: forall r g g',
  worder r -> substrate r = domain g -> fgraph g ->
  substrate r = domain g' -> fgraph g' ->
  (forall i, inc i (substrate r) -> (V i g) \Is (V i g'))
  -> (order_prod r g) \Is (order_prod r g').
Proof.
move=> r g g' wor sr fgf sr' fgg' alo.
have or: (order r) by move: wor => [or _].
apply (ord_prod_invariant1 wor sr fgf or sr' fgg' (identity_isomorphism or)).
by move=> i isr; rewrite identity_W //; apply alo.
Qed.

Lemma ord_prod_invariant3: forall r g,
  worder r -> substrate r = domain g -> fgraph g ->
  (forall i, inc i (domain g) -> worder (V i g)) ->
  finite_set (substrate r) ->
  ordinal (order_prod r g) =
    ord_prod r (L (substrate r) (fun i => ordinal (V i g))).
Proof.
move => r g wor sr fgg alo fsr.
have or: order r by fprops.
rewrite /ord_prod; apply ordinal_p8.
    apply order_prod_worder => //.
  apply order_prod_worder; [ exact | bw | gprops | | exact ].
  bw; move=> i isr; bw.
  rewrite sr in isr; apply (ordinal_p10 (ordinal_p1 (alo _ isr))).
apply ord_prod_invariant2; ee; [ bw | bw].
rewrite sr;move=> i isr ; bw; apply (ordinal_p2 (alo _ isr)).
Qed.

Lemma ord_prod_invariant4: forall r1 r2 r3 r4,
  r1 \Is r3 -> r2 \Is r4 ->
  (order_prod2 r1 r2) \Is (order_prod2 r3 r4).
Proof.
move=> r1 r2 r3 r4 h1 h2; rewrite /ord_prod2 /order_prod2.
apply ord_prod_invariant2; rewrite ?substrate_canonical_doubleton_order; bw.
      apply worder_canonical_doubleton_order.
    fprops.
   fprops.
move=> i itp; try_lvariant itp.
Qed.

Lemma ord_sum_invariant5: forall a b c, worder a -> worder b ->
  (order_sum2 a b) \Is c ->
  (ordinal a) +o (ordinal b) = ordinal c.
Proof.
move=> a b c oa ob h.
rewrite /ord_sum2; apply ordinal_p8.
  apply order_sum2_worder.
    apply (ordinal_p10 (ordinal_p1 oa)).
    apply (ordinal_p10 (ordinal_p1 ob)).
  move: h (order_sum2_worder oa ob); apply worder_invariance.
apply orderIT with (order_sum2 a b) => //; apply ord_sum_invariant4.
  apply orderIS; apply (ordinal_p2 oa).
apply orderIS; apply (ordinal_p2 ob).
Qed.

Lemma ord_prod_invariant5: forall a b c, worder a -> worder b->
  (order_prod2 a b) \Is c ->
  (ordinal a) *o (ordinal b) = ordinal c.
Proof.
move=> a b c oa ob h.
rewrite /ord_prod2; apply ordinal_p8.
  apply order_prod2_worder.
    apply (ordinal_p10 (ordinal_p1 oa)).
    apply (ordinal_p10 (ordinal_p1 ob)).
  move: h (order_prod2_worder oa ob); apply worder_invariance.
apply orderIT with (order_prod2 a b) => //; apply ord_prod_invariant4.
  apply orderIS; apply (ordinal_p2 oa).
apply orderIS; apply (ordinal_p2 ob).
Qed.

Lemma order_prod_pr1: forall a b c,
  is_ordinal a -> is_ordinal b -> order_isomorphic (ordinal_o b) c ->
  a *o b = ord_sum c (cst_graph (substrate c) a).
Proof.
move=> a b c ota otb ibc.
move: (ordinal_p10 ota) => wo0.
move: (ordinal_p10 otb) => wo1.
move: (worder_invariance ibc wo1) => wo2.
rewrite /ord_prod2 /ord_sum.
have ->: domain (cst_graph (substrate c) a) = substrate c.
   rewrite /cst_graph; bw.
apply ordinal_p8.
  by apply order_prod2_worder; apply ordinal_p10.
  apply order_sum_worder; [exact | bw | gprops | bw].
  move=> i isc; rewrite /cst_graph; bw;apply (ordinal_p10 ota).
move: (order_prod_pr (worder_is_order wo0)(worder_is_order wo1)).
set aux := order_sum _ _ .
move=> h; apply orderIT with aux; first by apply h.
move: ibc => [f isf].
rewrite /aux /cst_graph; apply ord_sum_invariant1 with f; bw;gprops; fprops.
move: isf => [_ [_ [[[ff _]] _] [sf [tf _]]]].
rewrite sf; move=> i id.
move: (inc_W_target ff id); rewrite -tf=> vt.
bw; apply orderIR; fprops.
Qed.

Lemma ord_sum_emptyset: forall r x,
  order r -> substrate r = domain x -> fgraph x ->
  substrate r = emptyset ->
  ord_sum r x = 0o.
Proof.
move=> r x or sr fgx sre.
have oa:order_sum_a r (L (domain x) (fun z : Set => ordinal_o (V z x))).
  by red;ee;bw; rewrite -sr sre; move => i ie; elim (emptyset_pr ie).
rewrite /ord_sum; apply ordinal0_pr1.
  by apply order_sum_order.
rewrite order_sum_substrate //.
apply is_emptyset; move=> t ts; move: (du_index_pr1 ts).
rewrite -sr sre L_domain; move => [qe _]; elim (emptyset_pr qe).
Qed.

Lemma ord_prod_emptyset: forall r x,
  worder r -> substrate r = domain x -> fgraph x ->
  substrate r = emptyset ->
  ord_prod r x = 1o.
Proof.
move=> r x wor sr fgx sre.
have la: (lexicographic_order_axioms r (L (domain x)
   (fun z => ordinal_o (V z x)))).
  red; bw;ee; rewrite -sr sre; move=> i idx; elim (emptyset_pr idx).
rewrite /ord_prod; apply singleton_ordinal.
apply order_prod_order; first by red; ee.
rewrite lexorder_substrate // /prod_of_substrates /fam_of_substrates -sr sre.
rewrite trivial_fgraph emptyset_domain trivial_fgraph product_trivial.
by exists emptyset.
Qed.

Lemma worder_singleton1: forall r e,
 order r -> substrate r = singleton e -> worder r.
Proof.
move=> r e or sr.
have aux: r = singleton (J e e).
  set_extens t; aw.
    move=> tr.
    have tp: t = J (P t) (Q t) by aw; rewrite (order_is_graph or tr).
    rewrite tp in tr |- *.
    move: (inc_arg1_substrate tr) (inc_arg2_substrate tr).
    by rewrite sr !singleton_rw; move=> -> ->.
  move=> ->; order_tac; rewrite sr; aw.
move: (singleton_worder e) => [_ h]; ue.
Qed.

Lemma ord_sum_singleton: forall r x e,
  order r -> substrate r = domain x -> fgraph x ->
  substrate r = singleton e -> is_ordinal (V e x) ->
  ord_sum r x = V e x.
Proof.
move=> r x e or sr fgf srs otve.
rewrite sr in srs.
have edx: (inc e (domain x)) by rewrite srs; fprops.
rewrite srs in sr;move: (worder_singleton1 or sr) => wor.
rewrite /ord_sum.
move: (ordinal_p10 otve) => ove.
set g := L _ _.
have osa: order_sum_a r g.
   rewrite /g; red;ee; first by bw; ue.
   bw; rewrite srs; move=> i idx; bw; awi idx; rewrite idx; fprops.
have wos: worder(order_sum r g).
  apply order_sum_worder=> //.
      rewrite /g; bw; ue.
    rewrite /g; gprops.
  rewrite /g; bw; rewrite srs; move=> i idx; bw; awi idx; rewrite idx; fprops.
apply (ordinal_p9 wos otve).
set (E:= substrate (order_sum r g)); set (F := substrate (ordinal_o (V e x))).
have He:E =sum_of_substrates g by rewrite /E order_sum_substrate //.
have Hf:F = V e x by rewrite /F; apply (ordinal_p7 otve).
have uE: (forall u, inc u E = (is_pair u & Q u = e & inc (P u) F)).
  move=> u; rewrite He /g; apply iff_eq.
    move=> us; move: (du_index_pr1 us).
    rewrite L_domain; move=> [Qu]; bw.
    rewrite srs in Qu; awi Qu; rewrite Qu; ee.
  move => [pu [Qu Pu]].
  have uJ: (u = J (P u) (Q u)) by aw.
  by rewrite uJ Qu; apply inc_disjoint_union1; bw.
have ta: (transf_axioms P E F).
  move=> t; rewrite uE; intuition.
exists (BL P E F).
red; ee; [ | symmetry ;aw | symmetry; aw |].
  apply bl_bijective => //.
    move=> u v; rewrite uE uE; aw; move=> [pu [Qu Pu]][pv [Qv Pv]] sp.
    apply pair_exten =>//; ue.
  move=> y ys; exists (J y e); rewrite uE; aw; ee.
rewrite bl_source;move=> a b aE bE; rewrite ! bl_W //.
move: (aE)(bE); rewrite {1} uE {1} uE; move=> [pu [Qu Pu]][pv [Qv Pv]].
rewrite (order_sum_gle osa) /order_sum_r -He -Hf Qu Qv.
rewrite /g Hf /glt; bw; apply iff_eq; intuition.
Qed.

Lemma ord_prod_singleton: forall r x e,
  order r -> substrate r = domain x -> fgraph x ->
  substrate r = singleton e -> is_ordinal (V e x) ->
  ord_prod r x = V e x.
Proof.
move=> r x e or sr fgf srs otve.
rewrite sr in srs.
have edx: (inc e (domain x)) by rewrite srs; fprops.
rewrite srs in sr;move: (worder_singleton1 or sr) => wor.
rewrite /ord_prod.
move: (ordinal_p10 otve) => ove.
set g := L _ _.
have la: (lexicographic_order_axioms r g).
  rewrite /g; red; ee; first by bw; ue.
  bw; move=> i; rewrite srs=> id; bw; aw; fprops.
move: (lexorder_order la) => ora.
have wos: worder(order_prod r g).
  apply order_prod_worder=> //.
       rewrite /g; bw;ue.
    rewrite /g; gprops.
  rewrite /g; bw; rewrite srs; move=> i idx; bw; awi idx; rewrite idx; fprops.
  rewrite sr; apply singleton_finite.
apply (ordinal_p9 wos otve).
move: (lexorder_substrate la).
set E:= substrate (lexicographic_order r g).
set F := substrate (ordinal_o (V e x)).
have Hf:F = V e x by rewrite /F; apply (ordinal_p7 otve).
have Hf': F = substrate (V e g) 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); rewrite /g ; bw.
have ta: transf_axioms (V e) E F.
  move=> t; rewrite slo Hf'; apply (prod_of_substrates_pr eg).
have Hc:forall a b, inc a E-> inc b E -> V e a = V e b -> a = b.
  have fg: (fgraph (L (singleton e) (fun i => substrate (V i g)))) by gprops.
  move=> a b; rewrite slo' dg => aE bE sV.
  by apply (productb_exten fg aE bE); bw; move=> i; aw; move => ->.
exists (BL (V e) E F).
red; rewrite bl_source bl_target; ee.
  apply bl_bijective =>//.
  move=> y ys; exists (L (singleton e) (fun _:Set => y)).
  rewrite slo' dg ; aw; bw; ee.
  by move=> i ie; bw; awi ie; rewrite ie -Hf'.
move=> a b aE bE; rewrite bl_W // bl_W //.
rewrite order_prod_gle // -slo; apply iff_eq.
  move=> [_ [_ hyp]]; case hyp.
     move: (worder_is_order ove) => orve.
     move=> ->; order_tac.
     move: bE; rewrite slo'; aw; bw; last by gprops.
     move=> [fgb [db aux]].
     have ed: inc e (domain b) by rewrite db dg; aw.
     by move: (aux _ ed); rewrite /g;bw; rewrite -/F Hf.
  rewrite sr srs;move=> [j [jsr]]; bw.
  by awi jsr; rewrite jsr; move=> [[jle _] _].
rewrite sr.
move=> h.
case (equal_or_not a b) => ab; ee.
right; exists e; ee.
  bw; split => //; first by dneg nab; apply Hc =>//.
move=> i [lie ine].
have : inc i (substrate r) by order_tac.
rewrite sr; aw=> h'; elim ine; auto.
Qed.

Lemma zero_unit_sum_ord1: forall r g j,
  order_sum_a r g -> sub j (domain g) ->
  (forall i, inc i (complement (domain g) j) -> V i g = emptyset) ->
  (order_sum r g) \Is (order_sum (induced_order r j) (restr g j)).
Proof.
move=> r g j oa sj alz.
move: (oa) => [or [sr [fgg alo]]].
have dr: (domain (restr g j)) = j by rewrite restr_domain1.
have sj1: sub j (substrate r) by ue.
have oa': order_sum_a (induced_order r j) (restr g j).
  red; aw;ee;rewrite dr;move=> i id;rewrite restr_ev //.
  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 inc_disjoint_union1 => //; rewrite restr_ev //; ue.
    have Qx: inc (Q z) (complement (domain g) j) by srw; ee;ue.
    move: (alz _ Qx) => Ve.
    rewrite Ve emptyset_substrate in Pd; elim (emptyset_pr Pd).
  move => zs; move: (du_index_pr1 zs) => [Qd [Pd pz]].
  have ->: z = J (P z) (Q z) by aw.
  apply inc_disjoint_union1 => //.
     rewrite -sr; apply sj1; ue.
  move: Pd; rewrite restr_ev //; ue.
exists (identity E).
red; rewrite identity_source; ee.
    apply identity_bijective.
  rewrite identity_target //.
have a1: forall x, inc x F -> inc (Q x) j.
   move=> x; rewrite /F; bw => xs; move: (du_index_pr1 xs)=> [aux _]; ue.
move=> x y xE yE; rewrite identity_W // identity_W //.
rewrite (order_sum_gle oa) (order_sum_gle oa').
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 <-: (gle (induced_order r j) (Q x) (Q y) = (gle r (Q x) (Q y))).
   rewrite /gle/related/induced_order; apply iff_eq; aw; first by move=> [ok _].
   move=> h; ee; rewrite /coarse; aw; ee; apply a1; ue.
have ->: V (Q x) (restr g j) = (V (Q x) g).
  rewrite restr_ev //; apply a1; ue.
done.
Qed.

Lemma zero_unit_sum_ord2: forall r g j,
  worder r -> substrate r = domain g -> fgraph g ->
  (forall i, inc i (domain g) -> is_ordinal (V i g)) ->
  sub j (domain g) ->
  (forall i, inc i (complement (domain g) j) -> V i g = 0o) ->
  ord_sum r g = ord_sum (induced_order r j) (restr g j).
Proof.
move=> r g j wor sr fgg albo jg alz.
have jsr: sub j (substrate r) by ue.
have or: order r by fprops.
have jd: j = domain (restr g j) by rewrite restr_domain1.
rewrite /ord_sum; apply ordinal_p8.
   apply order_sum_worder; [ exact | bw | gprops | bw ].
   by move => i idg; bw; apply ordinal_p10; apply albo.
 apply order_sum_worder; [ apply worder_restriction => // | bw; aw |gprops |]. rewrite -jd; bw; move=> i idg; bw; apply ordinal_p10; apply albo.
 by apply jg.
set g1:= (L (domain g) (fun z : Set => ordinal_o (V z g))).
have ->: (L (domain (restr g j)) (fun z : Set => ordinal_o (V z (restr g j)))
  = (restr g1 j)).
  rewrite /g1; apply fgraph_exten.
    - gprops.
    - apply restr_fgraph; gprops.
    - bw; rewrite -jd restr_domain1 //; gprops; bw.
    - bw; rewrite -jd => x xd; bw; [ by apply jg |gprops].
have dg1: domain g1 = domain g by rewrite /g1; bw.
apply zero_unit_sum_ord1.
    split; first by exact.
    split; first by ue.
    split; first rewrite /g1; gprops.
    rewrite dg1; move=> i idg; rewrite /g1; bw.
    apply (ordinal_p11 (albo _ idg)).
  ue.
rewrite dg1; move=> i ic. rewrite /g1; bw.
  rewrite (alz _ ic); apply empty_substrate_zero.
    apply (ordinal_p11 ordinal_0).
    by rewrite (ordinal_p7 ordinal_0).
by move: ic; srw; move => [ok _].
Qed.

Lemma one_unit_prod_ord1: forall r g j,
  order_prod_a r g -> sub j (domain g) ->
  (forall i, inc i (complement (domain g) j)
     -> is_singleton (substrate (V i g))) ->
  (order_prod r g) \Is (order_prod (induced_order r j) (restr g j)).
Proof.
move=> r g j oa sj alz.
move: (oa) => [or [sr [fgg alo]]].
have dr: (domain (restr g j)) = j by rewrite restr_domain1.
have sj1: sub j (substrate r) by ue.
have oa': order_prod_a (induced_order r j) (restr g j).
  red; red;aw; ee; first by apply worder_restriction => //.
  rewrite dr;move=> i id;rewrite restr_ev //; 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 ;gprops.
have fg2: fgraph (fam_of_substrates g) by rewrite /fam_of_substrates ;gprops.
have dg1: domain (fam_of_substrates g) = domain g
    by rewrite /fam_of_substrates; bw.
have dgr: domain (fam_of_substrates (restr g j)) = j.
  rewrite /fam_of_substrates restr_domain1 //; bw.
have rd: j = domain (restr g j) by rewrite restr_domain1 //.
have ta: transf_axioms (fun z => restr z j) E F.
   move=> z; rewrite Ep Fp /prod_of_substrates.
   aw; move=> [fgz [dz iVV]]; rewrite dg1 in dz.
   have sj2: sub j (domain z) by ue.
   ee; first by rewrite dgr restr_domain1 //; bw.
   move=> i; rewrite restr_domain1 // => ij.
   rewrite /fam_of_substrates //; bw; last by ue.
   move: (iVV _ (sj2 _ ij)); rewrite /fam_of_substrates; bw.
   by rewrite -dz; apply sj2.
have specs: forall i x y, inc i (domain g) -> ~ inc i j ->
  domain x = domain (fam_of_substrates g) ->
  domain y = domain (fam_of_substrates g) ->
  (forall i, inc i (domain x) -> inc (V i x) (V i (fam_of_substrates g))) ->
  (forall i, inc i (domain y) -> inc (V i y) (V i (fam_of_substrates g))) ->
  V i x = V i y.
  move=> i x y idg nij dx dy p1 p2.
  have xc: (inc i (complement (domain g) j)) by srw; ee.
  have xdu: inc i (domain x).
     by move: dx; rewrite /fam_of_substrates ; bw => ->.
   have xdv: inc i (domain y).
     by move: dy; rewrite /fam_of_substrates; bw => ->.
  move: (p1 _ xdu);rewrite /fam_of_substrates; bw => h1.
  move: (p2 _ xdv);rewrite /fam_of_substrates; bw => h2.
  by move: (alz _ xc); rewrite is_singleton_rw; move=> [_]; 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 /prod_of_substrates; aw.
  move=> [fgu [du up]][fgv [dv vp]] sar.
  apply fgraph_exten => //; first by ue.
  have sj3: sub j (domain u) by rewrite du dg1.
  have sj4: sub j (domain v) by rewrite dv dg1.
  rewrite du dg1; move=> x xdg; case (inc_or_not x j).
    move=> xj; move: (f_equal (V x) sar); rewrite restr_ev// restr_ev//.
  move=> nxj.
  apply specs => //.
exists (BL (fun z => restr z j) E F).
red; rewrite bl_source bl_target; ee.
  apply bl_bijective => //.
  move=> y; rewrite Ep Fp /prod_of_substrates; aw.
  move=> [fgy [dy iVV]].
  set x := (L (domain g)
    (fun z => Yo (inc z j) (V z y) (rep (substrate (V z g))))).
  have fgx: fgraph x by rewrite /x; gprops.
  have dx: domain x = domain g by rewrite /x; bw.
  exists x; split.
    aw; rewrite dx; ee; move=> i idx; rewrite /fam_of_substrates; bw.
    rewrite /x; bw; Ytac1 xj.
      rewrite dy dgr in iVV; move: (iVV _ xj); bw.
      rewrite /fam_of_substrates; bw; ue.
    apply nonempty_rep.
    have xc: (inc i (complement (domain g) j)) by srw; ee.
    by move: (alz _ xc); rewrite is_singleton_rw; intuition.
  have sj3: sub j (domain x) by ue.
  have dr3: domain (restr x j) = domain y by rewrite restr_domain1 // dy dgr.
  apply fgraph_exten => //; fprops.
  move=> i; rewrite dr3 dy dgr => ij; rewrite restr_ev //.
  by rewrite /x; bw; [ Ytac0 | apply sj].
have sjr: sub j (substrate r) by ue.
have odr: order r by move: or => [or _].
move=> x y xE yE; rewrite bl_W // bl_W//.
rewrite order_prod_gle // order_prod_gle // -Fp -Ep.
have ->: substrate (induced_order r j) = j by rewrite substrate_induced_order.
move: (xE)(yE); rewrite Ep /prod_of_substrates; aw.
move=> [fgx [dx iVVx]] [fgy [dy iVVy]].
have sjx: sub j (domain x) by rewrite dx dg1.
have sjy: sub j (domain y) by rewrite dy dg1.
have raux: forall k, inc k j ->
    glt (V k (restr g j)) (V k (restr x j)) (V k (restr y j))=
    glt (V k g) (V k x) (V k y).
  move=> k kj; rewrite restr_ev // restr_ev // restr_ev //.
apply iff_eq; move=> [_ [_ hyp]].
  split; first( by apply ta); split; first by apply ta.
  case hyp; first by move=> -> ; left.
  move => [k [ksr [klt kle]]]; right; exists k.
  case (inc_or_not k j) => kj.
    ee; first by rewrite raux.
    move => i ilt.
    move: (iorder_gle4 ilt) => [ij _].
    rewrite restr_ev // restr_ev //.
    apply (kle _ (iorder_gle2 ilt)).
  rewrite sr in ksr; move: klt => [_ bad]; elim bad.
  apply specs => //.
split => //; split => //; case hyp; first by move => aux; left; apply ri.
move => [k [ksr [klt kle]]]; right; exists k.
rewrite sr; split; first by apply sj.
split; first by rewrite -raux.
move=> i ik; case (inc_or_not i j) => ij.
  have lik: glt (induced_order r j) i k by rewrite /glt; aw.
  move: (kle _ lik); rewrite restr_ev// restr_ev//.
have isr: inc i (domain g) by rewrite -sr;order_tac.
apply specs => //.
Qed.

Lemma one_unit_prod_ord2: forall r g j,
  worder r -> substrate r = domain g -> fgraph g ->
  (forall i, inc i (domain g) -> is_ordinal (V i g)) ->
  finite_set (substrate r) ->
  sub j (domain g) ->
  (forall i, inc i (complement (domain g) j) -> V i g = 1o) ->
  ord_prod r g = ord_prod (induced_order r j) (restr g j).
Proof.
move=> r g j wor sr fgg albo fs jg alz.
have jsr: sub j (substrate r) by ue.
have or: order r by fprops.
have jd: j = domain (restr g j) by rewrite restr_domain1.
rewrite /ord_prod; apply ordinal_p8.
    apply order_prod_worder; [ exact | bw | gprops | bw | gprops ].
    by move => i idg; bw; apply ordinal_p10; apply albo.
  apply order_prod_worder; gprops.
        apply worder_restriction => //.
      bw; aw.
    rewrite -jd; bw; move=> i idg; bw; apply ordinal_p10; apply albo.
    by apply jg.
  aw; apply (sub_finite_set jsr fs).
set g1:= (L (domain g) (fun z : Set => ordinal_o (V z g))).
have ->: (L (domain (restr g j)) (fun z : Set => ordinal_o (V z (restr g j)))
  = (restr g1 j)).
  rewrite /g1; apply fgraph_exten.
    - gprops.
    - apply restr_fgraph; gprops.
    - bw; rewrite -jd restr_domain1 //; gprops; bw.
    - bw; rewrite -jd => x xd; bw; [ by apply jg |gprops].
have dg1: domain g1 = domain g by rewrite /g1; bw.
apply one_unit_prod_ord1.
    split; first by exact.
    split; first by ue.
    split; first rewrite /g1; gprops.
    rewrite dg1; move=> i idg; rewrite /g1; bw.
    apply (ordinal_p11 (albo _ idg)).
  ue.
rewrite dg1; move=> i ic.
rewrite /g1; bw; last by move: ic; srw; move => [ok _].
rewrite (alz _ ic) (ordinal_p7 ordinal_1).
by exists emptyset.
Qed.

Lemma unit_helper: forall x y j,
  let g := (variantLc x y) in
    let r := canonical_doubleton_order in
      is_ordinal x -> is_ordinal y -> sub j (domain g) ->
      (worder r & substrate r = domain g & fgraph g
        & (forall i, inc i (domain g) -> is_ordinal (V i g))
        & worder (induced_order r j)
        & substrate (induced_order r j) = j
        & substrate (induced_order r j) = domain (restr g j)
        & fgraph (restr g j)).
Proof.
move=> x y j g r ox oy sj.
have fgg: fgraph g by rewrite /g;fprops.
have dr: domain (restr g j) = j by rewrite restr_domain1.
have wor: worder r by apply worder_canonical_doubleton_order.
have sr: substrate r = domain g.
   by rewrite substrate_canonical_doubleton_order /g; bw.
have sj1: sub j (substrate r) by rewrite sr.
have sj2: substrate (induced_order r j) = j by aw; fprops.
have q4: (forall i : Set, inc i (domain g) -> is_ordinal (V i g)).
  by rewrite /g; bw; move=> i itp; try_lvariant itp.
ee.
- by apply worder_restriction.
- by rewrite sj2 dr.
Qed.

Lemma ord_0_plus_unit_l: forall x, is_ordinal x ->
  0o +o x = x.
Proof.
move=> x ox.
set g := (variantLc 0o x).
have ->: ord_sum2 0o x = ord_sum canonical_doubleton_order g.
  by rewrite /g /ord_sum2 /order_sum2 /ord_sum variantLc_comp.
set j := singleton TPb.
have sj: sub j (domain g) by rewrite /g/j; move=> t; bw; aw; move=>->; fprops.
move: (unit_helper ordinal_0 ox sj)=> [p1 [p2 [p3 [p4 [p5 [p6 [p7 p8]]]]]]].
have p11: (forall i, inc i (complement (domain g) j) -> V i g = 0o).
  move => i; rewrite /g /j; bw; aw;srw; aw; move=> [itp aux].
  by move: aux; move:itp=> [] ->; bw; move=> h; elim h.
rewrite (zero_unit_sum_ord2 p1 p2 p3 p4 sj p11).
have res: V TPb (restr g j) = x by rewrite /g /j; bw; fprops.
rewrite (ord_sum_singleton (e:= TPb)) //; [ fprops | ue ].
Qed.

Lemma ord_0_plus_unit_r: forall x, is_ordinal x ->
  x +o 0o = x.
Proof.
move=> x ox.
set g := (variantLc x 0o).
have ->: ord_sum2 x 0o = (ord_sum canonical_doubleton_order g).
  by rewrite /ord_sum2 /order_sum2 /ord_sum variantLc_comp.
set j := singleton TPa.
have sj: sub j (domain g) by rewrite /g/j; move=> t; bw; aw; move=>->; fprops.
move: (unit_helper ox ordinal_0 sj)=> [p1 [p2 [p3 [p4 [p5 [p6 [p7 p8]]]]]]].
have p11: (forall i, inc i (complement (domain g) j) -> V i g = 0o).
  move => i; rewrite /g /j; bw; aw;srw; aw; move=> [itp aux].
  by move: aux; move:itp=> [] ->; bw; move=> h; elim h.
rewrite (zero_unit_sum_ord2 p1 p2 p3 p4 sj p11).
have res: V TPa (restr g j) = x by rewrite /g/j; bw; fprops.
rewrite (ord_sum_singleton (e:= TPa)) //; [ fprops | ue ].
Qed.

Lemma ord_1_mult_unit_r: forall x, is_ordinal x ->
  x *o 1o = x.
Proof.
move=> x ox.
set g := (variantLc 1o x).
have ->: ord_prod2 x 1o = (ord_prod canonical_doubleton_order g).
  by rewrite /g/ord_prod2 /order_prod2 /ord_prod variantLc_comp.
set j := singleton TPb.
have fs: finite_set (substrate canonical_doubleton_order).
  rewrite substrate_canonical_doubleton_order.
  rewrite -two_points_pr2; apply doubleton_finite.
have sj: sub j (domain g) by rewrite /g/j; move=> t; bw; aw; move=>->; fprops.
move: (unit_helper ordinal_1 ox sj)=>[p1 [p2 [p3 [p4 [p5 [p6 [p7 p8]]]]]]].
have p11: (forall i, inc i (complement (domain g) j) -> V i g = 1o).
  move => i; rewrite /g /j; bw; aw;srw; aw; move=> [itp aux].
  by move: aux; move:itp=> [] ->; bw; move=> h; elim h.
rewrite (one_unit_prod_ord2 p1 p2 p3 p4 fs sj p11).
have res: V TPb (restr g j) = x by rewrite /g/j; bw; fprops.
rewrite (ord_prod_singleton (e:= TPb)) //; [ fprops | ue ].
Qed.

Lemma ord_1_mult_unit_l: forall x, is_ordinal x ->
  1o *o x = x.
Proof.
move=> x ox.
set g := (variantLc x 1o).
have ->: ord_prod2 1o x= (ord_prod canonical_doubleton_order g).
  by rewrite /g /ord_prod2 /order_prod2 /ord_prod variantLc_comp.
set j := singleton TPa.
have fs: finite_set (substrate canonical_doubleton_order).
  rewrite substrate_canonical_doubleton_order.
  rewrite -two_points_pr2; apply doubleton_finite.
have sj: sub j (domain g) by rewrite /g/j; move=> t; bw; aw; move=>->; fprops.
move: (unit_helper ox ordinal_1 sj)=>[p1 [p2 [p3 [p4 [p5 [p6 [p7 p8]]]]]]].
have p11: (forall i, inc i (complement (domain g) j) -> V i g = 1o).
  move => i; rewrite /g /j; bw; aw;srw; aw; move=> [itp aux].
  by move: aux; move:itp=> [] ->; bw; move=> h; elim h.
rewrite (one_unit_prod_ord2 p1 p2 p3 p4 fs sj p11).
have res: V TPa (restr g j) = x by rewrite /g/j; bw; fprops.
rewrite (ord_prod_singleton (e:= TPa)) //; [ fprops | ue ].
Qed.

Lemma order_sum_assoc_iso: forall r g r' g',
  order_sum_a r g -> order_sum_a r' g' ->
  r = order_sum r' g' ->
  let order_sum_assoc_aux :=
    fun l =>
    order_sum (V l g') (L (substrate (V l g')) (fun i => V (J i l) g)) in
  let order_sum_assoc :=
    order_sum r' (L (domain g') order_sum_assoc_aux)
  in order_isomorphism (BL (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=> r g r' g' oa oa' oa_link F G.
move: (oa) => [or [sr [fgg alo]]].
move: (oa') => [or' [sr' [fgg' alo']]].
have alo'' :forall l,
  inc l (substrate r') ->
  order_sum_a (V l g')
  (L (substrate (V l g')) (fun i => V (J i l) g)).
  move=> l ls; red; ee; bw; first by apply alo' =>//; ue.
  move => i isg; bw; apply alo; rewrite -sr oa_link.
  rewrite order_sum_substrate //; apply inc_disjoint_union1 =>// ; ue.
have order_sum_assoc_aux2 :forall l,
  inc l (domain g') -> order (F l).
  move=> l ldg'; rewrite /F; rewrite -sr' in ldg'.
  apply order_sum_order; apply alo'' => //.
have oa'' : order_sum_a r' (L (domain g') (fun l=> F l)).
  by red; bw; ee; move => i idf; bw; apply order_sum_assoc_aux2.
have org : order G by rewrite /G; apply order_sum_order=>//.
have ta: (transf_axioms (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 inc_disjoint_union1; bw.
  rewrite /F;bw; first by apply inc_disjoint_union1; bw; rewrite pQ.
  apply alo''; ue.
set(FF:= BL (fun x => J (J (P x) (P (Q x))) (Q (Q x)))
    (sum_of_substrates g) (substrate G)).
have injF: injection FF.
  apply bl_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 bl_surjective => //.
  move=> y; rewrite /G; bw => yG.
  move: (du_index_pr1 yG); rewrite L_domain=> [[Qd]]; bw; move=> [Py py].
  rewrite sr' in alo''; move: (alo'' _ Qd) => al.
  move: (Py); rewrite /F; bw => paux.
  move: (du_index_pr1 paux);rewrite L_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 inc_disjoint_union1 =>//.
    rewrite -sr oa_link; bw; apply inc_disjoint_union1 =>//.
  by ex_tac; rewrite /x ; aw; rewrite Ppy py.
rewrite /FF;red; rewrite bl_source bl_target; ee; bw.
move=> x y xs ys; rewrite (bl_W ta xs) (bl_W ta ys).
set gx := (J (J (P x) (P (Q x))) (Q (Q x))).
set gy := (J (J (P y) (P (Q y))) (Q (Q y))).
rewrite /G (order_sum_gle oa) (order_sum_gle oa'').
set P1:=inc gx (sum_of_substrates (L (domain g') (fun l : Set => F l))).
set P2:=inc gy (sum_of_substrates (L (domain g') (fun l : Set => F l))).
rewrite /gx /gy /order_sum_r ! pr1_pair ! pr2_pair.
rewrite oa_link; rewrite {1} /glt (order_sum_gle oa') /order_sum_r.
move: (du_index_pr1 xs)(du_index_pr1 ys) => [Qu [Pu pu]][Qv [Pv pv]].
move: Qu Qv;rewrite -sr oa_link (order_sum_substrate 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.
have p1p: P1.
  rewrite /P1; apply inc_disjoint_union1; bw.
  have Qs: inc (Q (Q x)) (substrate r') by ue.
  rewrite /F; bw; try apply alo'' =>//.
  apply inc_disjoint_union1; [ rewrite L_domain // | bw; ue].
have p2p: P2.
  rewrite /P2; apply inc_disjoint_union1; bw.
  have Qs: inc (Q (Q y)) (substrate r') by ue.
  rewrite /F; bw; try apply alo'' =>//.
  apply inc_disjoint_union1; [ rewrite L_domain // | bw; ue].
apply iff_eq.
  have aux1: inc (Q (Q x)) (substrate r') by ue.
  move: (alo'' _ aux1) => aux2.
  move=> hyp; eee; move: hyp => [_ [_ aux]]; case aux.
    move=> [[Qx1 [Qx2 hr]] nxy]; case hr; first by auto.
    move => [aa bb]; right; eee; bw; rewrite /F order_sum_gle //.
    eee.
        apply inc_disjoint_union1; bw; ue.
      rewrite aa;apply inc_disjoint_union1; bw; ue.
   red; rewrite !pr2_pair (L_V_rw _ PQx) !pr1_pair aux3.
   case (equal_or_not (P (Q x)) (P (Q y)))=> aux5; last by left;split.
   elim nxy; rewrite -aux3 -aux4 aa aux5 //.
  move=> [sq le1]; right;rewrite - sq; ee.
  bw;rewrite /F order_sum_gle //.
  eee.
      apply inc_disjoint_union1; bw; ue.
    rewrite sq;apply inc_disjoint_union1; bw; ue.
  red; rewrite !pr2_pair (L_V_rw _ PQx) !pr1_pair aux3; intuition.
move=> [_ [_ aux]]; ee; case aux.
  move=> lt; left; ee.
  move:lt => [_ ne]; dneg ne1; ue.
move=> [qq]; bw.
have Qs: inc (Q (Q x)) (substrate r') by ue.
rewrite /F (order_sum_gle (alo'' _ Qs)).
move=> [p1 [p2]]; rewrite /order_sum_r !pr1_pair !pr2_pair.
case; move => [hyp1 hyp2].
  have aux2: Q x <> Q y by dneg ne1; ue.
  left; ee.
right; ee; first by apply pair_exten =>//.
by move: hyp2; bw;rewrite pqu.
Qed.

Lemma order_prod_assoc_iso: forall r g r' g',
  order_prod_a r g -> order_sum_a r' g' ->
  r = order_sum r' g' ->
  worder r' ->
  (forall i, inc i (domain g') -> worder( V i g')) ->
  let order_sum_assoc_aux :=
    fun l =>
    order_prod (V l g') (L (substrate (V l g')) (fun i => V (J i l) g)) in
  let ordinal_prod_assoc :=
    order_prod r' (L (domain g') order_sum_assoc_aux)
  in order_isomorphism (BL
     (fun z => L (domain g') (fun l =>
       L (substrate (V l g')) (fun j => V (J j l) z)))
      (prod_of_substrates g) (substrate (ordinal_prod_assoc)))
  (order_prod r g) (ordinal_prod_assoc).
Proof.
move=> r g r' g' la oa oa_link wor' alwo F G.
move: (oa) => [or' [sr' [fgg' alo']]].
move: (la) => [wor [sr [fgg alo]]].
have dgpr: forall i j, inc i (domain g') -> inc j (substrate (V i g')) ->
   inc (J j i) (domain g).
  move=> i j id jd; rewrite -sr oa_link; bw; apply inc_disjoint_union1 =>//.
have la1: forall i, inc i (domain g') ->
   order_prod_a (V i g')
     (L (substrate (V i g')) (fun i0 : Set => V (J i0 i) g)).
   move=> i idg; red;red; ee;bw; move=> j js; bw; apply alo; apply dgpr =>//.
have la': order_prod_a r' (L (domain g') F).
  by red; red;ee;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 (L (domain g') (fun i => substrate (F i))).
  rewrite /G; bw; rewrite /prod_of_substrates /fam_of_substrates; bw.
  apply f_equal; apply L_exten1 =>//; move=> i idg; bw.
have sG0: substrate G = (prod_of_substrates (L (domain g') F)).
  rewrite /G lexorder_substrate // /prod_of_substrates /fam_of_substrates; bw.
have sG2: substrate G = productb
      (L (domain g') (fun i => productb
        (L (substrate (V i g'))(fun i0 : Set => substrate (V (J i0 i) g))))).
  rewrite sG1; apply f_equal; apply L_exten1 =>//.
  move=> i idg; rewrite /F;bw; last by apply la1 =>//.
  rewrite /prod_of_substrates /fam_of_substrates; bw.
  apply f_equal; apply L_exten1 =>//; move=> x xs; bw.
have g1: fgraph (L (domain g) (fun i => substrate (V i g))) by gprops.
have g2: fgraph (L (domain g') (fun i=> substrate (V i (L (domain g') F))))
  by gprops.
set h := (fun z => L (domain g') (fun l =>
     L (substrate (V l g')) (fun j => V (J j l) z))).
have p1: forall z, inc z (prod_of_substrates g) -> inc (h z) (substrate G).
  move=> z zp; move: (zp).
  rewrite /prod_of_substrates /fam_of_substrates; aw; bw.
  move=> [fgz [dz iVV]]; rewrite dz in iVV.
  rewrite sG2 /h; rewrite productb_rw ; last by gprops.
  split; first (by gprops); split; bw.
  move=> i idg; bw; aw; ee; gprops; bw; move=> j js; bw.
  move: (dgpr _ _ idg js) => aux; move: (iVV _ aux); bw; gprops.
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; rewrite /prod_of_substrates /fam_of_substrates; aw; bw.
  rewrite /h; move=> [fga [da iVVa]][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 (V (Q x)) eqn); bw => eq2.
  by move: (f_equal (V (P x)) eq2); bw; rewrite px.
have p3: forall x, inc x (substrate G) -> exists z,
  (inc z (prod_of_substrates g) & (h z) = x).
  move=> x;rewrite sG2.
  aw; bw; last (by gprops); move=> [fgx [dx iVVx]].
  exists (L (domain g) (fun w => V (P w) (V (Q w) x))); split.
    have aux: product_order_axioms g by red; ee.
    aw; ee; bw; move=> i idg; bw.
    move : idg; rewrite -sr oa_link; bw => xsr.
    move: (du_index_pr1 xsr) => [Qx [Px px]].
    rewrite dx in iVVx; move: (iVVx _ Qx); bw.
    rewrite productb_rw; last by gprops.
    bw; move=> [fg1 [d1 ivv1]];rewrite d1 in ivv1;move: (ivv1 _ Px); bw.
    by have ->: J (P i) (Q i) = i by aw.
  rewrite /h; apply fgraph_exten =>//;[ gprops | bw; ue | bw].
  move=> j jdg; bw; rewrite dx in iVVx; move: (iVVx _ jdg); bw; aw; bw.
    move=> [fgj [dj iVV2]]; apply fgraph_exten; [ gprops | exact | bw; ue | bw].
    move=> w ws; bw; [ aw | apply dgpr =>//].
  gprops.
red; ee; aw.
  apply bl_bijective; ee.
move=> a b ap bp.
rewrite order_prod_gle // order_prod_gle //.
rewrite bl_W // bl_W //.
set P1:= inc (h a) _; set P2:= inc (h b) _.
have P1p: P1 by rewrite /P1; move: (p1 _ ap); rewrite sG0 //.
have P2p: P2 by rewrite /P2; move: (p1 _ bp); rewrite sG0 //.
apply iff_eq; move=> [p4 [p5 cmp]]; eee.
  case cmp; 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; split.
    have paux: forall c, inc c (prod_of_substrates g) ->
      inc (V (Q j) (h c)) (prod_of_substrates
        (L (substrate (V (Q j) g')) (fun i : Set => V (J i (Q j)) g))).
      move=> i ic;move: (p1 _ ic); rewrite sG1.
      rewrite productb_rw; last by gprops.
      bw;move=> [fgh [dh ivv]]; rewrite dh in ivv; move: (ivv _ Qx); bw.
      rewrite /F lexorder_substrate //; apply la1 => //.
    bw; rewrite /F ;split.
      rewrite order_prod_gle //; last (by apply la1); ee.
      right; ex_tac; bw; split.
        rewrite /h; bw; by have ->: (J (P j) (Q j)) = j by aw.
      move=> i [ile ne].
      have isr: inc i (substrate (V (Q j) g')) by order_tac.
      rewrite /h; bw; apply jle; split; last by dneg aa; rewrite -aa; aw.
      rewrite oa_link order_sum_gle //; ee.
        apply inc_disjoint_union1=> //.
      red; eee; rewrite !pr1_pair !pr2_pair;right ; intuition.
    rewrite /h; bw; dneg aa; move: (f_equal (V (P j)) aa);bw.
    rewrite px //.
  move=> i ilt.
  have idg: inc i (domain g') by rewrite -sr'; order_tac.
  rewrite /h; bw; apply L_exten1 =>// k ks.
  apply jle; split; last by move: ilt => [_ bad]; dneg aa; rewrite -aa; aw.
  rewrite oa_link order_sum_gle //; ee.
    apply inc_disjoint_union1=> //.
  red; aw; intuition.
case cmp; 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; rewrite order_prod_gle //; last by apply la1.
move=> [p6 [p7]];case; first by move=> p8; elim ns.
move=> [k [ks [klt kle]]].
rewrite sr; move: (dgpr _ _ jsr ks) => pd.
ex_tac; split; 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: (order_sum_gle1 oa lti); aw; case => ch.
  move: (jle _ ch); rewrite /h; bw => eq1.
  by move: (f_equal (V (P i)) eq1); bw; rewrite pi.
move: ch => [Qi aux].
have ->: i = J (P i) j by rewrite -Qi; aw.
have aux2: glt (V j g') (P i) k.
   rewrite -Qi; split => //; dneg aa; rewrite -aa - Qi pi; aw.
rewrite Qi in Psg'; move: (kle _ aux2); bw.
Qed.

Lemma order_sum_assoc1: forall r g r' g',
  worder r -> substrate r = domain g ->
  fgraph g -> (forall i, inc i (domain g) -> is_ordinal (V i g)) ->
  worder r' -> substrate r' = domain g' ->
  fgraph g' -> (forall i, inc i (domain g') -> worder (V i g')) ->
  r = order_sum r' g' ->
  let order_sum_assoc_aux :=
    fun l =>
    ord_sum (V l g') (L (substrate (V l g')) (fun i => V (J i l) g)) in
  ord_sum r g = ord_sum r' (L (domain g') (order_sum_assoc_aux)).
Proof.
move=> r g r' g' wor sr fgf alB wor' sr' fgf' alw oal osa.
rewrite /ord_sum.
have oa': order_sum_a r' g' by red; ee.
apply ordinal_p8.
    apply order_sum_worder => //; [ bw | gprops | bw].
    by move=> i idg; bw; apply ordinal_p10; apply alB.
  apply order_sum_worder => //; [ bw | gprops | bw ].
  move=> i idg'; bw; apply ordinal_p10.
  rewrite /osa; apply ord_sum_ordinal => //; [ by apply alw | bw | gprops| bw].
  move => j js; bw; apply alB; rewrite -sr oal (order_sum_substrate oa').
  by apply inc_disjoint_union1.
set g'' := (L (domain g) (fun z => ordinal_o (V z g))).
have oa: order_sum_a r g''.
  rewrite /g'';red; bw;ee; move=> i idg; bw.
  apply (ordinal_p11 (alB _ idg)).
move: (order_sum_assoc_iso oa oa' oal) => /=.
set aux' := fun l =>
    order_sum (V l g') (L (substrate (V l g')) (fun i => V (J i l) g'')).
set f:= BL _ _ _.
move => oi1; move: (oi1) => [o1 [o2 _]].
apply orderIT with (order_sum r' (L (domain g') aux')); first by exists f; ee.
apply ord_sum_invariant2 =>//; bw; gprops; first by 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 L_exten1 => //;move=> j js.
  have pd: inc (J j i) (domain g).
    by rewrite -sr oal (order_sum_substrate oa'); by apply inc_disjoint_union1.
  rewrite /g''; bw.
apply ordinal_p2.
rewrite /s.
apply order_sum_worder; [by apply alw | bw | gprops | bw ].
move=> j js; bw; apply ordinal_p10; apply alB.
rewrite -sr oal (order_sum_substrate oa'); by apply inc_disjoint_union1.
Qed.

Lemma ordinal_prod_assoc1: forall r g r' g',
  worder r -> substrate r = domain g ->
  fgraph g -> (forall i, inc i (domain g) -> is_ordinal (V i g)) ->
  worder r' -> substrate r' = domain g' ->
  fgraph g' -> (forall i, inc i (domain g') -> worder (V i g')) ->
  r = order_sum r' g' ->
  finite_set (substrate r) ->finite_set (substrate r') ->
  (forall i, inc i (domain g') -> finite_set (substrate (V i g'))) ->
  let order_prod_assoc_aux :=
    fun l =>
    ord_prod (V l g') (L (substrate (V l g')) (fun i => V (J i l) g)) in
  ord_prod r g = ord_prod r' (L (domain g') order_prod_assoc_aux).
Proof.
move=> r g r' g' wor sr fgf alB wor' sr' fgf' alw oal fs fs' alfs osa.
rewrite /ord_prod.
have oa': order_sum_a r' g' by red; ee; red; ee.
apply ordinal_p8.
    apply order_prod_worder => //; [ bw | gprops | bw].
    by move=> i idg; bw; apply ordinal_p10; apply alB.
  apply order_prod_worder => //; [ bw | gprops | bw ].
  move=> i idg'; bw; apply ordinal_p10.
  rewrite /osa; apply ord_prod_ordinal; [ by apply alw | bw | gprops| bw |].
    move => j js; bw; apply alB; rewrite -sr oal (order_sum_substrate oa').
    by apply inc_disjoint_union1.
  by apply alfs.
set g'' := (L (domain g) (fun z => ordinal_o (V z g))).
have oa: order_prod_a r g''.
  rewrite /g'';red; red; bw;ee; move=> i idg; bw.
  apply (ordinal_p11 (alB _ idg)).
move: (order_prod_assoc_iso oa oa' oal wor' alw) => /=.
set aux' := fun l =>
    order_prod (V l g') (L (substrate (V l g')) (fun i => V (J i l) g'')).
set f:= BL _ _ _.
move => oi1; move: (oi1) => [o1 [o2 _]].
apply orderIT with (order_prod r' (L (domain g') aux'));
    first by exists f; ee.
apply ord_prod_invariant2 =>//; bw; gprops.
rewrite sr';move=> i isr; bw; rewrite /osa /ord_prod; bw.
set s:= order_prod _ _.
have -> : (aux' i = s).
  rewrite /aux' /s; apply f_equal.
  apply L_exten1 => //;move=> j js.
  have pd: inc (J j i) (domain g).
    by rewrite -sr oal (order_sum_substrate oa'); by apply inc_disjoint_union1.
  rewrite /g''; bw.
apply ordinal_p2.
rewrite /s.
apply order_prod_worder; [by apply alw | bw | gprops | bw | fprops].
move=> j js; bw; apply ordinal_p10; apply alB.
rewrite -sr oal (order_sum_substrate oa'); by apply inc_disjoint_union1.
Qed.

Lemma order_sum_assoc2: forall a b c,
  order a -> order b -> order c ->
  (order_sum2 a (order_sum2 b c))
  \Is (order_sum2 (order_sum2 a b) c).
Proof.
move=> a b c oa ob oc.
have oab: order (order_sum2 a b) by apply order_sum2_order.
have obc: order (order_sum2 b c) by apply order_sum2_order.
set E:= substrate (order_sum2 a (order_sum2 b c)).
set F:= substrate (order_sum2 (order_sum2 a b) c).
set A:= substrate a; set B := substrate b; set C := substrate c.
have Ev: E = canonical_du2 A (canonical_du2 B C).
  by rewrite /E ! order_sum2_substrate.
have Fv: F = canonical_du2 (canonical_du2 A B) C.
  by rewrite /F ! order_sum2_substrate.
move: two_points_distinctb => nT.
move: two_points_distinct => nT1.
set f := fun z => Yo (Q z = TPa) (J (J (P z) TPa) TPa)
          (Yo (Q (P z) = TPa) (J (J (P (P z)) TPb) TPa) (J (P (P z)) TPb)).
have p1: forall x, inc x E -> inc (f x) F.
  move => x; rewrite Ev Fv ! canonical_du2_pr.
  move=> [px]; case.
   move=> [PA Qa]; rewrite /f; Ytac0; split;first by fprops.
   aw; ee.
  move=> [[pPx alt] Qb].
  have nQa: Q x <> TPa by rewrite Qb.
  rewrite /f; Ytac0.
  case alt;move => [Ppx Qpx]; first by Ytac0; aw; ee.
  rewrite (Y_if_not_rw); aw; ee; rewrite Qpx //.
have p2: forall y, inc y F -> exists x, (inc x E & f x = y).
  move => y; rewrite Ev Fv ! canonical_du2_pr; move=> [py]; case.
    move=> [[pPy aux] Qpy]; case aux.
      move=> [PPa QP]; exists (J (P (P y)) TPa); split.
        rewrite canonical_du2_pr;aw; ee.
      rewrite /f pr2_pair; Ytac0; aw.
      apply pair_exten =>//; fprops; aw; try ue.
    move=> [PPy QPy]; exists (J (J (P (P y)) TPa) TPb); split.
      rewrite ! canonical_du2_pr;aw; ee.
    rewrite /f !(pr1_pair, pr2_pair); Ytac0; Ytac0.
    apply pair_exten =>//; fprops; aw; try ue.
  move=> [Py Qy]; exists (J (J (P y) TPb) TPb); split.
   rewrite ! canonical_du2_pr;aw; ee.
   rewrite /f !(pr2_pair, pr1_pair); Ytac0; Ytac0.
   apply pair_exten =>//;fprops; aw;ue.
have p3: forall x y, inc x E -> inc y E -> f x = f y -> x = y.
  move => x y; rewrite Ev ! canonical_du2_pr /f.
  move => [px hx][py hy].
  case hx.
    move => [PxA Qxa]; Ytac0.
    case hy.
      move => [PyA Qya]; Ytac0 => sf; move:(pr1_def sf).
      by rewrite - {1} Qxa - Qya px py.
    move=> [_ ] Qy; rewrite Qy; Ytac0; Ytac h1.
      move => h2;elim nT1; exact: (pr2_def(pr1_def h2)).
       move => h2;elim nT1; exact: (pr2_def h2).
   move=> [[pPx auxx] Qx]; rewrite Qx; Ytac0.
   case hy.
     move=> [_ Qy]; Ytac0; Ytac h.
       move => h2;elim nT; exact: (pr2_def(pr1_def h2)).
     move => h2;elim nT; exact: (pr2_def h2).
  move=> [[pPy auxy] Qy]; rewrite Qy; Ytac0.
  case auxx; move=> [PPx Qpx].
    Ytac0.
      case auxy; move=> [PPy Qpy].
         Ytac0 => sf; move: (pr1_def (pr1_def sf)) => sf1.
         apply pair_exten =>//; try ue.
         apply pair_exten =>//; try ue.
    rewrite Qpy;Ytac0=> sf; elim nT1; exact: (pr2_def sf).
  case auxy; move=> [_ Qpy].
     rewrite Qpx Qpy; Ytac0; Ytac0 => sf; elim nT; exact: (pr2_def sf).
  rewrite Qpx Qpy; Ytac0; Ytac0.
  move=> sf; move: (pr1_def sf) => sf1.
  apply pair_exten =>//; try ue.
  apply pair_exten =>//; try ue.
exists (BL f E F); red; ee; aw.
  apply bl_bijective => //.
move=> x y xE yE;
rewrite bl_W // bl_W// ! order_sum2_gle // !order_sum2_substrate //.
rewrite -/A -/B -/C - Ev -Fv.
apply iff_eq.
  move=> [_ [_ hyp]]; split; first by apply (p1 _ xE).
  split; first by apply (p1 _ yE).
  move: xE; rewrite Ev canonical_du2_pr; move=> [px hx].
  move: yE; rewrite Ev canonical_du2_pr; move=> [py hy].
  case hyp.
    move=> [Qx [Qy le]]; left; rewrite /f (Y_if_rw Qx) (Y_if_rw Qy).
    rewrite ! pr1_pair ! pr2_pair.
    split ; first (by []);split ; first (by []).
    split.
       case hx; move => [hxa hxb].
         rewrite canonical_du2_pr; aw; split; [fprops | left ; split =>//].
         elim nT; by rewrite -Qx -hxb.
    split.
       case hy; move => [hxa hxb].
         rewrite canonical_du2_pr; aw; split; [fprops | left ; split =>//].
         elim nT; by rewrite -Qy -hxb.
    by left; split; [| split ].
  case; last first.
    move=> [Qxa Qyb].
    have fx: f x = (J (J (P x) TPa) TPa) by rewrite /f Y_if_rw //.
    rewrite fx ! pr1_pair ! pr2_pair.
    case hy; first by move=> [_ bad]; contradiction.
    move=> [Py Qy].
    have: f y = (Yo (Q (P y) = TPa)(J (J (P (P y)) TPb) TPa) (J (P (P y)) TPb)).
      by rewrite /f Y_if_not_rw //.
     move: Py; rewrite canonical_du2_pr; move=> [pPy]; case.
       move=> [PPy QPy]; rewrite QPy; Ytac0 => ->.
        rewrite ! pr1_pair ! pr2_pair; left; split => //; split => //.
       split.
         rewrite canonical_du2_pr //; aw; split; first by fprops.
         left; split =>//; case hx; first by move => [pa ].
         by rewrite Qxa; move=> [_ bad]; elim nT.
       split.
         rewrite canonical_du2_pr //; aw; split; fprops.
      right; right; split =>//.
     move=> [PPy QPy]; rewrite QPy; Ytac0 => ->.
     rewrite ! pr1_pair ! pr2_pair; right; right; split =>//.
  move=> [Qx [Qy [Px [Py aux]]]].
  have: f y=(Yo (Q (P y) = TPa) (J (J (P (P y)) TPb) TPa) (J (P (P y)) TPb)).
    by rewrite /f Y_if_not_rw //.
  have: f x = (Yo (Q (P x) = TPa)(J (J (P (P x)) TPb) TPa) (J (P (P x)) TPb)).
    by rewrite /f Y_if_not_rw //.
  case aux.
    move=> [QPx [QPy le]]; rewrite QPx QPy; Ytac0; Ytac0 => -> ->.
    rewrite !(pr1_pair, pr2_pair).
    left; split ; first (by []);split ; first (by []).
    split.
      rewrite canonical_du2_pr; aw; split; [ fprops | right ; split => // ].
      move: Px; rewrite canonical_du2_pr; move=> [pPx]; case.
       by move => [ok _].
       by rewrite QPx; move=> [_ bad]; elim nT.
    split.
      rewrite canonical_du2_pr; aw; split; [ fprops | right ; split => // ].
      move: Py; rewrite canonical_du2_pr; move=> [pPx]; case.
       by move => [ok _].
       by rewrite QPy; move=> [_ bad]; elim nT.
    right; left; split; [exact | split ; exact].
  case.
    move => [QPx [QPy le]]; Ytac0; Ytac0 => -> ->.
    right; left; aw; split; [exact | split ; exact].
  move => [QPx QPy];Ytac0; Ytac0 => -> ->.
  by right; right; aw; split.
move=> [fxF [fyF hyp]].
split; first (by exact); split; first (by exact).
move: xE; rewrite Ev canonical_du2_pr; move=> [px hx].
move: yE; rewrite Ev canonical_du2_pr; move=> [py hy].
case hx; move => [Px Qx].
   have fx: f x = (J (J (P x) TPa) TPa) by rewrite /f Y_if_rw.
   case hy; move => [Py Qy].
     have fy: f y = (J (J (P y) TPa) TPa) by rewrite /f Y_if_rw.
     left; split; first (by exact); split; first (by exact).
     case hyp.
       move=> [_ [_ [pc [pd]]]]; case.
          by rewrite fx fy; aw; move=> [_ [_ res]].
       case.
         by move=> [_ [bad _]];move: bad; rewrite fy; aw.
         by move=> [_ bad];move: bad; rewrite fy; aw.
      case. by move=> [_ [bad _]];move: bad; rewrite fy; aw.
      by move=> [_ bad];move: bad; rewrite fy; aw.
    right; right; rewrite Qx Qy; split; exact.
  right; left; split; first by ue.
have fx: f x = (Yo (Q (P x) = TPa) (J (J (P (P x)) TPb) TPa) (J (P (P x)) TPb)).
   rewrite /f Y_if_not_rw //; last by ue.
case hy; move => [Py Qy].
  have fy: f y = (J (J (P y) TPa) TPa) by rewrite /f Y_if_rw.
  elim nT; case hyp.
    move=> [Qfx [Qfy [Pfx [Pfy aux]]]].
    have aux2: Q (P (f y)) = TPa by rewrite fy; aw.
    rewrite aux2 in aux; case: aux; last first.
      by case => [ [_ [bad _]] | [_ bad]]; elim bad.
    move=> [h1 _].
    move: fx; Ytac aux3 => fx; [ move: h1 | move: Qfx ]; rewrite fx; aw.
  by rewrite fy; aw; case => [ [_ [bad _]] | [_ bad]]; elim bad.
have fy: f y = (Yo (Q (P y) = TPa) (J (J (P (P y)) TPb) TPa) (J (P (P y)) TPb)).
   rewrite /f Y_if_not_rw //; last by ue.
   split; first (by ue); split; first (by exact);split; first by exact.
move: Px; rewrite canonical_du2_pr; move=> [pPx hpx].
move: Py; rewrite canonical_du2_pr; move=> [pPy hpy].
move: fx; case hpx; move => [_ QPx]; rewrite QPx;Ytac0 => fx.
  move: fy;case hpy; move => [_ QPy]; rewrite QPy; Ytac0 => fy.
    left;eee; case hyp.
      move => [h1 [h2 [h3 [h4]]]]; rewrite fx fy !pr1_pair !pr2_pair.
      case; first by move=> [bad _]; elim nT.
      case; first by move=> [_ [_ ok]].
      by move=> [bad _]; elim nT.
    rewrite fx fy !pr1_pair !pr2_pair.
    case; first by move=> [bad _]; elim bad.
    by move=> [_ bad]; elim bad.
  right; right;split => //.
right; left;split; first by exact.
case hyp; first by move => [h1 _]; rewrite fx in h1; awi h1; contradiction.
rewrite fx !pr1_pair !pr2_pair.
move: fy; case hpy; move => [_ QPy]; rewrite QPy; Ytac0; move=> ->.
  by rewrite !pr1_pair !pr2_pair; case => [ [_ [bad _]] | [_ bad]]; elim bad.
case; first by move=> [_ [_ ok]]; split => //; move: ok; aw.
by move=> [bad _]; elim bad.
Qed.

Lemma order_prod_assoc2: forall a b c,
  order a -> order b -> order c ->
  (order_prod2 a (order_prod2 b c))
  \Is (order_prod2 (order_prod2 a b) c).
Proof.
move=> a b c oa ob oc.
have oab: order (order_prod2 a b) by apply order_prod2_order.
have obc: order (order_prod2 b c) by apply order_prod2_order.
set E:= substrate (order_prod2 a (order_prod2 b c)).
set F:= substrate (order_prod2 (order_prod2 a b) c).
set A:= substrate a; set B := substrate b; set C := substrate c.
have Ev: E = product2 (product2 C B) A.
  by rewrite /E ! order_prod2_substrate.
have Fv: F = product2 C (product2 B A).
  by rewrite /F ! order_prod2_substrate.
have CB_pr: forall z, inc z (product2 C B) =
   (fgraph z & domain z = two_points & inc (V TPa z) C & inc (V TPb z) B).
   by move=> z; rewrite product2_rw.
have BA_pr: forall z, inc z (product2 B A) =
   (fgraph z & domain z = two_points & inc (V TPa z) B & inc (V TPb z) A).
   by move=> z; rewrite product2_rw.
have Ep: forall z, inc z E =
    (fgraph z & domain z = two_points &
       (fgraph (V TPa z) & domain (V TPa z) = two_points &
        inc (V TPa (V TPa z)) C & inc (V TPb (V TPa z)) B) & inc (V TPb z) A).
   by move=> z; rewrite Ev product2_rw CB_pr; ee.
have Fp: forall z, inc z F =
    (fgraph z & domain z = two_points & inc (V TPa z) C &
       (fgraph (V TPb z) & domain (V TPb z) = two_points &
        inc (V TPa (V TPb z)) B & inc (V TPb (V TPb z)) A)).
    move=> z; rewrite Fv product2_rw BA_pr; ee.
set f := fun z => variantLc (V TPa (V TPa z))
     (variantLc (V TPb (V TPa z)) (V TPb z)).
have p1: forall x, inc x E -> inc (f x) F.
  move=> x; rewrite Ep Fp; move => [fgx [dx [[fgx1 [dx1 [xc xb]]] xa]]].
  rewrite /f; ee; bw; fprops.
have p2: forall x y, inc x E -> inc y E -> f x = f y -> x = y.
   move=> x y; rewrite Ep; move => [fgx [dx [[fgx1 [dx1 [xc xb]]] xa]]].
   rewrite /f Ep; move => [fgy [dy [[fgy1 [dy1 [yc yb]]] ya]]] sf.
   move: (f_equal (V TPa) sf) (f_equal (V TPb) sf); bw => sf1 sf2.
   move: (f_equal (V TPa) sf2) (f_equal (V TPb) sf2); bw => sf3 sf4.
   apply fgraph_exten =>//; try ue.
   rewrite dx; move=> z zdx; try_lvariant zdx.
   apply fgraph_exten =>//; try ue.
   rewrite dx1; move=> zz zdx; try_lvariant zdx.
have p3: forall y, inc y F -> exists x, (inc x E & f x = y).
  move=> y; rewrite Fp; move => [fgx [dx [xc [fgx1 [dx1 [xb xba]]]]]].
  exists (variantLc (variantLc (V TPa y) (V TPa (V TPb y)))
       (V TPb (V TPb y))).
  split; first by rewrite Ep;ee; bw; fprops.
  rewrite /f; apply fgraph_exten => //; bw; [fprops | by symmetry | ].
  move=> x xtp; try_lvariant xtp.
  apply fgraph_exten => //; bw ; [fprops | by symmetry | ].
  move=> z xtp; try_lvariant xtp.
exists (BL f E F); red;ee; aw.
  apply bl_bijective => //.
move=> x y xE yE; aw.
rewrite order_prod2_gle // /glt.
rewrite order_prod2_gle // order_prod2_gle //.
rewrite order_prod2_gle // order_prod2_substrate //.
rewrite order_prod2_substrate //.
rewrite -/A -/B -/C -Ev -Fv.
apply iff_eq.
  move: (p1 _ xE)(p1 _ yE) => xF yF.
  move=> [_ [_ aux]]; split; first (by exact) ;split; first by exact.
  move: xF; rewrite Fp; move => [fgx [dx [xc [fgx1 [dx1 [xb xba]]]]]].
  move: yF; rewrite Fp; move => [fgy [dy [yc [fgy1 [dy1 [yb yba]]]]]].
  have x1: inc (V TPb (f x)) (product2 B A) by rewrite BA_pr; ee.
  have y1: inc (V TPb (f y)) (product2 B A) by rewrite BA_pr; ee.
  set hi1:= inc (V TPb (f x)) (product2 B A).
  set hi2:= inc (V TPb (f y)) (product2 B A).
  rewrite /f; bw.
  case aux.
    move=> [Va lVb]; left; rewrite Va; ee.
  move=> [[_ [_ aux']] nse]; case aux'.
    move=> [Vaa Vba]; left.
     split; first (by exact);split; first (by exact);split; first (by exact).
     right; split =>//; dneg aux3.
     move: xE; rewrite Ep; move => [_ [_ [[tfgx1 [tdx1 _]]]] _].
     move: yE; rewrite Ep; move => [_ [_ [[tfgy1 [tdy1 _]]]] _].
     apply fgraph_exten =>//; try ue.
     rewrite tdx1; move=> z zd; try_lvariant zd.
  by move=> aux2; right.
move=> aux.
split; first (by exact);split; first by exact.
move: (xE); rewrite Ep; move => [fgx [dx [[fgx1 [dx1 [xc xb]]] xa]]].
move: (yE); rewrite Ep; move => [fgy [dy [[fgy1 [dy1 [yc yb]]] ya]]].
have x1: inc (V TPa x) (product2 C B) by rewrite CB_pr; ee.
have y1: inc (V TPa y) (product2 C B) by rewrite CB_pr; ee.
move: aux => [fxF [fyF]]; case.
  move=> [sVa [fxb [fxa]]].
  move: sVa; rewrite /f; bw => xaa.
  case.
    move=> [sVab le]; left; split =>//.
    apply fgraph_exten => //; first by ue.
    rewrite dx1; move=> z zd; try_lvariant zd.
  move=> [lt2 neq]; right; ee.
  by dneg aux; rewrite aux.
rewrite /f; bw; move=> h; right. ee.
by move: h => [_ ne]; dneg eql; rewrite eql.
Qed.

Lemma order_sum_distributive: forall x y z,
  order x -> order y -> order z ->
  (order_prod2 z (order_sum2 x y))
  \Is (order_sum2 (order_prod2 z x) (order_prod2 z y)).
Proof.
move=> a b c oa ob oc.
move: (order_sum2_order oa ob) => oz.
move: (order_prod2_order oc oa) => op2.
move: (order_prod2_order oc ob) => op1.
move: (order_prod2_order oc oz) => op3.
move:(order_sum2_order op2 op1) => op4.
set (f := fun z => J (variantLc (P (V TPa z)) (V TPb z)) (Q (V TPa z))).
set A := substrate a; set B := substrate b; set C := substrate c.
set E:= substrate (order_prod2 c (order_sum2 a b)).
set F:= substrate(order_sum2 (order_prod2 c a)(order_prod2 c b)).
have Ep: E = product2 (canonical_du2 A B) C.
   rewrite /E order_prod2_substrate // order_sum2_substrate //.
have Fp: F = canonical_du2 (product2 A C)(product2 B C).
  rewrite /F order_sum2_substrate // !order_prod2_substrate //.
have Ev: forall x, inc x E = (fgraph x & domain x = two_points &
    (is_pair (V TPa x) &
     (inc (P (V TPa x)) A & Q (V TPa x) = TPa) \/
     (inc (P (V TPa x)) B & Q (V TPa x) = TPb)) & inc (V TPb x) C).
  by move=> x; rewrite Ep product2_rw canonical_du2_pr.
have Fv: forall x, inc x F = (is_pair x & fgraph (P x) &
    domain (P x) = two_points & inc (V TPb (P x)) C &
    (inc (V TPa (P x)) A & Q x = TPa) \/
    (inc (V TPa (P x)) B & Q x = TPb)).
  move=> x; rewrite Fp canonical_du2_pr ! product2_rw.
  apply iff_eq.
     move=> [px h]; split => //; case h; move=> [[p1 [p2 [p3 p4]]] p5]; ee.
  move=> [p1 [p2 [p3 [p4 p5]]]]; split =>//.
   case p5; move=> [p6 p7]; [left | right]; ee.
have p1: forall x, inc x E -> inc (f x) F.
  move=> x; rewrite Ev; move => [fgx [dx [[px hx] qx]]].
   rewrite /f Fv !pr1_pair !pr2_pair; bw; ee.
have p2: forall x y, inc x E -> inc y E -> f x = f y -> x = y.
  move=> x y; rewrite Ev Ev /f.
  move => [fgx [dx [[px hx] qx]]] [fgy [dy [[py hy] qy]]] sf.
  move: (pr1_def sf)(pr2_def sf) => r1 r2.
  move: (f_equal (V TPa) r1)(f_equal (V TPb) r1); bw; move => [r3 r4].
  apply fgraph_exten =>//; [ ue | rewrite dx; move=> z zd; try_lvariant zd].
  apply pair_exten =>//.
have p3: forall y, inc y F -> exists x, (inc x E & f x = y).
  move=> y; rewrite Fv; move=> [py [fPy [dPy [Vby Vay]]]].
  exists (variantLc (J (V TPa (P y)) (Q y)) (V TPb (P y))).
  split.
    rewrite Ev; bw; rewrite !pr1_pair !pr2_pair; ee.
  rewrite /f; bw;aw; apply pair_exten =>//; [ fprops | aw | aw].
  apply fgraph_exten; [ fprops | exact | by bw | bw].
  move=> x xtp; try_lvariant xtp.
exists (BL f E F); red; ee; aw; first by apply bl_bijective.
move=> x y xE yE; rewrite bl_W // bl_W //.
rewrite order_sum2_gle // ! order_prod2_gle // /glt order_sum2_gle //.
have ->: Q (f x) = Q (V TPa x) by rewrite /f pr2_pair.
have ->: Q (f y) = Q (V TPa y) by rewrite /f pr2_pair.
have ->: V TPa (P (f x)) = P (V TPa x) by rewrite /f; aw; bw.
have ->: V TPa (P (f y)) = P (V TPa y) by rewrite /f; aw; bw.
have ->: V TPb (P (f x)) = V TPb x by rewrite /f; aw; bw.
have ->: V TPb (P (f y)) = V TPb y by rewrite /f; aw; bw.
have pa: is_pair (V TPa x) by move: xE; rewrite Ev; move => [_ [_[[ px _]]]].
have pb: is_pair (V TPa y) by move: yE; rewrite Ev; move => [_ [_[[ px _]]]].
apply iff_eq.
  move => [_ [_ h]].
  split; first by move: (p1 _ xE); rewrite /F order_sum2_substrate.
  split; first by move: (p1 _ yE); rewrite /F order_sum2_substrate.
  case h.
    move=> [q1 q2].
    case (equal_or_not (Q (V TPa x)) TPa)=> q3.
      left; rewrite -q1; split; first (by exact); split; first (by exact).
      split.
        rewrite product2_rw; rewrite /f pr1_pair; bw.
        move: xE; rewrite Ev; move=> [fgx [dx [[px hx] qx]]].
        case hx; move=> [q4 q5].
          by split; [fprops | split; [trivial | split]].
        by rewrite q3 in q5; elim two_points_distinct.
        split.
        rewrite product2_rw; rewrite /f pr1_pair; bw.
        move: yE; rewrite Ev; move=> [fgx [dx [[px hx] qx]]].
        rewrite q1 in q3; rewrite q3 in hx; case hx; move=> [q4 q5].
          by split; [fprops | split; [trivial | split]].
        by elim two_points_distinct.
      left; split =>//.
    right; left; split; first (by exact); split; first (by ue).
    split.
        rewrite product2_rw; rewrite /f pr1_pair; bw.
        move: xE; rewrite Ev; move=> [fgx [dx [[px hx] qx]]].
        case hx; move=> [q4 q5]; first by rewrite q5 in q3; elim q3.
        by split; [fprops | split; [trivial | split]].
    split.
        rewrite product2_rw; rewrite /f pr1_pair; bw.
        move: yE; rewrite Ev; move=> [fgx [dx [[px hx] qx]]].
        case hx; move=> [q4 q5]; first by rewrite -q1 in q5; contradiction.
        by split; [fprops | split; [trivial | split]].
    left; rewrite -q1; split =>//.
  case.
    move=> [_ [_ h1]] h2; case h1.
      move=> [q1 [q2 q3]]; left.
      split; [exact | split ; [exact | ]].
      split.
        rewrite product2_rw; rewrite /f pr1_pair; bw.
        move: xE; rewrite Ev; move=> [fgx [dx [[px hx] qx]]].
        case hx; move=> [q4 q5]; last by elim two_points_distinct; ue.
        by split; [fprops | split; [trivial | split]].
     split.
        rewrite product2_rw; rewrite /f pr1_pair; bw.
        move: yE; rewrite Ev; move=> [fgx [dx [[px hx] qx]]].
        case hx; move=> [q4 q5]; last by elim two_points_distinct; ue.
        by split; [fprops | split; [trivial | split]].
    right; split => //;dneg aux.
    apply pair_exten => //; ue.
  case.
    move => [q1 [q2 q3]]; right; left.
    split; [exact | split ; [exact | ]].
    split.
        rewrite product2_rw; rewrite /f pr1_pair; bw.
        move: xE; rewrite Ev; move=> [fgx [dx [[px hx] qx]]].
        case hx; move=> [q4 q5]; first by contradiction.
        by split; [fprops | split; [trivial | split]].
     split.
        rewrite product2_rw; rewrite /f pr1_pair; bw.
        move: yE; rewrite Ev; move=> [fgx [dx [[px hx] qx]]].
        case hx; move=> [q4 q5]; first by contradiction.
        by split; [fprops | split; [trivial | split]].
     right; split => //.
     move=> sP; elim h2; apply pair_exten => //.
     move: xE; rewrite Ev; move=> [fgx [dx [[px hx] qx]]].
     case hx; move => [_ Qx]; first (by contradiction); rewrite Qx.
     move: yE; rewrite Ev; move=> [_ [_ [[_ hy] _]]].
     case hy; move => [_ Qy]; first (by contradiction); rewrite Qy.
     done.
  move=> res; right; right; exact.
move => [_ [_ h]].
split; first by move: xE; rewrite /E order_prod2_substrate //.
split; first by move: yE; rewrite /E order_prod2_substrate //.
have pc: inc (V TPa x) (canonical_du2 (substrate a) (substrate b)).
   by move: xE; rewrite Ev canonical_du2_pr; move => [_ [_[px etc]]].
have pd: inc (V TPa y) (canonical_du2 (substrate a) (substrate b)).
   by move: yE; rewrite Ev canonical_du2_pr; move => [_ [_[px etc]]].
case h.
  move=> [q1 [q2 [q3 [q4 aux]]]]; case aux; move=> [q5 q6]; [left | right ].
    split =>//; apply pair_exten =>//; ue.
  split =>//; last by dneg neq; rewrite neq.
  split => //; split => //; left; rewrite q1 q2; split =>//; split =>//.
case.
  move=> [q1 [q2 [q3 [q4 aux]]]]; case aux; move => [q5 q6]; [left | right ].
    split =>//; apply pair_exten =>//; try ue.
    move : xE yE; rewrite ! Ev;move => [_ [_[[_ px] _]]] [_ [_[[_ qx] _]]].
    case px; move=> [_ ppx]; first by contradiction.
    case qx; move=> [_ qpx]; first (by contradiction); ue.
  split =>//; last by dneg neq; rewrite neq.
  split => //; split => //; right; ee.
move=> [q5 q6]; right; split =>//; last by dneg neq;rewrite -neq.
split => //; split => //; right;right; ee.
Qed.

Lemma order_sum_assoc3: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  a +o (b +o c) = (a +o b) +o c.
Proof.
move => a b c oa ob oc.
move: (ord_sum2_ordinal ob oc) => obc.
move: (ord_sum2_ordinal oa ob) => oab.
move: (ordinal_p10 oa) => wa.
move: (ordinal_p10 ob) => wb.
move: (ordinal_p10 oc) => wc.
rewrite/ord_sum2; apply ordinal_p8.
  apply order_sum2_worder; apply ordinal_p10 => //.
  apply order_sum2_worder; apply ordinal_p10 => //.
apply orderIT with
    (order_sum2 (ordinal_o a) (order_sum2 (ordinal_o b) (ordinal_o c))).
  apply ord_sum_invariant4.
    apply orderIR; apply (worder_is_order wa).
  apply orderIS; apply ordinal_p2; apply order_sum2_worder => //.
apply orderIT with
  (order_sum2 (order_sum2 (ordinal_o a) (ordinal_o b))(ordinal_o c)).
apply order_sum_assoc2; fprops.
apply ord_sum_invariant4.
  apply ordinal_p2; apply order_sum2_worder => //.
apply orderIR; apply (worder_is_order wc).
Qed.

Lemma order_prod_assoc3: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  a *o (b *o c) = (a *o b) *o c.
Proof.
move => a b c oa ob oc.
move: (ord_prod2_ordinal ob oc) => obc.
move: (ord_prod2_ordinal oa ob) => oab.
move: (ordinal_p10 oa) => wa.
move: (ordinal_p10 ob) => wb.
move: (ordinal_p10 oc) => wc.
rewrite/ord_prod2; apply ordinal_p8.
  apply order_prod2_worder; apply ordinal_p10 => //.
  apply order_prod2_worder; apply ordinal_p10 => //.
apply orderIT with
 (order_prod2 (ordinal_o a) (order_prod2 (ordinal_o b) (ordinal_o c))).
  apply ord_prod_invariant4.
    apply orderIR; apply (worder_is_order wa).
  apply orderIS; apply ordinal_p2; apply order_prod2_worder => //.
apply orderIT with
  (order_prod2 (order_prod2 (ordinal_o a) (ordinal_o b))(ordinal_o c)).
apply order_prod_assoc2; fprops.
apply ord_prod_invariant4.
  apply ordinal_p2; apply order_prod2_worder => //.
apply orderIR; apply (worder_is_order wc).
Qed.

Lemma order_sum_distributive3: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  c *o (a +o b) = (c *o a) +o (c *o b).
Proof.
move => a b c oa ob oc.
move: (ord_prod2_ordinal oc oa) => obc.
move: (ord_prod2_ordinal oc ob) => ocb.
move: (ord_sum2_ordinal oa ob) => oab.
move: (ordinal_p10 oa) => wa.
move: (ordinal_p10 ob) => wb.
move: (ordinal_p10 oc) => wc.
rewrite/ord_prod2/ord_sum2; apply ordinal_p8.
  apply order_prod2_worder; apply ordinal_p10 => //.
  apply order_sum2_worder; apply ordinal_p10 => //.
apply orderIT with
  (order_prod2 (ordinal_o c) (order_sum2 (ordinal_o a) (ordinal_o b))).
  apply ord_prod_invariant4.
    apply orderIR; apply (worder_is_order wc).
  apply orderIS; apply ordinal_p2; apply order_sum2_worder => //.
apply orderIT with
     (order_sum2
        (order_prod2 (ordinal_o c) (ordinal_o a))
        (order_prod2 (ordinal_o c) (ordinal_o b))).
apply order_sum_distributive; fprops.
apply ord_sum_invariant4.
  apply ordinal_p2; apply order_prod2_worder => //.
apply ordinal_p2; apply order_prod2_worder => //.
Qed.

Lemma ord_zero_absorbing: forall r g,
   order_prod_a r g ->
    (exists i, inc i (domain g) & substrate (V i g) = emptyset)
  -> order_prod r g = emptyset.
Proof.
move=> r g la [j [jdg Vz]].
apply empty_substrate_zero; first by apply order_prod_order.
rewrite lexorder_substrate // /prod_of_substrates /fam_of_substrates.
apply is_emptyset.
move: la => [la1 [la2 [la3 la4]]].
move=> y;aw; last by gprops.
bw; move=> [fgy [dy p]]; rewrite dy in p;move: (p _ jdg); bw.
rewrite Vz=> res; elim (emptyset_pr res).
Qed.

Lemma ord0_prodr: forall x, is_ordinal x ->
  x *o 0o = 0o.
Proof.
move=> x otx; rewrite /ord_prod2 /order_prod2.
move: ordinal_0 => oz.
rewrite ord_zero_absorbing; first by apply ordinal0_pr.
apply order_prod2_axioms; apply ordinal_p11 => //.
exists TPa; bw; ee; rewrite ordinal_p7 => //.
Qed.

Lemma ord0_prodl: forall x, is_ordinal x ->
  0o *o x = 0o.
Proof.
move=> x otx; rewrite /ord_prod2 /order_prod2.
move: ordinal_0 => oz.
rewrite ord_zero_absorbing; first by apply ordinal0_pr.
apply order_prod2_axioms; apply ordinal_p11 => //.
exists TPb; bw; ee; rewrite ordinal_p7 => //.
Qed.

Lemma ord_zero_pr1: forall x, worder x -> ordinal x = 0o
  -> substrate x = emptyset.
Proof.
move=> x wor h; move: (ordinal_p2 wor); rewrite h.
move=> [f [_ [_ [bf [sf [tf _]]]]]].
rewrite (ordinal_p7 ordinal_0) in tf; rewrite sf.
have tf': target f = emptyset by ue.
apply is_emptyset; move=> y ysf.
empty_tac1 (W y f); apply inc_W_target=> //; fct_tac.
Qed.

Lemma ord_prod2_nz: forall a b, is_ordinal a -> is_ordinal b ->
   a <> 0o -> b <> 0o -> a *o b <> 0o.
Proof.
move=> a b oa ob anz bnz pz.
rewrite /ord_prod2 in pz.
have wo: worder (order_prod2 (ordinal_o a) (ordinal_o b)).
  by apply order_prod2_worder; apply ordinal_p10.
move: (ord_zero_pr1 wo pz).
rewrite (order_prod2_substrate (ordinal_p11 oa)(ordinal_p11 ob)).
rewrite (ordinal_p7 oa) (ordinal_p7 ob) => nep.
case (emptyset_dichot a);first by apply anz.
move=> [u ua].
case (emptyset_dichot b);first by apply bnz.
move=> [v vb].
empty_tac1 (variantLc v u).
rewrite product2_rw; ee; bw.
Qed.

Lemma zero_least_ordinal: forall x, is_ordinal x -> 0o <=o x.
Proof. apply ordinal_least. Qed.

Lemma zero_least_ordinal1: forall x, is_ordinal x -> x <> 0o ->
  1o <=o x.
Proof.
move=> x ox xne;rewrite ordinal_le_pr0; ee; first by apply ordinal_1.
rewrite /1o /card_one.
move=> t; aw; move=> ->.
have p1: sub emptyset x by apply emptyset_sub_any.
have p2: transitive_set emptyset by move=> u; case; case.
have p3: emptyset <> x by auto.
apply (ox _ p1 p2 p3).
Qed.

Lemma zero_least_ordinal3: forall x,
  x <=o 0o -> x = 0o.
Proof.
move=> x; rewrite /0o /card_zero ordinal_le_pr0; move=> [_[_]] h.
apply is_emptyset; move=> y yx; move: (h _ yx); case; case.
Qed.

Lemma zero_least_ordinal5: forall x,
  1o <=o x -> x <> 0o.
Proof.
move=> x h xs; rewrite xs in h; move: (zero_least_ordinal3 h) => h1.
by elim card_one_not_zero.
Qed.

Lemma ord_sum_increasing1: forall r f g ,
  order_sum_a r f -> order_sum_a r g ->
  (forall x, inc x (domain f) -> order_le (V x f) (V x g)) ->
  order_le (order_sum r f) (order_sum r g).
Proof.
move => r f g oa oa1 ale.
have o1: order (order_sum r f) by fprops.
have o2: order (order_sum r g) by fprops.
red; ee; apply (order_le_alt o1 o2).
set si:= fun j => choose (fun x => order_morphism x (V j f) (V j g)).
have sip: forall j, inc j (domain f) ->
       order_morphism (si j) (V j f) (V j g).
  move=> j jdf; move:(ale _ jdf) => [p1 [p2 [f0 [x [fx1 fx2]]]]].
  move: (order_le_alt2 p1 p2 fx1 fx2) => [res _].
  rewrite /si; apply choose_pr.
  by exists (BL (fun z => W z f0) (substrate (V j f)) (substrate (V j g))).
have dfdg: domain f = domain g by move: oa oa1 => [_ [s1 _]] [_ [s2 _]]; ue.
set E := (substrate (order_sum r g)).
set F := (disjoint_union_fam (fam_of_substrates f)).
have p1: partition_fam F (substrate (order_sum r f)).
  bw;rewrite /F /sum_of_substrates; rewrite /disjoint_union.
  apply partion_union_disjoint; rewrite /fam_of_substrates; gprops.
have p3: (domain F = domain f).
   rewrite /F/disjoint_union_fam /fam_of_substrates; bw.
set di:= fun i => (product (substrate (V i f)) (singleton i)).
set sj:= fun i => BL (fun z => J (W (P z) (si i)) i) (di i) E.
have p0: forall i, inc i (domain f) ->
   transf_axioms (fun z => J (W (P z) (si i)) i) (di i) E.
  move=> i idf z zV.
  move: (sip _ idf) => [_ [_ [[ff _] [sf [tf _]]]]].
  have aux: inc (W (P z) (si i)) (substrate (V i g)).
    rewrite tf; apply inc_W_target=>//; move: zV; rewrite /di; aw.
    move=> [_ [Ps _]]; ue.
  rewrite /E;bw; apply inc_disjoint_union1 => //; ue.
have FP: forall i, inc i (domain f) -> V i F = di i.
  move=> i idf; rewrite /F /disjoint_union_fam/fam_of_substrates ; bw.
have p2: forall i, inc i (domain F) ->
   function_prop (sj i) (V i F) E.
  rewrite p3;move=> i idf; rewrite /sj FP; red; ee; aw.
  by apply bl_function; apply p0.
move: (extension_partition p1 p2) => [[G [[fG [sG tG]] alg]] _].
rewrite p3 in alg.
have aux: forall x, inc x (source G) ->
  (inc (Q x) (domain f) & inc x (di (Q x)) & is_pair x &
     inc (P x) (substrate (V (Q x) f)) & W x G = J (W (P x) (si (Q x))) (Q x)).
  rewrite sG; bw; move => x xs; move: (du_index_pr1 xs)=> [Qxd [Pxd px]].
  have xdi: inc x (di (Q x)) by rewrite /di; aw.
  ee.
  move: (alg _ Qxd); rewrite /agrees_on; move=> [q1 [q2 q3]].
  move: (xdi); rewrite -FP // => q4.
  move: (q3 _ q4); rewrite /sj; rewrite bl_W; aw;apply p0 => //.
exists G; red; ee.
  split => //; move=> x y xs ys.
  move: (aux _ xs) (aux _ ys) => [Qx [_ [px [Px Wx]]]][Qy [_ [py [Py Wy]]]] sW.
  rewrite Wx Wy in sW; move: (pr1_def sW)(pr2_def sW) => sW1 sQ.
  apply pair_exten =>//.
  rewrite -sQ in sW1; move: (sip _ Qx) => [_ [_ [[_ injf] [sf _]]]].
  apply injf =>//; rewrite -sf //; ue.
move=> x y xs ys.
move: (aux _ xs) (aux _ ys) => [Qx [xdi [px [Px Wx]]]][Qy [ydi [py [Py Wy]]]].
rewrite (order_sum_gle oa) (order_sum_gle oa1).
have ->: (sum_of_substrates f = source G) by rewrite sG; bw.
have ->: (sum_of_substrates g = target G) by rewrite tG /E; bw.
rewrite / order_sum_r; apply iff_eq; move=>[q1 [q2 q3]].
  split;ee ; rewrite Wx Wy; aw; case q3; first by auto.
  move=> [Qxx le1]; right; ee.
  rewrite -Qxx; move: (sip _ Qx) => [_ [_ [_ [sf [tf orf]]]]].
  rewrite -orf //; rewrite -sf //; ue.
rewrite Wx Wy !pr2_pair !pr1_pair in q3.
ee;case q3; first by auto.
move=> [Qxx le1]; right; ee.
move: (sip _ Qx) => [_ [_ [_ [sf [tf orf]]]]].
rewrite -sf in orf;rewrite -Qxx in Py le1; rewrite orf //.
Qed.

Lemma ord_sum_increasing2: forall r f g, worder r ->
  fgraph f -> fgraph g -> substrate r = domain f -> substrate r = domain g ->
  (forall x, inc x (domain f) -> ordinal_le (V x f) (V x g)) ->
  (ord_sum r f) <=o (ord_sum r g).
Proof.
move=> r f g wor fgf fgg sf sg alo.
rewrite /ord_sum -order_le_compatible1.
    apply ord_sum_increasing1.
        red; bw; ee; move=> i idf; bw; move: (alo _ idf) => [aa [bb _]].
        by apply ordinal_p11.
      red; bw; ee; move=> i idf; bw; rewrite -sg sf in idf.
      by move: (alo _ idf) => [aa [bb _]];apply ordinal_p11.
    by bw; move=> x xdf; bw; [move: (alo _ xdf)=> [_ [ _ res]] |rewrite -sg sf].
  apply order_sum_worder => //; [ bw | gprops | bw ].
  move=> i idf; bw; apply ordinal_p10.
  by move: (alo _ idf) => [aa [bb _]].
apply order_sum_worder => //; [ bw | gprops | bw ].
move=> i idf; bw; apply ordinal_p10.
rewrite -sg sf in idf.
by move: (alo _ idf) => [aa [bb _]].
Qed.

Lemma ord_sum_increasing3: forall r f j,
  order_sum_a r f ->
  sub j (domain f) ->
  order_le (order_sum (induced_order r j) (restr f j)) (order_sum r f).
Proof.
move=> r f j oa jd.
move: (oa) => [or [sr [fgf alo]]].
set (g:= L (domain f) (fun z => Yo (inc z j) (V z f) emptyset)).
have dfdg: domain f = domain g by rewrite /g; bw.
have fg: fgraph g by rewrite /g; gprops.
have oa': order_sum_a r g.
  red; ee; first by ue.
  rewrite -dfdg; move=> i idg; rewrite /g; bw; Ytac1 ij; first by apply alo.
   apply emptyset_order.
have sjd': sub j (domain g) by ue.
have cz: (forall i, inc i (complement (domain g) j) -> V i g = 0o).
  by move=> i; srw;rewrite -dfdg /g; move=> [idf nij]; bw; Ytac0.
move: (zero_unit_sum_ord1 oa' sjd' cz).
have drf: domain (restr f j) = j.
  by rewrite restr_domain //; rewrite intersection2C - intersection2_sub.
have drg: domain (restr g j) = j.
  by rewrite restr_domain // -dfdg intersection2C - intersection2_sub.
have ->: (restr f j = restr g j).
    apply fgraph_exten; fprops; rewrite! drf ?drg=>//.
  move=> x xj; move: (jd _ xj) => xdf.
  by bw; rewrite /g; bw; Ytac0.
move=> oi1.
have oi2: order_isomorphic (order_sum r f) (order_sum r f).
  by apply orderIR; apply order_sum_order.
rewrite -(order_le_compatible oi1 oi2).
apply ord_sum_increasing1 => //.
rewrite -dfdg; move=> x xdg; rewrite /g; bw.
Ytac1 xj; first by apply order_le_reflexive=>//; apply alo.
move: emptyset_order => eo.
red;ee; exists (identity emptyset); exists emptyset.
have auw: sub emptyset (substrate (V x f)) by apply emptyset_sub_any.
split => //; red; ee; aw.
      apply identity_bijective.
    apply emptyset_substrate.
  apply (alo _ xdg).
move=> u v ue; elim (emptyset_pr ue).
Qed.

Lemma ord_sum_increasing4: forall r f j, worder r ->
  fgraph f -> substrate r = domain f ->
  sub j (domain f) ->
  (forall j, inc j (domain f) -> is_ordinal (V j f)) ->
  (ord_sum (induced_order r j) (restr f j)) <=o (ord_sum r f).
Proof.
move => r f j wor fgf sr sjf alo.
have sjr: sub j (substrate r) by ue.
have or: order r by move: wor => [or _].
have dr: (domain (restr f j)) = j by rewrite restr_domain1 //.
rewrite /ord_sum -order_le_compatible1; last first.
    apply order_sum_worder => //; [ bw | gprops | bw ].
    move=> i idf; bw; apply ordinal_p10; apply (alo _ idf).
  apply order_sum_worder.
        apply worder_restriction => //; ue.
      by bw; aw;rewrite dr.
    gprops.
  rewrite dr; bw; move=> i ij; bw.
  by apply ordinal_p10; apply alo; apply sjf.
set g:= (L (domain f) (fun z : Set => ordinal_o (V z f))).
have fgg: fgraph g by rewrite /g; gprops.
have sjdg: sub j (domain g) by rewrite /g; bw; ue.
have ->: (L (domain (restr f j)) (fun z : Set => ordinal_o (V z (restr f j))))
   = restr g j.
  apply fgraph_exten; [ gprops | apply (restr_fgraph _ fgg) | bw | ].
    by rewrite dr restr_domain1.
  by rewrite dr /g; bw; move => x xj; bw; apply sjf.
apply ord_sum_increasing3 => //.
by red; ee; rewrite /g; bw; move=> i idf; bw; apply ordinal_p11; apply alo.
Qed.

Lemma ord_prod_increasing1: forall r f g ,
  order_prod_a r f -> order_prod_a r g ->
  (forall x, inc x (domain f) -> order_le (V x f) (V x g)) ->
  order_le (order_prod r f) (order_prod r g).
Proof.
move => r f g oa oa1 ale.
have o1: order (order_prod r f) by fprops.
have o2: order (order_prod r g) by fprops.
red; ee; apply (order_le_alt o1 o2).
set si:= fun j => choose (fun x => order_morphism x (V j f) (V j g)).
have sip: forall j, inc j (domain f) ->
       order_morphism (si j) (V j f) (V j g).
  move=> j jdf; move:(ale _ jdf) => [p1 [p2 [f0 [x [fx1 fx2]]]]].
  move: (order_le_alt2 p1 p2 fx1 fx2) => [res _].
  rewrite /si; apply choose_pr.
  by exists (BL (fun z => W z f0) (substrate (V j f)) (substrate (V j g))).
have dfdg: domain f = domain g by move: oa oa1 => [_ [s1 _]] [_ [s2 _]]; ue.
set E:= substrate (lexicographic_order r f).
set F := substrate(lexicographic_order r g).
have Ep: E = (prod_of_substrates f) by apply lexorder_substrate => //.
have Fp: F = (prod_of_substrates g) by apply lexorder_substrate => //.
have Ep1: forall z, inc z E =
    (fgraph z & domain z = domain f &
       (forall i, inc i (domain f) -> inc (V i z) (substrate (V i f)))).
  move: oa => [wor [sr [fgf alof]]].
  move=> z; rewrite Ep;aw; red; ee.
have Fp1: forall z, inc z F =
    (fgraph z & domain z = domain f &
       (forall i, inc i (domain f) -> inc (V i z) (substrate (V i g)))).
  move: oa1 => [wor [sr [fgf alof]]].
  move=> z; rewrite Fp dfdg;aw; red; ee.
set h:= fun z => L (domain f) (fun i => W (V i z) (si i)).
have ta: transf_axioms h E F.
  move => t; rewrite Ep1 Fp1; move=> [fgt [dt als]].
  rewrite /h; bw;ee; move=> i idf; bw.
  move: (sip _ idf) => [_ [_ [[fsi _] [ssi [tsi _]]]]].
  by rewrite tsi; apply inc_W_target =>//; rewrite -ssi;apply als.
have hi: forall u v, inc u E -> inc v E -> h u = h v -> u = v.
  move=> u v; rewrite Ep1 Ep1 /h; move=> [fgu [du alu]][fgv [dv alv]] sh.
  apply fgraph_exten =>//; first by ue.
  rewrite du; move=> x xdf; move: (f_equal (V x) sh); bw => sW.
  move: (sip _ xdf) => [_ [_ [[fsi insi] [ssi [tsi _]]]]].
  apply insi =>//; rewrite -ssi; [ apply alu => // |apply alv => //].
exists (BL h E F); red; aw; ee.
  apply bl_injective => //.
move=> x y xE yE; rewrite /h bl_W // bl_W //.
rewrite order_prod_gle // order_prod_gle //.
rewrite -Ep -Fp.
have srdf: substrate r = domain f by move: oa => [_ [sr _]].
move: (xE)(yE); rewrite Ep1 Ep1; move=> [fgx [dx alx]][fgy [dy aly]].
apply iff_eq.
  move => [_ [_ aux]]; split; first (by apply ta); split; first by apply ta.
  case aux; first by move=>->; left.
  move=> [j [jsr [jlt jle]]]; right; ex_tac; split.
    rewrite srdf in jsr;move: jlt; bw.
    move: (sip _ jsr) => [_ [_ [[fsi insi] [ssi [tsi jsrp]]]]].
    have vsx: inc (V j x) (source (si j)) by rewrite -ssi; apply alx => //.
    have vsy: inc (V j y) (source (si j)) by rewrite -ssi; apply aly => //.
    rewrite /glt -jsrp //;move=> [p1 p2]; split =>//; dneg sV; apply insi=>//.
  move=> i ij.
  have idf: inc i (domain f) by rewrite -srdf; order_tac.
  by move: (jle _ ij); bw; move=> ->.
move=> [h1 [h2 aux]].
split=> //; split => //; case aux.
  move => sh; left; apply hi =>//.
move=> [j [jsr [jlt jle]]]; right; ex_tac; split.
rewrite srdf in jsr;move: jlt; bw.
move: (sip _ jsr) => [_ [_ [[fsi insi] [ssi [tsi jsrp]]]]].
rewrite /glt -jsrp; first by move=> [p1 p2]; split =>//; dneg sV; ue.
    rewrite -ssi; apply alx => //.
  rewrite -ssi; apply aly => //.
move=> i ij.
have idf: inc i (domain f) by rewrite -srdf; order_tac.
move: (jle _ ij); bw.
move: (sip _ idf) => [_ [_ [[fsi insi] [ssi [tsi jsrp]]]]].
apply insi; rewrite - ssi;[ apply alx => // | apply aly => //].
Qed.

Lemma ord_prod_increasing2: forall r f g, worder r ->
  fgraph f -> fgraph g -> substrate r = domain f -> substrate r = domain g ->
  (forall x, inc x (domain f) -> ordinal_le (V x f) (V x g)) ->
  finite_set (substrate r) ->
  (ord_prod r f) <=o (ord_prod r g).
Proof.
move=> r f g wor fgf fgg sf sg alo fsr.
rewrite /ord_prod-order_le_compatible1.
    apply ord_prod_increasing1.
        red; red; bw; ee; move=> i idf; bw; move: (alo _ idf) => [aa [bb _]].
        by apply ordinal_p11.
      red;red; bw; ee; move=> i idf; bw; rewrite -sg sf in idf.
      by move: (alo _ idf) => [aa [bb _]];apply ordinal_p11.
    by bw; move=> x xdf; bw; [move: (alo _ xdf)=> [_ [ _ res]] |rewrite -sg sf].
  apply order_prod_worder => //; [ bw | gprops | bw ].
  move=> i idf; bw; apply ordinal_p10.
  by move: (alo _ idf) => [aa [bb _]].
apply order_prod_worder => //; [ bw | gprops | bw ].
move=> i idf; bw; apply ordinal_p10.
rewrite -sg sf in idf.
by move: (alo _ idf) => [aa [bb _]].
Qed.

Lemma ord_prod_increasing3: forall r f j,
  order_prod_a r f ->
  sub j (domain f) ->
  (forall x, inc x (complement (domain f) j) ->
     substrate (V x f) <> emptyset) ->
  order_le (order_prod (induced_order r j) (restr f j)) (order_prod r f).
Proof.
move=> r f j oa jd anot.
move: (oa) => [or [sr [fgf alo]]].
set (g:= L (domain f) (fun z => Yo (inc z j) (V z f) (ordinal_o 1o))).
have dfdg: domain f = domain g by rewrite /g; bw.
have fg: fgraph g by rewrite /g; gprops.
have oa': order_prod_a r g.
  red; red;ee; first by ue.
  rewrite -dfdg; move=> i idg; rewrite /g; bw; Ytac1 ij; first by apply alo.
  by apply (ordinal_pr51 ordinal_1).
have sjd': sub j (domain g) by ue.
have cz: (forall i, inc i (complement (domain g) j) ->
  is_singleton (substrate (V i g))).
  move=> i; srw;rewrite -dfdg /g; move=> [idf nij]; bw; Ytac0.
  by rewrite (ordinal_p7 ordinal_1); exists emptyset.
move: (one_unit_prod_ord1 oa' sjd' cz).
have drf: domain (restr f j) = j.
  by rewrite restr_domain //; rewrite intersection2C - intersection2_sub.
have drg: domain (restr g j) = j.
  by rewrite restr_domain // -dfdg intersection2C - intersection2_sub.
have ->: (restr f j = restr g j).
    apply fgraph_exten; fprops; rewrite! drf ?drg=>//.
  move=> x xj; move: (jd _ xj) => xdf.
  by bw; rewrite /g; bw; Ytac0.
move=> oi1.
have oi2: order_isomorphic (order_prod r f) (order_prod r f).
  by apply orderIR; apply order_prod_order.
rewrite -(order_le_compatible oi1 oi2).
apply ord_prod_increasing1 => //.
rewrite -dfdg; move=> x xdg; rewrite /g; bw.
Ytac1 nij; first by apply order_le_reflexive=>//; apply alo.
have p2: order (V x f) by move: oa => [q1 [q2 [q3 q4]]]; apply q4.
have [y yd]: nonempty (substrate (V x f)).
  case (emptyset_dichot (substrate (V x f))) => // p1.
  have xcz: inc x (complement (domain f) j) by srw; ee.
  move: (anot _ xcz) => p4; contradiction.
have s1: sub (singleton y) (substrate (V x f)) by apply sub_singleton.
set h:= BL (fun z => y) (singleton emptyset) (singleton y).
have ta: transf_axioms (fun _ : Set => y) (singleton emptyset) (singleton y).
  by move=> t; aw.
red;ee; exists h; exists (singleton y); ee.
rewrite /h;red; ee; bw; aw.
  apply bl_bijective => //; first by move=> u v; aw; move => -> ->.
  move=> u; aw; move => ->; exists emptyset; aw; ee.
move => u v; rewrite ! singleton_rw; move=> -> ->; aw.
apply iff_eq => un; first by order_tac.
rewrite /1o/card_one; ee.
Qed.

Lemma ord_prod_increasing4: forall r f j, worder r ->
  fgraph f -> substrate r = domain f ->
  sub j (domain f) ->
  (forall j, inc j (domain f) -> is_ordinal (V j f)) ->
  finite_set (substrate r) ->
  (forall x, inc x (complement (domain f) j) -> V x f <> 0o) ->
  (ord_prod (induced_order r j) (restr f j)) <=o (ord_prod r f).
Proof.
move => r f j wor fgf sr sjf alo fsr alnz.
have sjr: sub j (substrate r) by ue.
have or: order r by move: wor => [or _].
have dr: (domain (restr f j)) = j by rewrite restr_domain1 //.
rewrite /ord_prod -order_le_compatible1; last first.
      apply order_prod_worder => //; [ bw | gprops | bw ].
      move=> i idf; bw; apply ordinal_p10; apply (alo _ idf).
    apply order_prod_worder.
          apply worder_restriction => //; ue.
        by bw; aw;rewrite dr.
      gprops.
    rewrite dr; bw; move=> i ij; bw.
    by apply ordinal_p10; apply alo; apply sjf.
  aw;apply (sub_finite_set sjr fsr).
set g:= (L (domain f) (fun z : Set => ordinal_o (V z f))).
have fgg: fgraph g by rewrite /g; gprops.
have sjdg: sub j (domain g) by rewrite /g; bw; ue.
have ->: (L (domain (restr f j)) (fun z : Set => ordinal_o (V z (restr f j))))
   = restr g j.
  apply fgraph_exten; [ gprops | apply (restr_fgraph _ fgg) | bw | ].
    by rewrite dr restr_domain1.
  by rewrite dr /g; bw; move => x xj; bw; apply sjf.
apply ord_prod_increasing3 => //.
  by red;red; ee; rewrite /g; bw; move=> i idf; bw; apply ordinal_p11;apply alo.
rewrite /g; bw;move=> x xc; move: (alnz _ xc).
have xdf: inc x (domain f) by move: xc; srw; intuition.
by bw; rewrite (ordinal_p7 (alo _ xdf)).
Qed.

Lemma ord_sum2_increasing1: forall a b c d,
  ordinal_le a b -> ordinal_le c d ->
  ordinal_le (ord_sum2 a c) (ord_sum2 b d).
Proof.
move=> a b c d le1 le2.
rewrite !ord_sum2_pr; apply ord_sum_increasing2; fprops.
- apply worder_canonical_doubleton_order.
- rewrite substrate_canonical_doubleton_order; bw.
- rewrite substrate_canonical_doubleton_order; bw.
bw; move=> x xtp; try_lvariant xtp.
Qed.

Lemma ord_sum2_increasing2: forall a b,
  is_ordinal a -> is_ordinal b -> a <=o (a +o b).
Proof.
move=> a b oa ob.
set j := singleton TPa; set g := (variantLc a b).
rewrite ord_sum2_pr.
move: worder_canonical_doubleton_order => p1.
have p2: fgraph g by rewrite /g;fprops.
have p3: substrate canonical_doubleton_order = domain g.
  by rewrite /g substrate_canonical_doubleton_order; bw.
have p4: sub j (domain g).
  move=> t; rewrite /j /g; bw; aw; move=> ->; fprops.
have p5: (forall i, inc i (domain g) -> is_ordinal (V i g)).
  rewrite /g;bw; move=> i jd; try_lvariant jd.
move:(ord_sum_increasing4 p1 p2 p3 p4 p5).
have res: V TPa (restr g j) = a by rewrite /g/j; bw; fprops.
have q1: sub j (substrate canonical_doubleton_order) by ue.
have q2: substrate (induced_order canonical_doubleton_order j) = j.
  by aw; move: p1 => [or _ ].
have q3: worder (induced_order canonical_doubleton_order j)
  by apply worder_restriction.
have q4: domain (restr g j) = j by rewrite /g restr_domain1 //.
have q5: inc TPb (singleton TPb) by fprops.
rewrite (ord_sum_singleton (e:= TPa)) => //; try ue; bw; fprops.
Qed.

Lemma ord_sum2_increasing3: forall a b,
  is_ordinal a -> is_ordinal b -> b <=o (a +o b).
Proof.
move=> a b oa ob.
set j := singleton TPb; set g := (variantLc a b).
rewrite ord_sum2_pr.
move: worder_canonical_doubleton_order => p1.
have p2: fgraph g by rewrite /g;fprops.
have p3: substrate canonical_doubleton_order = domain g.
  by rewrite /g substrate_canonical_doubleton_order; bw.
have p4: sub j (domain g).
  move=> t; rewrite /j /g; bw; aw; move=> ->; fprops.
have p5: (forall i, inc i (domain g) -> is_ordinal (V i g)).
  rewrite /g;bw; move=> i jd; try_lvariant jd.
move:(ord_sum_increasing4 p1 p2 p3 p4 p5).
have res: V TPb (restr g j) = b by rewrite /g/j; bw; fprops.
have q1: sub j (substrate canonical_doubleton_order) by ue.
have q2: substrate (induced_order canonical_doubleton_order j) = j.
  by aw; move: p1 => [or _ ].
have q3: worder (induced_order canonical_doubleton_order j)
  by apply worder_restriction.
have q4: domain (restr g j) = j by rewrite /g restr_domain1 //.
have q5: inc TPa (singleton TPa) by fprops.
rewrite (ord_sum_singleton (e:= TPb)) => //; try ue; bw; fprops.
Qed.

Lemma ord_prod2_increasing1: forall a b c d,
  a <=o b -> c <=o d -> (a *o c) <=o (b *o d).
Proof.
move=> a b c d le1 le2; rewrite !ord_prod2_pr.
apply ord_prod_increasing2; fprops.
- apply worder_canonical_doubleton_order.
- rewrite substrate_canonical_doubleton_order; bw.
- rewrite substrate_canonical_doubleton_order; bw.
- bw; move=> x xtp; try_lvariant xtp.
- rewrite substrate_canonical_doubleton_order -two_points_pr2.
  apply doubleton_finite.
Qed.

Lemma ord_prod2_increasing2: forall a b,
  is_ordinal a -> is_ordinal b -> b <> 0o -> a <=o (a *o b).
Proof.
move=> a b oa ob bnz.
set j := singleton TPb.
rewrite ord_prod2_pr.
move: worder_canonical_doubleton_order => p1.
have p2: fgraph (variantLc b a) by fprops.
have p3: substrate canonical_doubleton_order = domain (variantLc b a).
  by rewrite substrate_canonical_doubleton_order; bw.
have p4: sub j (domain (variantLc b a)).
  move=> t; rewrite /j; bw; aw; move=> ->; fprops.
have p5: (forall i, inc i (domain (variantLc b a)) ->
   is_ordinal (V i (variantLc b a))).
  bw; move=> i jd; try_lvariant jd.
have p6: finite_set (substrate canonical_doubleton_order).
  rewrite substrate_canonical_doubleton_order -two_points_pr2.
  apply doubleton_finite.
have p7: (forall x, inc x (complement (domain (variantLc b a)) j)
     -> V x (variantLc b a) <> 0o).
  rewrite /j;move=> x; bw; srw; aw; move=> [xtp]; move:xtp=> [] ->; bw.
  by move => h; elim h.
move:(ord_prod_increasing4 p1 p2 p3 p4 p5 p6 p7).
have res: V TPb (restr (variantLc b a) j) = a by bw; rewrite /j; fprops.
have q1: sub j (substrate canonical_doubleton_order) by ue.
have q2: substrate (induced_order canonical_doubleton_order j) = j.
  by aw; move: p1 => [or _ ].
have q3: worder (induced_order canonical_doubleton_order j)
  by apply worder_restriction.
have q4: domain (restr (variantLc b a) j) = j by rewrite restr_domain1 //.
have q5: inc TPb (singleton TPb) by fprops.
rewrite (ord_prod_singleton (e:= TPb)) => //; try ue; bw; fprops.
Qed.

Lemma ord_prod2_increasing3: forall a b,
  is_ordinal a -> is_ordinal b -> a <> 0o -> b <=o (a *o b).
Proof.
move=> a b oa ob bnz.
set j := singleton TPa.
rewrite ord_prod2_pr.
move: worder_canonical_doubleton_order => p1.
have p2: fgraph (variantLc b a) by fprops.
have p3: substrate canonical_doubleton_order = domain (variantLc b a).
  by rewrite substrate_canonical_doubleton_order; bw.
have p4: sub j (domain (variantLc b a)).
  move=> t; rewrite /j; bw; aw; move=> ->; fprops.
have p5: (forall i, inc i (domain (variantLc b a)) ->
   is_ordinal (V i (variantLc b a))).
  bw; move=> i jd; try_lvariant jd.
have p6: finite_set (substrate canonical_doubleton_order).
  rewrite substrate_canonical_doubleton_order -two_points_pr2.
  apply doubleton_finite.
have p7: (forall x, inc x (complement (domain (variantLc b a)) j)
     -> V x (variantLc b a) <> 0o).
  rewrite /j;move=> x; bw; srw; aw; move=> [xtp]; move:xtp=> [] ->; bw.
  by move => h; elim h.
move:(ord_prod_increasing4 p1 p2 p3 p4 p5 p6 p7).
have res: V TPa (restr (variantLc b a) j) = b by bw; rewrite /j; fprops.
have q1: sub j (substrate canonical_doubleton_order) by ue.
have q2: substrate (induced_order canonical_doubleton_order j) = j.
  by aw; move: p1 => [or _ ].
have q3: worder (induced_order canonical_doubleton_order j)
  by apply worder_restriction.
have q4: domain (restr (variantLc b a) j) = j by rewrite restr_domain1 //.
have q5: inc TPa (singleton TPa) by fprops.
rewrite (ord_prod_singleton (e:= TPa)) => //; try ue; bw; fprops.
Qed.

Lemma ord_sum2_increasing4: forall a b c,
  a <=o b -> is_ordinal c -> (a +o c) <=o (b +o c).
Proof. move=> a b c leab oc; apply ord_sum2_increasing1 => //; ord_tac. Qed.

Lemma ord_sum2_increasing5: forall a b c,
  a <=o b -> is_ordinal c -> (c +o a) <=o (c +o b).
Proof. move=> a b c leab oc; apply ord_sum2_increasing1 => //; ord_tac. Qed.

Lemma ord_prod2_increasing4: forall a b c,
  a <=o b -> is_ordinal c -> (a *o c) <=o (b *o c).
Proof. move=> a b c leab oc; apply ord_prod2_increasing1 => //; ord_tac. Qed.

Lemma ord_prod2_increasing5: forall a b c,
  a <=o b -> is_ordinal c -> (c *o a) <=o (c *o b).
Proof. move=> a b c leab oc; apply ord_prod2_increasing1 => //; ord_tac. Qed.

Lemma cardinal_of_ordinal: forall x, worder x ->
  cardinal (ordinal x) = cardinal (substrate x).
Proof.
move=> x wx; move: (ordinal_p2 wx); move=> [f [_ [_ [bf [sf [tf _]]]]]].
symmetry.
rewrite (ordinal_p7 (ordinal_p1 wx)) in tf.
rewrite sf tf; aw; exists f; ee.
Qed.

Lemma cardinal_ord_sum: forall a b, is_ordinal a -> is_ordinal b ->
  cardinal (a +o b) = (cardinal a) +c (cardinal b).
Proof.
move=> a b oa ob.
move: (ordinal_p11 oa)(ordinal_p11 ob)=> p1 p2.
set h := (order_sum2 (ordinal_o a) (ordinal_o b)).
have wh:worder h by rewrite /h; apply order_sum2_worder;apply ordinal_p10.
rewrite (cardinal_of_ordinal wh) order_sum2_substrate //.
rewrite (ordinal_p7 oa) (ordinal_p7 ob).
have ->: cardinal (canonical_du2 a b) = card_plus a b by [].
by symmetry;apply card_plus_pr2; apply double_cardinal.
Qed.

Lemma cardinal_ord_sum2: forall a b,
  inc a Bnat -> inc b Bnat ->
  a +o b = a +c b.
Proof.
move=> a b aB bB.
have ba: is_ordinal a by apply cardinal_ordinal; fprops.
have bb: is_ordinal b by apply cardinal_ordinal; fprops.
move: (cardinal_ord_sum ba bb).
set X := ord_sum2 a b.
have boX: is_ordinal X by rewrite /X; apply ord_sum2_ordinal.
rewrite (Bnat_cardinal aB) (Bnat_cardinal bB) => h.
have fs: finite_set X by red;rewrite -inc_Bnat h; hprops.
rewrite -(cardinal_of_cardinal (finite_cardinal_pr1 (ordinal_finite1 boX fs))).
done.
Qed.

Lemma ord_11_2: 1o +o 1o = 2o.
Proof.
by move:(cardinal_ord_sum2 inc1_Bnat inc1_Bnat); rewrite card_two_pr.
Qed.

Lemma ord_plus_int_omega: forall n, inc n Bnat ->
  ord_sum2 n ord_omega = ord_omega.
Proof.
move=> n nB.
move: Bnat_order_worder => woB.
move: (interval_Bnatco_worder nB) => woi.
rewrite ord_omega_pr (finite_ordinal1 nB).
apply ord_sum_invariant5 =>//.
have os: order (order_sum2 (interval_Bnatco n) Bnat_order) by fprops.
have oB: order Bnat_order by fprops.
have oi: order (interval_Bnatco n) by fprops.
set E:= substrate (order_sum2 (interval_Bnatco n) Bnat_order).
set F:= substrate Bnat_order.
have Fp: F = Bnat by rewrite /F Bnat_order_substrate.
have Ep: E = canonical_du2 (interval_co_0a n) F.
   aw; rewrite /E order_sum2_substrate // interval_Bnatco_substrate //.
set f:= fun z => Yo (Q z = TPa) (P z) (card_plus n (P z)).
have tpd: TPb <> TPa by fprops.
have ta: transf_axioms f E F.
  move=> t; rewrite Ep Fp canonical_du2_pr //; move=> [pt h].
  rewrite /f; case h; move => [Pt Qt]; rewrite Qt; Ytac0; last by hprops.
     apply (sub_interval_co_0a_Bnat Pt).
have fi: forall x y, inc x E -> inc y E -> f x = f y -> x = y.
  move=> x y; rewrite Ep canonical_du2_pr // canonical_du2_pr // /f.
  move=> [px hx][py hy].
  case hx; case hy; move=> [Py Qy][Px Qx]; rewrite Qx Qy; Ytac0; Ytac0 => aux.
        apply pair_exten => //; ue.
      move: Px; rewrite interval_co_0a_pr2//; move=> pxn.
      have npx: cardinal_le n (P x).
        rewrite aux; apply sum_increasing3 =>//; [ | rewrite Fp in Py]; fprops.
      co_tac.
    move: Py; rewrite interval_co_0a_pr2//; move=> pxn.
    have npx: cardinal_le n (P y).
      rewrite -aux; apply sum_increasing3 =>//; [ | rewrite Fp in Px]; fprops.
    co_tac.
  apply pair_exten => //; last by ue.
  rewrite Fp in Px Py;apply plus_simplifiable_left with n =>//.
exists (BL f E F); red; ee; aw.
  apply bl_bijective => //.
  rewrite Fp; move=> y yF.
  have cn: is_cardinal n by fprops.
  have cy: is_cardinal y by fprops.
  case (cardinal_le_total_order2 cn cy) => cny.
    exists (J (card_sub y n) TPb); rewrite Ep canonical_du2_pr //; ee.
      right; aw; rewrite Fp; ee.
    rewrite /f; aw; rewrite Y_if_not_rw //; apply (card_sub_pr cny).
  exists (J y TPa); rewrite Ep canonical_du2_pr //; ee.
    left; aw;rewrite interval_co_0a_pr2//.
  by rewrite /f; aw;rewrite Y_if_rw.
move=> x y xE yE.
rewrite order_sum2_gle // ! Bnat_order_le /Bnat_le.
rewrite bl_W // bl_W//.
rewrite Fp in ta.
apply iff_eq; move=> [p1 [p2 p3]].
  split; first (by apply ta); split; first by apply ta.
  rewrite /f; case p3.
    move=> [q1 [q2 q3]]; rewrite q1 q2; Ytac0; Ytac0.
    rewrite interval_Bnatco_related // in q3; intuition.
  case.
    move=> [q1 [q2 [q3 [q4 q5]]]]; Ytac0; Ytac0.
    apply sum_increasing2 => //; fprops.
  move=> [q1 q2]; Ytac0; Ytac0.
  move: xE; rewrite Ep canonical_du2_pr //; move => [px]; case.
    rewrite interval_co_0a_pr2//.
    move=> [[ple _] _].
    have le2: cardinal_le n (card_plus n (P y)).
       apply sum_increasing3 => //; fprops.
       move: yE; rewrite Ep canonical_du2_pr //; move => [qx]; case.
       move=> [py _]; move: (sub_interval_co_0a_Bnat py) => pB; fprops.
       rewrite Fp; move=> [py _]; fprops.
       co_tac.
  by move=> [_ Qx]; elim tpd;rewrite -q1 -Qx.
split; first by move: xE; rewrite /E order_sum2_substrate //.
split; first by move: yE; rewrite /E order_sum2_substrate //.
move: xE yE; rewrite Ep canonical_du2_pr // canonical_du2_pr // /f.
move=> [px hx][py hy].
move: p3; rewrite /f.
case hx; case hy; move=> [Py Qy][Px Qx]; rewrite Qx Qy; Ytac0; Ytac0 => fp.
      left; ee; rewrite interval_Bnatco_related //; ee.
      move: Py; rewrite interval_co_0a_pr2//.
    right; right; ee.
  have le2: cardinal_le n (card_plus n (P x)).
    apply sum_increasing3 => //; fprops; rewrite Fp in Px; fprops.
  have le3: cardinal_le n (P y) by co_tac.
  move: Py; rewrite interval_co_0a_pr2// => le4; co_tac.
right; left; ee; try ue.
apply plus_le_simplifiable with n => //; ue.
Qed.

Lemma ord_mult_int_omega: forall n, inc n Bnat ->
  n <> 0c -> n *o \omega = \omega.
Proof.
move=> n nB nz.
move: Bnat_order_worder => woB.
move: (interval_Bnatco_worder nB) => woi.
rewrite ord_omega_pr (finite_ordinal1 nB).
apply ord_prod_invariant5 =>//.
have os: order (order_prod2 (interval_Bnatco n) Bnat_order) by fprops.
have oB: order Bnat_order by fprops.
have oi: order (interval_Bnatco n) by fprops.
set E:= substrate (order_prod2 (interval_Bnatco n) Bnat_order).
set F:= substrate Bnat_order.
have Fp: F = Bnat by rewrite /F Bnat_order_substrate.
have Ep: E = product2 F (interval_co_0a n).
   aw; rewrite /E order_prod2_substrate // interval_Bnatco_substrate //.
have ep1: forall x, inc x E ->
  (inc (V TPa x) Bnat & inc (V TPb x) Bnat & cardinal_lt (V TPb x) n).
  move=> x; rewrite Ep Fp product2_rw; move=> [fgx [dx [xa xb]]].
  split => //; split.
    apply (sub_interval_co_0a_Bnat xb).
  move: xb;rewrite interval_co_0a_pr2//.
set f:= fun z => card_plus (card_mult n (V TPa z)) (V TPb z).
have ta: forall x, inc x E -> inc (f x) F.
  move=> x xE; rewrite Fp /f; move: (ep1 _ xE) => [p1 [p2 _]]; hprops.
have fi: forall x y, inc x E -> inc y E -> f x = f y -> x = y.
  rewrite /f=> x y xE yE sf.
  move: (ep1 _ xE) (ep1 _ yE)=> [p1 [p2 p3]][p4 [p5 p6]].
  set m := card_plus (card_mult n (V TPa x)) (V TPb x).
  have mB: inc m Bnat by rewrite /m; hprops.
  have d1: (division_prop m n (V TPa x) (V TPb x)) by red;ee.
  have d2: (division_prop m n (V TPa y) (V TPb y)) by red;ee.
  move: (division_unique mB nB p1 p2 p4 p5 nz d1 d2) => [sa sb].
  move: xE yE; rewrite Ep product2_rw product2_rw.
  move => [fgx [dx _]][fgy [dy _]].
  apply fgraph_exten=>//; first by ue.
  rewrite dx; move=> i idx; try_lvariant idx.
exists (BL f E F); red; aw;ee.
  apply bl_bijective => //; rewrite Ep Fp.
  move=> y yB; move: (Bnat_division yB nB nz) => [rB [qB [d1 d2]]].
  exists (variantLc (card_quo y n) (card_rem y n)); split.
    rewrite product2_rw; bw; ee.
      rewrite -inc_Bnat//.
    rewrite interval_co_0a_pr2//.
  by rewrite /f; bw.
move=> x y xE yE; rewrite bl_W // bl_W//.
rewrite Bnat_order_le /Bnat_le.
rewrite order_prod2_gle //.
apply iff_eq; move=> [p1 [p2 aux]].
  rewrite -Fp;split; first (by apply ta);split; first by apply ta.
  rewrite /f; case aux.
    move=> [vv]; rewrite vv.
    rewrite interval_Bnatco_related //; move=> [lea _].
    apply sum_increasing2; fprops.
  rewrite /glt; rewrite Bnat_order_le /Bnat_le; move=> [[axB [ayB axy]] naxy].
  set pr1 := (card_mult n (V TPa x)).
  set pr2 := (card_mult n (V TPa y)).
  have p1B: inc pr1 Bnat by rewrite /pr1;hprops.
  have p2B: inc pr2 Bnat by rewrite /pr2;hprops.
  move: (ep1 _ xE) (ep1 _ yE)=> [r1 [r2 [r3 _]]][r4 [r5 r6]].
  have le1: cardinal_le pr2 (card_plus pr2 (V TPb y)).
    apply sum_increasing3; fprops.
  have le2: cardinal_le (card_plus pr1 (V TPb x)) (card_plus pr1 n).
    apply sum_increasing2; fprops.
  have le3: (card_plus pr1 n = card_mult n (succ (V TPa x))).
    rewrite /pr1 (Bsucc_rw r1) cardinal_distrib_prod_sum3 one_unit_prodr;fprops.
  rewrite le3 in le2.
  have le4: cardinal_le (succ (V TPa x)) (V TPa y).
    rewrite lt_n_succ_le0 //; fprops.
  have le5: cardinal_le (card_mult n (succ (V TPa x)))(card_mult n (V TPa y)).
     apply product_increasing2; fprops.
  have le6: cardinal_le (card_plus pr1 (V TPb x)) (card_mult n (V TPa y)).
    co_tac.
  co_tac.
split; first by move: xE; rewrite /E order_prod2_substrate.
split; first by move: yE; rewrite /E order_prod2_substrate.
move: aux; rewrite /f => fv.
set ax:= V TPa x; set bx:= V TPb x; set ay:= V TPa y; set byv:= V TPb y.
move: (ep1 _ xE) (ep1 _ yE)=> [r1 [r2 [r3 _]]][r4 [r5 r6]].
have cax: is_cardinal ax by fprops.
have cay: is_cardinal ay by fprops.
case (cardinal_le_total_order1 cax cay).
  move=> sa; left; ee.
  rewrite interval_Bnatco_related //; ee.
  rewrite /bx /byv.
  move:fv. rewrite -/ax -/ay sa.
  apply plus_le_simplifiable; hprops.
case; first by move=> [r7 rr8]; right;rewrite /glt Bnat_order_le /Bnat_le; ee.
have le1: cardinal_le (card_mult n (V TPa x))
    (card_plus (card_mult n (V TPa x)) (V TPb x)).
  apply sum_increasing3; fprops.
have le2: cardinal_le (card_mult n (V TPa x))
    (card_plus (card_mult n (V TPa y)) (V TPb y)) by co_tac.
move: (r6) => [r6a r6b].
have : cardinal_lt (card_plus (card_mult n (V TPa y)) (V TPb y))
 (card_plus (card_mult n (V TPa y)) n).
  split.
     apply sum_increasing2; [apply cardinal_le_reflexive; fprops | exact ].
  dneg aux.
  apply plus_simplifiable_left with (card_mult n (V TPa y)); hprops.
have ->: (card_plus (card_mult n (V TPa y)) n = card_mult n (succ (V TPa y))).
  rewrite (Bsucc_rw r4) cardinal_distrib_prod_sum3 one_unit_prodr;fprops.
move => le4.
have le5: cardinal_lt (card_mult n (V TPa x)) (card_mult n (succ (V TPa y))).
  co_tac.
rewrite -lt_n_succ_le0 // => le6.
have le7: cardinal_le (card_mult n (succ ay))(card_mult n ax).
  apply product_increasing2; fprops.
rewrite -/ay in le5.
co_tac.
Qed.

Lemma ordinal_a_ne_ab: forall a b, is_ordinal a -> is_ordinal b ->
   a = a +o b -> b = 0o.
Proof.
move=> a b oa ob; rewrite /ord_sum2.
set c:= order_sum2 _ _ .
move: (ordinal_p11 oa) => ora.
move: (ordinal_p11 ob) => orb.
move=> aoc.
set A := Zo (substrate c) (fun z => (Q z) = TPa).
have p1: worder c by rewrite /c; apply order_sum2_worder;apply ordinal_p10.
have orc: order c by move: p1 => [oc _].
have p2: sub A (substrate c) by rewrite /A; apply Z_sub.
have p3: is_segment c A.
   red; ee; move=> x y; rewrite /A ! Z_rw ; move => [_ Qx] cx;split.
     order_tac.
   move: cx; rewrite (order_sum2_gle _ _ ora orb); move=> [_ [_ cs]].
   case cs; first (by intuition); case; last by intuition.
   by move=> [_ [bad _]].
have p4: is_segment c (substrate c) by apply substrate_is_segment.
have sc: substrate c = (canonical_du2 a b).
   rewrite /c order_sum2_substrate // !ordinal_p7//.
have aux: order_isomorphic (ordinal_o a) (induced_order c A).
  have ta: transf_axioms (fun z => (J z TPa)) a A.
    move=> z zs; rewrite /A; apply Z_inc; last by aw.
    rewrite sc canonical_du2_pr;aw; ee.
  exists (BL (fun z => (J z TPa)) a A).
  red; ee; aw.
    apply bl_bijective => //; first by move=> u v _ _; apply pr1_def.
    move=> y; rewrite Z_rw sc canonical_du2_pr.
    move=> [[py h] Qy]; case h; move=> [Py Qy'].
      by ex_tac; apply pair_exten; ee; aw.
    by elim two_points_distinct; rewrite -Qy -Qy'.
  move=> x y xs ys; aw; try apply ta => //.
  rewrite /c order_sum2_gle // (ordinal_p7 oa) (ordinal_p7 ob) -sc.
  apply iff_eq.
   move=> h; split; [by apply p2; apply ta | split; [by apply p2; apply ta |]].
   left; aw; ee.
  move=> [_ [_ ]]; aw;case; first by intuition.
  by case; [ move=> [_ [bad _]] | move => [_ bad]] ; elim bad.
have p5: order_isomorphic (induced_order c (substrate c)) (induced_order c A).
  rewrite induced_order_substrate //.
  move:(ordinal_p2 p1); rewrite -aoc => aux2.
  apply (orderIT aux2 aux).
move:(segments_iso1 p1 p2 p3 p4 p5) => Ac.
apply is_emptyset.
move=> y yb.
have: inc (J y TPb)(substrate c) by rewrite sc canonical_du2_pr; aw;ee.
by rewrite -Ac /A Z_rw; aw; move=> [_ bad]; elim two_points_distinctb.
Qed.

Lemma ord_double: forall x, is_ordinal x ->
  x *o 2o = x +o x.
Proof.
move=> x Bx.
rewrite - ord_11_2 (order_sum_distributive3 ordinal_1 ordinal_1 Bx).
by rewrite (ord_1_mult_unit_r Bx).
Qed.

Lemma ord_omega_non_zero: \omega <> 0o.
Proof.
move: inc0_Bnat;rewrite -[ord_omega]/Bnat.
move=> ob bad ;rewrite bad in ob; elim (emptyset_pr ob).
Qed.

Lemma order_sum_nc: let x := 1o in let y := \omega in
   x +o y <> y +o x.
Proof.
move=> x y; rewrite (ord_plus_int_omega inc1_Bnat) /y=> h.
move: (ordinal_a_ne_ab ordinal_omega ordinal_1 h).
apply card_one_not_zero.
Qed.

Lemma order_prod_nc: let x := 2o in let y := \omega in
   x *o y <> y *o x.
Proof.
move: card_two_not_zero => tnz.
move=> x y; rewrite (ord_mult_int_omega inc2_Bnat tnz).
rewrite (ord_double ordinal_omega) => h.
move: (ordinal_a_ne_ab ordinal_omega ordinal_omega h).
apply ord_omega_non_zero.
Qed.

Lemma order_sum_distr4:
  let a:= 1o in let b:= 1o in let c:= ord_omega in
  (a +o b) *o c <> (a *o c) +o (b *o c).
Proof.
move=> a b c.
move: card_one_not_zero => onz.
move: card_two_not_zero => tnz.
move: inc1_Bnat => ob.
rewrite (ord_mult_int_omega ob onz) (cardinal_ord_sum2 ob ob).
rewrite card_two_pr (ord_mult_int_omega inc2_Bnat tnz) => h.
move: (ordinal_a_ne_ab ordinal_omega ordinal_omega h).
apply ord_omega_non_zero.
Qed.

Lemma ord_succ_pr: forall x, is_ordinal x ->
  x +o 1o = succ_o x.
Proof.
move=> x xo; rewrite /ord_sum2.
move: (ordinal_succ xo) => sxo.
move: ordinal_1 => o1.
set aux:= (order_sum2 _ _).
have wo1: worder aux.
  by apply order_sum2_worder; apply ordinal_p10 => //.
apply ordinal_p9 => //.
set A:= substrate aux.
set B:= substrate (ordinal_o (succ_o x)).
have bv:succ_o x = B by symmetry; apply ordinal_p7.
have av: A = canonical_du2 x 1o.
  by rewrite /A order_sum2_substrate ?ordinal_p7 ; fprops.
have ab: TPb <> TPa by fprops.
have ta: transf_axioms (fun z : Set => Yo (Q z = TPa) (P z) x) A B.
  rewrite av -bv /succ_o;move=> z; rewrite canonical_du2_pr.
  move=> [_]; case; move=> [pz qz]; rewrite qz;Ytac0; fprops.
exists (BL (fun z => (Yo (Q z = TPa) (P z) x)) A B).
red; ee; aw.
  apply bl_bijective => //.
    move=> u v;rewrite av !canonical_du2_pr; move=> [up p1][vp p2].
    case p1=> [] [pa pb]; case p2=> [] [qa qb]; rewrite pb qb; Ytac0;Ytac0 => h.
    - apply pair_exten => //; ue.
    - rewrite h in pa; elim (ordinal_irreflexive xo pa).
    - rewrite -h in qa; elim (ordinal_irreflexive xo qa).
    - move: pa qa; rewrite /1o /card_one; aw.
      move => r1 r2; apply pair_exten => //; ue.
  rewrite av -bv /succ_o;move=> y; rewrite tack_on_rw; case.
    by move=> yw; exists (J y TPa); rewrite canonical_du2_pr; aw; ee;Ytac0.
  move => ->; exists (J emptyset TPb); rewrite canonical_du2_pr; aw; ee.
      right; rewrite /1o/card_one; fprops.
  by Ytac0.
have o2: order (ordinal_o x) by apply ordinal_p11.
have o3: order (ordinal_o 1o) by apply ordinal_p11.
move=> u v uA vA; rewrite (bl_W ta uA) (bl_W ta vA) /aux.
rewrite (order_sum2_gle _ _ o2 o3) (ordinal_p7 xo) (ordinal_p7 o1) -av.
rewrite/ordinal_o /gle ! subinclusion_order_rw.
rewrite /succ_o; apply iff_eq.
  move=> [_ [_ ]]; case; [ | case ];
  [move => [p1 [p2 p3]] | move => [p1 [p2 p3]] | move=> [p1 p2]];
   Ytac0; Ytac0; [ ee | ee |].
  move: uA; rewrite av canonical_du2_pr; move=> [_]; case; move=> [p3 p4].
    ee; apply (ordinal_transitive xo p3).
  by elim ab; ue.
move=> [h1 [h2 h3]]; ee.
move: uA vA h1 h2 h3;rewrite av !canonical_du2_pr; move=> [up p1][vp p2].
case p1=> [][pa p]; case p2 => [] [qa q]; rewrite p q; Ytac0; Ytac0 => h1 h2 h3.
- left; ee.
- right; right; ee.
- elim (ordinal_decent xo qa (h3 _ qa)).
- right; left; ee.
   move: pa; rewrite /1o/card_one; aw => ->; apply emptyset_sub_any.
Qed.

Lemma ord_succ_lt: forall a, is_ordinal a -> a <o (succ_o a).
Proof.
move=> a oa;rewrite ordinal_lt_pr0; ee.
  apply (ordinal_succ oa).
rewrite /succ_o; fprops.
Qed.

Lemma ord_lt_01: 0o <o 1o.
Proof.
rewrite ordinal_lt_pr0; ee.
    apply ordinal_0.
  apply ordinal_1.
rewrite /1o/card_one; fprops.
Qed.

Lemma ord_lt_12: 1o <o 2o.
Proof.
move: ordinal_1 => x1.
rewrite - ord_11_2 (ord_succ_pr x1); apply (ord_succ_lt x1).
Qed.

Lemma ord_lt_02: 0o <o 2o.
Proof. move: ord_lt_12 => [le _]; apply (ordinal_lt_le_trans ord_lt_01 le).
Qed.

Lemma succ_ordinal: forall a, is_ordinal a -> is_ordinal (a +o 1o).
Proof. by move=> a oa; move: ordinal_1 => oo; apply ord_sum2_ordinal.
Qed.

Hint Resolve ordinal_succ: fprops.

Lemma ord_lt_succ: forall a b, a <o (succ_o b) = a <=o b.
Proof.
move=> a b; rewrite ordinal_lt_pr0 ordinal_le_pr0.
apply iff_eq; move=> [p1 [p2 p3]].
  have bs: inc b (succ_o b) by rewrite /succ_o; fprops.
  move: (elt_of_ordinal p2 bs) => ob.
  by ee; rewrite (ordinal_sub4 p1 ob).
rewrite -(ordinal_sub4 p1 p2); ee.
Qed.

Lemma ord_succ_lt2: forall a b, a <o b = (succ_o a) <=o b.
Proof.
move=> a b; rewrite ordinal_lt_pr0 ordinal_le_pr0.
apply iff_eq; move=> [p1 [p2 p3]].
  ee. rewrite /succ_o; move => t; aw.
  case; [ apply (ordinal_transitive p2 p3) | by move=> -> ].
have asa: inc a (succ_o a) by rewrite /succ_o; fprops.
ee; apply (elt_of_ordinal p1 asa).
Qed.

Lemma ord2_lt_pr: forall x, 2o <=o x = 1o <o x.
Proof. by move=> x; rewrite /ord_two -succ_o_one -ord_succ_lt2. Qed.

Lemma ord2_trichotomy: forall x, is_ordinal x ->
  x = 0o \/ x= 1o \/ 2o <=o x.
Proof.
move=> x ox.
case (equal_or_not x 0o); first by left.
move=> xe; right.
case (equal_or_not x 1o); first by left.
move=> xee; right;rewrite ord2_lt_pr.
split; first apply zero_least_ordinal1; fprops.
Qed.

Lemma ord2_trichotomy1: forall x,
  2o <=o x -> (x <> 0o & x <> 1o).
Proof.
move=> x h; split.
    move=> xz; rewrite xz in h; move: (zero_least_ordinal3 h).
    apply card_two_not_zero.
  move => xz; move: h; rewrite xz ord2_lt_pr; by move=> [_].
Qed.

Lemma ord_succ_inj: forall a b, is_ordinal a -> is_ordinal b ->
   (succ_o a = succ_o b) -> a = b.
Proof.
rewrite /succ_o;move=> a b oa ob ss.
have: inc a (tack_on b b) by rewrite -ss; fprops.
have: inc b (tack_on a a) by rewrite ss; fprops.
aw; case => //; move=> h1 //;case => // => h2.
move: (ordinal_transitive oa h1 h2) => h3.
by elim (ordinal_decent oa h3).
Qed.

End Ordinals1.
Export Ordinals1.