Library ssete6

Theory of Sets : Exercises sections 6

Copyright INRIA (2012-2013) Marelle Team (Jose Grimm).

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

Require Export sset15.

Module Exercise6.

Definition csup_s A := \csup (fun_image A succ_c).

Lemma csup_s1 A (x := csup_s A): cardinal_set A ->
  (forall y, inc y A -> y <c x).
Proof.
move => csa y yA.
rewrite /x/csup_s; set B := fun_image _ _.
apply /(succ_c_pr5P (csa _ yA)) ; apply:card_sup_ub.
move => t /funI_P [z za ->]; first by exact: (CS_succ_c (csa _ za)).
by apply /funI_P; ex_tac.
Qed.

Lemma csup_s2 A z: cardinal_set A -> cardinalp z ->
  (forall y, inc y A -> y <c z) -> csup_s A <=c z.
Proof.
move => csa cz h2; apply: card_ub_sup => //.
  move => t /funI_P [u za ->]; exact (CS_succ_c (csa _ za)).
move => i /funI_P [t /h2 tA ->]; apply /succ_c_pr5P => //; co_tac.
Qed.

Definition disjointness_degree F :=
  csup_s (fun_image (coarse F -s diagonal F)
       (fun z => cardinal ((P z) \cap (Q z)))).

Lemma dd_pr1 F x y: inc x F -> inc y F -> x <> y ->
  cardinal (x \cap y) <c (disjointness_degree F).
Proof.
move => xF yF xy; apply: csup_s1.
  move=> t /funI_P [z _ ->]; fprops.
apply /funI_P; exists (J x y); aw => //.
apply /setC_P;split => //; first by apply :setXp_i.
by case /diagonal_pi_P.
Qed.

Lemma dd_pr2 F z: cardinalp z ->
  (forall x y, inc x F -> inc y F -> x <> y ->
     cardinal (x \cap y) <c z)
  -> (disjointness_degree F) <=c z.
Proof.
move => cz h; apply:csup_s2 => //.
  move=> t /funI_P [u _ ->]; fprops.
move => y /funI_P [t /setC_P [/setX_P [pt Pt Qt] pb ->]]; apply: h => //.
by move => xy; case: pb; apply /diagonal_i_P.
Qed.

Lemma dd_pr3 F : (disjointness_degree F = \0c) <-> small_set F.
Proof.
split => h.
   move => x y fx fy; ex_middle xy.
   by move: (dd_pr1 fx fy xy); rewrite h => /card_lt0.
by apply: card_le0; apply: (dd_pr2 CS0) => x y xf yf; move: (h _ _ xf yf).
Qed.

Lemma dd_pr4 F : (disjointness_degree F = \1c) <->
  (~ small_set F /\ forall x y, inc x F -> inc y F -> disjointVeq x y).
Proof.
split => h.
  split; first by move /dd_pr3; rewrite h; fprops.
  move => x y xf yf; case: (equal_or_not x y); first by left.
  move => xny; move: (dd_pr1 xf yf xny); rewrite h.
  by move /card_lt1 /cardinal_nonemptyset; right.
move: h => [/dd_pr3 dn0 h1]; ex_middle aux.
have aux2: disjointness_degree F <=c \1c.
   apply: (dd_pr2 CS1) => x y xF yF; case: (h1 _ _ xF yF) => // -> _.
   rewrite cardinal_set0 ; exact: card_lt_01.
by case: dn0; move/card_lt1: (conj aux2 aux).
Qed.


Exercise 5.7


Definition Noetherian r :=
  (forall X, sub X (substrate r) -> nonempty X ->
    exists a, maximal (induced_order r X) a).

Definition Noetherian_set r x:=
   sub x (substrate r) /\ Noetherian (induced_order r x).

Lemma Noetherian_set_pr r x: order r -> sub x (substrate r) ->
   (Noetherian_set r x <->
   (forall X, sub X x -> nonempty X ->
    exists2 a, inc a X & (forall x, inc x X -> gle r a x -> x = a))).
Proof.
move => or xsr; rewrite /Noetherian_set /Noetherian.
rewrite (iorder_sr or xsr); split.
  move => [_ h] X Xx xne; move: (h _ Xx xne);rewrite (iorder_trans _ Xx).
  move=> [a []]; rewrite (iorder_sr or (sub_trans Xx xsr)) => ax ap.
  by ex_tac; move => t tX lat; apply: ap; apply /iorder_gleP.
move => h; split; first by exact.
move => X Xx ne; rewrite (iorder_trans _ Xx); move: (h _ Xx ne) => [a ax ap].
exists a; split; first by rewrite (iorder_sr or (sub_trans Xx xsr)).
by move => b => /iorder_gle5P; move=> [_ bx ab]; apply: ap.
Qed.

Lemma Exercise6_29a r: order r ->
  Noetherian r -> Noetherian_set r (substrate r).
Proof.
move => or nr; split; [fprops | by rewrite (iorder_substrate or) ].
Qed.

Lemma Exercise6_29b r: Noetherian_set r emptyset.
Proof.
split; fprops.
move => X xns [w wx]; move: (xns _ wx).
have ->: (induced_order r emptyset) = emptyset.
  by apply /set0_P => y /setI2_P [_]/setX_P [_ /in_set0].
by rewrite /substrate domain_set0 range_set0 setU2_id => /in_set0.
Qed.

Lemma Exercise6_29c r a b: order r ->
  Noetherian_set r a -> Noetherian_set r b -> Noetherian_set r (a \cup b).
Proof.
move => or pa pb.
move: (proj1 pa) (proj1 pb) => asr bsr.
move: pa; rewrite (Noetherian_set_pr or asr) => pa.
move: pb; rewrite (Noetherian_set_pr or bsr) => pb.
have usr: sub (a \cup b) (substrate r)
  by move=> t; case /setU2_P; [apply asr | apply: bsr].
rewrite (Noetherian_set_pr or usr).
move => X Xu neX.
set Xa:= intersection2 X a.
case: (emptyset_dichot Xa) => Xane.
  have sb: sub X b.
    move => t tX; move: (Xu _ tX); case /setU2_P => // ta.
    empty_tac1 t; apply /setI2_P;split => //.
  by apply: pb.
have sxa: sub Xa a by apply: subsetI2r.
move: (pa _ sxa Xane) => [ea sea eap].
set Xb:= Zo X (fun t => glt r ea t).
case: (emptyset_dichot Xb) => Xbne.
  have eax: inc ea X by move: sea;move /setI2_P=> [].
  exists ea => //; move => x xE le1; ex_middle ne.
  by empty_tac1 x; apply: Zo_i => //;split => //; apply:nesym.
have sxb: sub Xb b.
  move => t /Zo_P [tx [le1 ne1]].
  move: (Xu _ tx);case /setU2_P=> // ta.
  have txa: inc t Xa by rewrite /Xa; fprops.
  by move: (eap _ txa le1) =>eq1; case: ne1.
move: (pb _ sxb Xbne) => [eb seb ebp].
have ebx: inc eb X by move: seb => /Zo_P [].
exists eb => //; move => x xE le1.
apply: ebp => //; apply: Zo_i => //.
move: seb => /Zo_P [_ lt1]; order_tac.
Qed.

Lemma Exercise6_29d r X: order r ->
  finite_set X ->
  (forall x, inc x X -> Noetherian_set r x) ->
  Noetherian_set r (union X).
Proof.
move => or; move: X.
apply: (finite_set_induction).
  move => _; rewrite setU_0; apply: Exercise6_29b.
move => a n Hrec aux.
have ->: union (a +s1 n) = (union a) \cup n.
  set_extens t.
    move => /setU_P [y ty] /setU1_P;
       case => h; apply /setU2_P; [ left;union_tac | right; ue].
  case /setU2_P.
      move /setU_P=> [y ty ya]; union_tac.
  by move => tn; apply /setU_P;exists n;fprops.
apply: (Exercise6_29c or); last by apply: aux; fprops.
apply: Hrec=> x xa; apply: aux; fprops.
Qed.

Lemma Exercise6_29e r X: order r -> Noetherian r ->
  sub X (substrate r) -> Noetherian_set r X.
Proof.
move => or Nr xsr.
rewrite (Noetherian_set_pr or xsr) => Y YX neY.
move: (sub_trans YX xsr) => Ysr.
move: (Nr _ Ysr neY) => [a []]. rewrite (iorder_sr or Ysr) => pa pb.
by ex_tac; move => x xY ax; apply: pb; apply /iorder_gleP.
Qed.

Lemma Exercise6_29f r: order r ->
 (Noetherian r <->
   (forall i, inc i (substrate r) -> Noetherian_set r (interval_ou r i))).
Proof.
move => or; split => h.
  by move => i isr; apply: (Exercise6_29e or h); apply: Zo_S.
move => X Xsr neX.
move: (neX) => [a aX].
case: (p_or_not_p (maximal (induced_order r X) a)) => ma.
  by exists a.
set Y := Zo X (fun z => glt r a z).
case: (emptyset_dichot Y) => neY.
  case: ma; split; first by rewrite (iorder_sr or Xsr).
  move => x /iorder_gle5P [_ pa pb].
  by ex_middle exa; empty_tac1 x; apply: Zo_i=> //; split => //; apply: nesym.
have sY: sub Y (interval_ou r a).
  move => y /Zo_P [yX ay]; apply /Zo_P; split => //; order_tac. fprops.
move: (h _ (Xsr _ aX)).
have Isr: sub (interval_ou r a) (substrate r) by apply: Zo_S.
rewrite (Noetherian_set_pr or Isr) => aux.
move: (aux _ sY neY) => [b ibY etc].
move: ibY => /Zo_P [bX ab].
exists b; split; first by rewrite (iorder_sr or Xsr).
move=> x /iorder_gle5P [_ xX bx].
apply: etc => //;apply /Zo_P; split => //; order_tac.
Qed.

Definition restriction_to_segmentA r x g :=
  [/\ order r, inc x (substrate r), function g& sub (segment r x) (source g)].

Lemma rts_function1 r x g: restriction_to_segmentA r x g ->
  function (restriction_to_segment r x g).
Proof.
move=> [p1 p2 p3 p4].
rewrite /restriction_to_segment; apply: (proj31 (restriction1_prop p3 p4)).
Qed.

Lemma rts_W1 r x g a: restriction_to_segmentA r x g ->
  glt r a x -> Vf (restriction_to_segment r x g) a = Vf g a.
Proof.
move=> [p1 p2 p3 p4] ax.
rewrite /restriction_to_segment; apply: restriction1_V =>//.
rewrite /segment/interval_uo; apply: Zo_i=>//; order_tac.
Qed.

Lemma rts_surjective1 r x g: restriction_to_segmentA r x g ->
  surjection (restriction_to_segment r x g).
Proof.
move=> [p1 p2 p3 p4].
rewrite /restriction_to_segment.
by apply: restriction1_fs.
Qed.

Lemma rts_extensionality1 r s x f g:
  order r -> inc x (substrate r) -> order s -> inc x (substrate s) ->
  segment r x = segment s x ->
  function f -> sub (segment r x) (source f) ->
  function g -> sub (segment s x) (source g) ->
  (forall a , inc a (segment r x) -> Vf f a = Vf g a) ->
  restriction_to_segment r x f = restriction_to_segment s x g.
Proof.
move=> wor xsr wos xss srsx ff srf fg ssg sv.
have rf: (restriction_to_segmentA r x f) by done.
have rg: (restriction_to_segmentA s x g) by done.
apply: function_exten =>//; try apply: rts_function1;
  try solve [rewrite /restriction_to_segment/restriction1; aw].
  rewrite /restriction_to_segment/restriction1; aw.
  set_extens t.
    move/(Vf_image_P ff srf)=> [u us Wu]; apply /(Vf_image_P fg ssg).
    by rewrite - srsx; ex_tac; rewrite - sv.
  move/(Vf_image_P fg ssg)=> [u us Wu]; apply /(Vf_image_P ff srf).
  by rewrite - srsx in us; ex_tac; rewrite sv.
move=> u;rewrite /restriction_to_segment/restriction1; aw.
move=> us.
have p1: glt r u x by apply: (inc_segment us).
have p2: glt s u x by rewrite srsx in us;apply: (inc_segment us); ue.
rewrite rts_W1 // rts_W1 // sv //.
Qed.

Lemma transfinite_unique11 r p f f' z: order r ->
  inc z (substrate r) ->
  transfinite_def r p f -> transfinite_def r p f' ->
  (forall x : Set, inc x (segment r z) -> Vf f x = Vf f' x) ->
  restriction_to_segment r z f = restriction_to_segment r z f'.
Proof.
move=> wo zsr [[ff _ ] sf Wf] [[ff' _] sf' Wf'] sW.
have ss: sub (segment r z) (substrate r) by apply: sub_segment.
apply: rts_extensionality1=> //; ue.
Qed.

Lemma inc_set_of_segments1 r x: order r ->
  inc x (segments r) -> segmentp r x.
Proof.
rewrite /segments/segmentss=> or.
case /setU1_P.
  by move /funI_P => [z zr ->]; apply: segment_segment=>//.
by move=> ->; apply: substrate_segment.
Qed.


Lemma Exercise_6_20b a:
   \2c <c a ->
   (forall m, \0c <c m -> m <c a -> a ^c m = a) -> regular_cardinal a.
Proof.
move => a2 h.
have ca: cardinalp a by co_tac.
case: (finite_dichot ca).
  move /BnatP => aB.
  move: (h _ card_lt_02 a2); rewrite cpowx2 => eq1.
  have aa: a <=c a by fprops.
  have anz: a <> \0c by move => eq2; rewrite eq2 in a2; case: (card_lt0 a2).
  move: (cprod_Mlelt aB aB aa a2 anz); rewrite eq1 => le1.
  move: (cprod_M1le ca card2_nz) => le2; co_tac.
move => ica; apply /regular_cardinalP; split; first by exact.
ex_middle ne1.
have sa: singular_cardinal a by split.
have pa: (cpow_less_ec_prop a a \1c).
  split; first by apply: finite_lt_infinite; fprops.
  move => b; rewrite (cpowx1 ca); move /card_ge1P => b1 ba.
  by rewrite (h _ b1 ba).
move: (cantor ca); rewrite - (infinite_power1_b ica).
move: (cpow_less_ec_pr3 pa (proj1 a2) sa) => [-> <-].
by rewrite (cpowx1 ca); move => [].
Qed.

Lemma Exercise_6_20c1 a:
   GenContHypothesis -> regular_cardinal a ->
   (forall m, \0c <c m -> m <c a -> a ^c m = a).
Proof.
move => gch /regular_cardinalP [ia ra] m [_ m0] ma.
move: (infinite_power10 gch m ia); move=> [_ pa _ _].
by apply: pa; [ apply:nesym | ue].
Qed.

Lemma Exercise_6_20c2:
  (forall a, regular_cardinal a ->
    (forall m, \0c <c m -> m <c a -> a ^c m = a)) ->
 GenContHypothesis.
Proof.
move => h.
move => t ict; move: (ict) => [ct _].
move: (ord_index_pr1 ict)=> [on tv].
move: (regular_initial_successor on).
rewrite - (succ_c_pr on) tv => rs.
move: (h _ rs _ (finite_lt_infinite finite_0 ict) (succ_c_pr2 ct)).
move => le1.
apply: card_leA; first by apply: (succ_c_pr3 ct).
have pa: \2c <=c succ_c t.
   rewrite -tv (succ_c_pr on).
   apply: (finite_le_infinite finite_2 (aleph_pr5c (OS_succ on))).
by rewrite -le1; apply: (cpow_Mleeq _ pa card2_nz).
Qed.

Lemma Exercise6_22c1 x:
   card_dominant x ->
   (x = omega0 \/ (exists2 n, limit_ordinal n & x = \aleph n)).
Proof.
move => [pa pb].
move: (ord_index_pr1 pa); set c := ord_index x; move => [pd pe].
case: (limit_ordinal_pr2 pd) => ln;last by right; exists c.
  by left; rewrite -pe ln aleph_pr1.
move: ln => [m om mv].
set y:= \aleph m.
have yx: y <c x.
  by rewrite /y -pe; apply: aleph_lt_ltc; rewrite mv; apply: ord_succ_lt.
move: (pb _ _ yx yx); rewrite (infinite_power1_b (aleph_pr5c om)) => le1.
move: (succ_c_pr3 (CS_aleph om));rewrite (succ_c_pr om) -mv pe => le2;co_tac.
Qed.

Lemma Exercise6_22c2 x
  (p1 := forall z, \0c <c z -> z <c x -> x ^c z = x)
  (p2:= forall z, \0c <c z -> x ^c z = x *c \2c ^c z):
  [/\ (infinite_c x -> p1 -> p2),
    (card_dominant x -> (p1 <-> p2)),
    (card_dominant x -> p1 -> (x = omega0 \/ inaccessible x)) &
    (x = omega0 \/ inaccessible x -> (card_dominant x /\ p1))].
Proof.
have r1:infinite_c x -> p1 -> p2.
  move=> icx hp1 z zp.
  move: (infinite_ge_two icx) => x2.
  move: (infinite_nz icx) => xnz.
  have cz: cardinalp z by co_tac.
  case: (card_le_to_ee (proj1 icx) (CS_pow \2c z)).
    move => le1.
    move: (ge_infinite_infinite icx le1) => icp.
    case: (finite_dichot cz) => icz.
      have f1: finite_c (\2c ^c z).
        by apply /BnatP; apply BS_pow; fprops; rewrite inc_Bnat.
      case: (infinite_dichot1 f1 icp).
    rewrite (infinite_power1 x2 le1 icz).
    by rewrite cprodC product2_infinite.
  have pnz: \2c ^c z <> \0c by apply: cpow2_nz.
  move => le1.
  rewrite (hp1 _ zp (card_lt_leT (cantor cz) le1)).
  rewrite product2_infinite //.
have r2: card_dominant x -> (p1 <-> p2).
  move=> [icx cdx]; split; first by apply: r1.
  move => hp2 z z0 zx.
  have pnz: \2c ^c z <> \0c by apply: cpow2_nz.
  move: (cdx _ _ (finite_lt_infinite finite_2 icx) zx) => [l1 _].
  rewrite (hp2 _ z0) product2_infinite //.
have r3: card_dominant x -> p1 -> x = omega0 \/ inaccessible x.
  move => pa pc; case: (Exercise6_22c1 pa); first by left.
  move => h; right.
  move: pa => [pa pb].
  split; last first.
    by move => t tx; apply: pb => //; apply: (finite_lt_infinite finite_2 pa).
  split; last by exact.
  move: (cofinality_c_small (infinite_ge_two pa)) => h1.
  split => //; ex_middle eq1.
  have pd: \0c <c cofinality_c x.
    apply: (finite_lt_infinite finite_0 (cofinality_infinite pa)).
  move: (power_cofinality (infinite_ge_two pa)).
  by rewrite (pc _ pd (conj h1 eq1)); move => [_].
split => //.
case => ix.
  rewrite ix; split; first by apply: card_dominant_pr2.
  move => z z0 zf.
  have pa: infinite_c x by rewrite ix; apply: omega_infinitec.
  have pb: inc z Bnat.
    by rewrite ix in zf; move:(ordinal_cardinal_lt zf) => /ord_ltP0 [_ _].
  have pc: z <> \0c by move: z0 => [_ /nesym].
  by rewrite power_of_infinite.
split; first by apply: inaccessible_dominant.
by move => z [_ zc] zx;apply: inaccessible_pr7 => //; apply:nesym.
Qed.


Exercise 6 33

Section Exercise6_33.
Variables a b E F: Set.
Hypothesis ha: \2c <=c a.
Hypothesis hb: \1c <=c b.
Hypothesis iab: infinite_c a \/ infinite_c b.
Hypothesis HF0: sub F (powerset E).
Hypothesis HF1: a ^c b <c cardinal F.
Hypothesis HF2: forall x, inc x F -> cardinal x <=c b.
Definition Ex6_33_conc:=
   exists G q, [/\ sub G F , a ^c b <c cardinal G &
   forall a b, inc a G -> inc b G -> a <> b -> intersection2 a b = q].

Lemma Exercise6_33a: infinite_c (a ^c b).
Proof.
have ca: cardinalp a by move: ha => [_ ca _].
have bnz : b <> \0c.
  move => bz;move: hb; rewrite bz => hb1; move: card_lt_01 => hb2; co_tac.
move: (cpow_Mleeq b ha card2_nz) => h1.
case iab => iiab; first by apply: infinite_pow => //.
exact: (ge_infinite_infinite (infinite_powerset iiab) h1).
Qed.

Definition E6_33_c := succ_c (a ^c b).
Definition E6_33_X :=
   choose (fun f => injection_prop f E6_33_c F).
Definition E6_33_M := unionb (Lg (source E6_33_X) (Vf E6_33_X)).

Lemma Exercise6_33b (d := (a ^c b)):
     [/\ d <c E6_33_c,
        (forall z, d <c z -> E6_33_c <=c z) &
        (forall z, z <c E6_33_c -> z <=c d)].
Proof.
move: (succ_c_pr1 (proj1 (Exercise6_33a))).
move => [pa pb pc]; split => // z; apply: succ_c_pr4; fprops.
Qed.

Lemma Exercise6_33c: infinite_c E6_33_c.
Proof.
move: Exercise6_33a Exercise6_33b => pb [[pa _] _ _].
by move: (ge_infinite_infinite pb pa).
Qed.

Lemma Exercise6_33d (f := E6_33_X):
  injection_prop f E6_33_c F.
Proof.
rewrite /f/ E6_33_X; apply choose_pr; apply eq_subset_ex_injP.
apply /eq_subset_cardP1.
move: ( Exercise6_33b)=> [[[_ cc _] _] pa _].
by rewrite (card_card cc);apply: pa.
Qed.

Lemma Exercise6_33e n: inc n E6_33_c -> sub (Vf E6_33_X n) E6_33_M.
Proof.
move => nc.
move: Exercise6_33d => [[fx ix] sx tx].
rewrite /E6_33_M => t tw; apply /setUb_P; bw; rewrite sx; ex_tac; bw.
Qed.

Lemma Exercise6_33f: cardinal E6_33_M = E6_33_c.
Proof.
have le: cardinal E6_33_M <=c E6_33_c.
  set f := (Lg (source E6_33_X) (fun z => Vf E6_33_X z)).
  have fx: fgraph f by rewrite /f; fprops.
  move: (csum_pr1 f); rewrite -/ E6_33_M; bw.
  set f1 := (Lg (domain f) (fun a0 : Set => cardinal (Vg f a0))).
  set g := cst_graph (source E6_33_X) b.
  have f1x: fgraph f1 by rewrite /f1/cst_graph; fprops.
  have gx: fgraph g by rewrite /g/cst_graph; fprops.
  have sd: domain f1 = domain g by rewrite /f1 /g /f /cst_graph; bw.
  move: Exercise6_33d => [[ff ijf] sf tf].
  have le1: (forall x, inc x (domain f1) -> Vg f1 x <=c Vg g x).
    rewrite /f1/f/g/cst_graph; bw => x xd; bw; apply: HF2.
    by rewrite -tf; Wtac.
  move: (csum_increasing sd le1).
  rewrite /g csum_of_same sf.
  have pd: b <=c E6_33_c.
    move: Exercise6_33b => [qa qb qc].
    apply: (card_leT (proj1 (cantor (proj32 hb)))).
    apply: card_leT (proj1 qa); apply: cpow_Mleeq => //; apply card2_nz.
  have bnz : b <> \0c.
    move => bz;move: hb; rewrite bz => hb1; move: card_lt_01 => hb2; co_tac.
  move: Exercise6_33c => pc.
  rewrite cprodC product2_infinite //.
  by move => le2 le3; co_tac.
ex_middle ne.
move: Exercise6_33b => [sa sb sc]; move: (sc _ (conj le ne)) => le1.
move: le => [_ cc _].
set T := (fun_image (functions b E6_33_M) image_of_fun) +s1 emptyset.
move: (Exercise6_33d) => [[fx ix] sx tx].
have pa: forall i, inc i E6_33_c -> inc (Vf E6_33_X i) T.
  move => i ic.
  rewrite - sx in ic.
  move: ((Vf_target fx) _ ic); rewrite tx => wf.
  move: (HF2 wf) => cl.
  case: (emptyset_dichot (Vf E6_33_X i)) => wne; first by rewrite wne /T; fprops.
  apply /setU1_P; left; aw.
  move: cl; rewrite - {1} (card_card (proj32 hb)) => le2.
  have [c cb ecb]: equipotent_to_subset (Vf E6_33_X i) b.
    apply /(eq_subset_cardP); exact: (cardinal_le_aux1 le2).
  have [f [bf sf tf]]: c \Eq Vf E6_33_X i by eqsym.
  pose g z := Yo (inc z c) (Vf f z) (rep (Vf E6_33_X i)).
  have pa: forall z, inc (g z) (Vf E6_33_X i).
    move => z; rewrite /g; Ytac zc; last by apply: rep_i.
    rewrite -tf; Wtac; fct_tac.
  have pb: forall z, inc z (Vf E6_33_X i) -> exists2 i, inc i b & g i = z.
    rewrite -tf; move=> z ztf; move: ((proj2 (proj2 bf)) _ ztf)=> [y ysf <-].
    rewrite sf in ysf; exists y; [by apply: cb | by rewrite /g; Ytac0].
  have pc: lf_axiom g b E6_33_M.
    move => z zb; move: (pa z) => i1; apply /setUb_P; bw; ex_tac; bw.
  set G := Lf g b E6_33_M.
  have fg: function G by apply: lf_function.
  have pd: inc G (functions b E6_33_M).
    by rewrite /G;apply /fun_set_P;split => //; aw.
  apply /funI_P;ex_tac; symmetry;set_extens t.
    move /(Vf_image_P1 fg) => [u usg ->].
      rewrite /G; aw; move: usg; rewrite /G;aw.
  move => tw; move: (pb _ tw) => [z zi <-]; apply /(Vf_image_P1 fg).
  exists z; rewrite /G; aw;split => //.
have : equipotent_to_subset E6_33_c T.
  rewrite eq_subset_ex_injP.
  exists (Lf (fun z => (Vf E6_33_X z)) E6_33_c T); split; aw.
  apply: lf_injective; first by apply: pa.
  rewrite - sx; apply: ix.
move /eq_subset_cardP1; rewrite (card_card cc) => eq1.
set T1:= fun_image (functions b E6_33_M) image_of_fun.
set aa:= (functions b E6_33_M); set ff:= image_of_fun.
have sj: (surjection (Lf ff aa (fun_image aa ff))).
  apply: lf_surjective.
    by move=> t ta; apply /funI_P;exists t.
  by move=> y /funI_P.
move: (image_smaller_cardinal (proj1 sj)).
move: (surjective_pr0 sj); aw; move => ->; rewrite /aa /ff -/T1.
rewrite cpow_pr1 (card_card (proj32 hb)).
have ->: cardinal T1 = cardinal T.
  case: (inc_or_not emptyset T1) => eT.
    by rewrite /T (setU1_eq eT).
  move: Exercise6_33c => i1.
  move: (ge_infinite_infinite Exercise6_33c eq1) => it.
  have pb: cardinal T = succ (cardinal T1) by rewrite /T -/T1 (card_succ_pr eT).
  case: (finite_dichot (CS_cardinal T1)).
      move/ (finite_succP (CS_cardinal T1)); rewrite - pb => nit.
      case: (infinite_dichot1 nit it).
  by move /infinite_cP; rewrite - pb; move => [_].
move => l2; move: (card_leT eq1 l2).
have bnz : b <> \0c.
  move => bz;move: hb; rewrite bz => hb1; move: card_lt_01 => hb2; co_tac.
case: (equal_or_not (cardinal E6_33_M) \0c) => mz.
  by rewrite mz (cpow0x bnz) => h; symmetry; apply: card_le0.
move: (cpow_Mleeq b le1 mz); rewrite - cpow_pow.
suff ->: a ^c (b *c b) = a ^c b.
    by move => l1 l3; move: (card_leT l3 l1) => l4; co_tac.
case: (finite_dichot (proj32 hb)) => fb.
  move: fb => /BnatP => fb.
  move: (BS_prod fb fb) => fb2.
  case: iab => fa.
  rewrite (power_of_infinite fa fb2 (cprod2_nz bnz bnz)).
  by rewrite (power_of_infinite fa fb bnz).
  by rewrite square_of_infinite.
by rewrite square_of_infinite.
Qed.

Definition E6_33_x:= choose (fun z => bijection_prop z E6_33_c E6_33_M).
Definition E6_33_r :=
  image_by_fun (ext_to_prod E6_33_x E6_33_x) (ordinal_o E6_33_c).
Definition E6_33_rho n := ordinal (induced_order E6_33_r (Vf E6_33_X n)).

Lemma Exercise6_33g : bijection_prop E6_33_x E6_33_c E6_33_M.
Proof.
move: Exercise6_33f.
rewrite -{1} (card_card (proj1 Exercise6_33c)) => h.
by rewrite /E6_33_x; apply choose_pr; eqsym; apply /card_eqP.
Qed.

Lemma Exercise6_33h (x := E6_33_x) (r:= E6_33_r) (c := E6_33_c):
  [/\ worder_on r E6_33_M,
  order_isomorphism x (ordinal_o E6_33_c) r &
  (forall a b, inc a c -> inc b c ->
     (a <=o b <-> gle r (Vf x a) (Vf x b)))].
Proof.
move: (proj1 (proj1 Exercise6_33c)) => oc.
move: (ordinal_o_wor oc) => wo1; move: (wo1) => [o1 _].
move: (ordinal_o_sr E6_33_c) => sr1.
move: Exercise6_33g; rewrite -/x; move => [bx sx tx].
rewrite -{2} sx in sr1.
move: (order_transportation bx o1 sr1); rewrite /x -/ E6_33_r -/r => oi1.
move: (oi1) => [_ or [_ _ sr2] xinc].
red in xinc; rewrite tx in sr2; rewrite sx in xinc.
have wo: worder r by apply: worder_invariance wo1; exists E6_33_x.
split => //.
move => u v ux vx; rewrite - (xinc _ _ ux vx); split.
  move => [_ _ h]; apply /ordo_leP;split => //.
move /ordo_leP => [_ _ h]; split => //; ord_tac0.
Qed.

Lemma Exercise6_33i n: inc n E6_33_c ->
  [/\ worder (induced_order E6_33_r (Vf E6_33_X n)),
   ordinalp (E6_33_rho n) & cardinal (E6_33_rho n) <=c b].
Proof.
move => ni; rewrite /E6_33_rho.
set r := induced_order _ _.
move: Exercise6_33h => [[wo1 sr] oi oie].
move: Exercise6_33d => [[fx ix] sx tx].
have wr: inc (Vf E6_33_X n) F by rewrite -tx; Wtac.
move: (Exercise6_33e ni); rewrite - sr => pa.
have wor: worder r by move: (induced_wor wo1 pa).
split; first (by exact);first by apply: OS_ordinal.
rewrite (cardinal_of_ordinal wor) (iorder_sr (proj1 wo1) pa).
by apply: HF2.
Qed.

Definition E6_33_y n := the_ordinal_iso (induced_order E6_33_r (Vf E6_33_X n)).
Definition E6_33_Mi m := Zo E6_33_M
    (fun z => exists n, [/\ inc n E6_33_c, inc m (source (E6_33_y n)) &
      z = Vf (E6_33_y n) m]).
Definition E6_33_al :=
   intersection (Zo (a ^c b) (fun m => (cardinal (E6_33_Mi m) = E6_33_c))).

Lemma Exercise6_33j n
    (yn := E6_33_y n) (r := induced_order E6_33_r (Vf E6_33_X n)):
  inc n E6_33_c ->
    [/\ order_isomorphism yn (ordinal_o (E6_33_rho n)) r,
     source yn = E6_33_rho n & target yn = (Vf E6_33_X n)].
Proof.
move=> nc.
have pa: order_isomorphism yn (ordinal_o (E6_33_rho n)) r.
  by apply: the_ordinal_iso1; move: (Exercise6_33i nc) => [].
move: (pa) => [_ _ [_ sf tf] _].
move: (Exercise6_33i nc) => [pd pb pc].
rewrite sf tf.
move: (Exercise6_33h) => [[pe pf] _ _].
have pg: sub (Vf E6_33_X n) (substrate E6_33_r).
  by rewrite pf; apply: Exercise6_33e.
by rewrite ordinal_o_sr /r (iorder_sr (proj1 pe)).
Qed.

Lemma Exercise6_33k n: inc n E6_33_c ->
  ((forall t, inc t (E6_33_rho n) -> t <o a ^c b)
    /\ sub (E6_33_rho n) E6_33_c).
Proof.
move=> ns.
move: Exercise6_33b => [sa sb sc].
have le1: b <c a ^c b.
  apply: card_lt_leT (cpow_Mleeq b ha card2_nz).
  exact (cantor (proj32 hb)).
move: (Exercise6_33i ns) => [_ qa qb].
move: (card_le_ltT qb le1).
move/(ordinal_cardinal_le2P (CS_pow a b) qa) => h.
split.
  move => t /(ord_ltP qa) [pa _]; ord_tac.
have o3: ordinalp E6_33_c by exact (proj1 (proj1 Exercise6_33c)).
move: h sa => [[_ _ s1] _] [[_ _ s2] _].
apply: (sub_trans s1 s2).
Qed.

Lemma Exercise6_33l: E6_33_M = unionb (Lg (a ^c b) E6_33_Mi).
Proof.
set_extens x.
  move: Exercise6_33d => [[fc ix] sx tx].
  move => xM; move: (xM) => /setUb_P; bw; move => [y ys]; bw => xW.
  rewrite sx in ys.
  move: (Exercise6_33j ys) => [[o1 o2 [bf sf tf] _] sy ty].
  rewrite - ty in xW.
  move: (proj2 (proj2 bf) _ xW) => [n ns xv].
  move: ( Exercise6_33k ys) => [s1 s2].
  rewrite - sy in s1; move: (s1 _ ns) => ns1.
  move: (s1 _ ns) => /(ord_ltP (proj32_1 ns1)) np.
  apply /setUb_P; exists n=> //; bw; apply: Zo_i; first by exact.
  exists y; split => //.
by move /setUb_P; bw;move => [y yp]; bw => /Zo_P [].
Qed.

Lemma Exercise6_33m x (c:= cardinal (E6_33_Mi x)):
  inc x (a ^c b) -> c <=c (a ^c b) \/ c = E6_33_c.
Proof.
move: Exercise6_33l => eq1 xs.
have s1: sub (E6_33_Mi x) E6_33_M.
   move =>t ti; rewrite eq1; apply /setUb_P; bw; ex_tac; bw.
move: (sub_smaller s1); rewrite Exercise6_33f => le1.
move:(Exercise6_33b) => [pa pb pc].
by case: (equal_or_not c E6_33_c) => cc; [ right | left; apply: pc; split].
Qed.

Lemma Exercise6_33n: exists2 m,
  m <o (a ^c b) & (cardinal (E6_33_Mi m)) = E6_33_c.
Proof.
ex_middle pa.
have le1: forall x, inc x (a ^c b) -> cardinal (E6_33_Mi x) <=c (a ^c b).
  move=> x xab; case: (Exercise6_33m xab) => // e1; case: pa; exists x => //.
  have oab: ordinalp (a ^c b) by move: (CS_pow a b) => [].
  by move: xab => /(ord_ltP oab).
set f := (Lg (a ^c b) E6_33_Mi).
move: (csum_pr1 f); rewrite /f -/E6_33_M - Exercise6_33l Exercise6_33f.
rewrite /card_sumb;bw.
set f1 := Lg _ _.
set f2 := cst_graph (a ^c b) (a ^c b).
have fgf1: fgraph f1 by rewrite /f1; fprops.
have fgf2: fgraph f2 by rewrite /f2/cst_graph; fprops.
have sd: domain f1 = domain f2 by rewrite /f1/f2/cst_graph; bw.
have pb: (forall x, inc x (domain f1) -> Vg f1 x <=c Vg f2 x).
  by rewrite /f1/f2/cst_graph;bw => x xa; bw; apply: le1.
move: (csum_increasing sd pb).
rewrite /f2 csum_of_same (square_of_infinite Exercise6_33a).
move => l1 l2; move: (card_leT l2 l1) => l3.
move: (Exercise6_33b) => [l4 _ _]; co_tac.
Qed.

Lemma Exercise6_33o (al:= E6_33_al):
  [/\ al <o (a ^c b), (cardinal (E6_33_Mi al) = E6_33_c) &
  (forall m, m <o al -> cardinal (E6_33_Mi m) <=c (a ^c b))].
Proof.
rewrite /al /E6_33_al; set Z := Zo _ _.
have oab: ordinalp (a ^c b) by move: (CS_pow a b) => [].
have nez: nonempty Z.
   move: Exercise6_33n => [m [m1 m2]]; exists m; apply: Zo_i=> //.
   by apply/(ord_ltP oab).
have oz: ordinal_set Z by move=> t => /Zo_P [tab _]; ord_tac0.
move: (ordinal_setI nez oz); set c := intersection Z => cz.
move: (cz) => /Zo_P [pa pb].
have lt: c <o a ^c b by apply /(ord_ltP oab).
split => //.
move => m mc; move: (ord_lt_leT mc (proj1 lt)).
move/(ord_ltP oab) => mab.
case: (Exercise6_33m mab) => // eq1.
move: mc => /(ord_ltP (oz _ cz)) mc.
have mz: inc m Z by apply: Zo_i.
case: (ordinal_irreflexive (oz _ mz) (setI_hi mc mz)).
Qed.

Lemma Exercise6_33p:
   cardinal (unionb (Lg E6_33_al E6_33_Mi)) <=c a ^c b.
Proof.
set f := Lg _ _.
move: (csum_pr1 f); rewrite /card_sumb.
set f1 := Lg _ _.
set f2 := cst_graph E6_33_al (a ^c b).
have fgf1: fgraph f1 by rewrite /f1; fprops.
have fgf2: fgraph f2 by rewrite /f2/cst_graph; fprops.
have sd: domain f1 = domain f2 by rewrite /f1/f/f2/cst_graph; bw.
have pb: (forall x, inc x (domain f1) -> Vg f1 x <=c Vg f2 x).
  rewrite /f1/f/f2/cst_graph; bw => x xa; bw.
  move: Exercise6_33o=> [[[oa _] _] _ _]; apply.
  by apply /(ord_ltP oa).
move: (csum_increasing sd pb).
move => l1 l2; move: (card_leT l2 l1).
move: Exercise6_33o=> [[pa _] _ _].
rewrite /f2 csum_of_same => l3; apply: (card_leT l3).
move: (ordinal_cardinal_le1 pa); rewrite (card_card (CS_pow a b)) => le3.
rewrite - cprod2_pr2b; apply: (product2_infinite1 le3 Exercise6_33a).
Qed.

Definition E6_33_N0 := fun_image (E6_33_Mi E6_33_al)
   (fun t => rep (Zo E6_33_c
      (fun n => inc E6_33_al (source (E6_33_y n))
               /\ Vf (E6_33_y n) E6_33_al = t))).

Lemma Exercise6_33q (N0 := E6_33_N0) (al := E6_33_al)
  (Ma := E6_33_Mi E6_33_al):
  [/\ forall t, inc t N0 ->
   [/\ inc t E6_33_c, inc al (source (E6_33_y t))& inc (Vf (E6_33_y t) al) Ma],
    (forall t1 t2, inc t1 N0 -> inc t2 N0 ->
      (Vf (E6_33_y t1) al) = (Vf (E6_33_y t2) al) -> t1 = t2),
    (forall s, inc s Ma -> exists2 t, inc t N0 & s = (Vf (E6_33_y t) al)),
    sub N0 E6_33_c &
  cardinal N0 = E6_33_c].
Proof.
pose Z z := Zo E6_33_c
         (fun n : Set =>
          inc E6_33_al (source (E6_33_y n)) /\ Vf (E6_33_y n) E6_33_al = z).
have znz: forall z, inc z (E6_33_Mi E6_33_al) -> nonempty (Z z).
  move => z => /Zo_P [zM [n [nc als zv]]].
    by exists n; apply: Zo_i.
have pa: forall t, inc t N0 ->
  [/\ inc t E6_33_c, inc al (source (E6_33_y t)) & inc (Vf (E6_33_y t) al) Ma].
  move => t /funI_P [z z1 rz].
 move: (rep_i (znz _ z1)); rewrite rz; move /Zo_P => [pa [pb pc]].
 split => //; rewrite pc //.
have pb: (forall t1 t2, inc t1 N0 -> inc t2 N0 ->
      (Vf (E6_33_y t1) al) = (Vf (E6_33_y t2) al) -> t1 = t2).
  move => t1 t2 t1n t2n sv.
  move: t1n => /funI_P [z z1 rz].
  move: (rep_i (znz _ z1)); rewrite rz; move => /Zo_hi [_ pc].
  move: t2n => /funI_P [z' z1' rz'].
  move: (rep_i (znz _ z1')); rewrite rz'; move /Zo_hi => [_ pc'].
  by move: pc pc' sv; rewrite - {1}rz - {1} rz' -/al => -> -> ->.
have pc: (forall s, inc s Ma -> exists2 t, inc t N0 & s = Vf (E6_33_y t) al).
  move => s sm.
  set u := rep (Z s).
   have un: inc u N0 by apply /funI_P; rewrite -/Ma; exists s => //.
   exists u => //.
   by move: (rep_i (znz _ sm)) => /Zo_P [_ [_ ->]].
split => //.
  by move => t tn; move: (pa _ tn) => [ok _].
set f:= Lf (fun t => Vf (E6_33_y t) al) N0 Ma.
have bf: bijection f.
  by apply: lf_bijective => // t ta; move: (pa _ ta) => [_ _ ok].
have: (source f \Eq target f) by exists f; split => //.
rewrite /f; aw; move /card_eqP.
by move: Exercise6_33o => [_ -> _].
Qed.

End Exercise6_33.

End Exercise6.

The von Neuman ordinals

Module VonNeumann.

A numeration is a functional graph f such that f(x) is the set of all f(y) where y<x for r. A set is numerable if well-ordered and there is a numeration.

Definition numeration r f:=
  [/\ fgraph f, domain f = substrate r &
  forall x, inc x (domain f) -> Vg f x = direct_image f (segment r x)].
Definition numerable r :=
   worder r /\ exists f, numeration r f.
Each set has at most one numeration
Lemma direct_image_exten f f' a:
  fgraph f -> fgraph f' -> (forall x, inc x a -> Vg f x = Vg f' x) ->
  sub a (domain f) -> sub a (domain f') ->
  direct_image f a = direct_image f' a.
Proof.
move=> fgf fgf' sVVg adf adf'.
set_extens x; move /dirim_P => [u us Jg]; apply /dirim_P; ex_tac.
    move: (pr2_V fgf Jg); aw; move=> ->; rewrite (sVVg _ us).
    by apply: fdomain_pr1 =>//; apply: adf'.
move: (pr2_V fgf' Jg); aw; move=> ->; rewrite -(sVVg _ us).
by apply: fdomain_pr1 =>//; apply: adf.
Qed.

Lemma numeration_unique r f f':
  worder r -> numeration r f -> numeration r f' -> f = f'.
Proof.
move=> [or wor] [fgf df Vf][fgf' df' Vf'].
set A :=Zo (substrate r)(fun x=> Vg f x <> Vg f' x).
case: (emptyset_dichot A)=> neA.
  apply: fgraph_exten=>//; try ue.
  rewrite df=> a xdf.
  by ex_middle nVV; empty_tac1 a; rewrite /A; apply: Zo_i.
have sAs: sub A (substrate r) by apply: Zo_S.
move: (wor _ sAs neA)=> [y []]; aw => yA leyA.
move: (sAs _ yA)=> ysr.
have srp: forall z, inc z (segment r y) -> Vg f z = Vg f' z.
  move=> z /segmentP zy.
  ex_middle nVV.
  have zA: (inc z A) by rewrite /A; apply: Zo_i=>//; order_tac.
  move: (iorder_gle1 (leyA _ zA)) => yz; order_tac.
have nyA: Vg f y = Vg f' y.
  rewrite df in Vf; rewrite df' in Vf'.
  rewrite Vf // Vf' //.
  apply: direct_image_exten =>//.
    rewrite df; apply: sub_segment.
    rewrite df'; apply: sub_segment.
move: yA => /Zo_P [_ cnyA]; contradiction.
Qed.

A numeration of a segment is obtained by restriction

Lemma sub_numeration r f x:
  let r' := induced_order r (segment r x) in
  worder r -> numeration r f -> inc x (substrate r) ->
  numeration r' (restr f (segment r x)).
Proof.
move=> r' wor num xsr.
move: (@sub_segment r x)=> sss.
move: (induced_wor wor sss)=> wor'.
move: num=> [fgf df pf].
have sr':substrate r' = (segment r x) by rewrite /r'; aw; fprops.
have dr:domain (restr f (segment r x)) = substrate r' by bw.
have ssd: sub (segment r x) (domain f) by ue.
split;fprops.
rewrite dr sr'; move=> a asr.
have sra: (segment r' a = (segment r a)).
  rewrite /r'; apply: segment_induced_a =>//; fprops.
  apply: segment_segment; fprops.
rewrite sra restr_ev // pf; try ue.
have ssad: sub (segment r a) (domain f).
   move => w /segmentP; rewrite df => wlt; order_tac.
have sax: sub (segment r a) (segment r x).
  move=> t; move: asr => /segmentP p1 /segmentP p2.
  have or: order r by fprops.
  apply /segmentP;order_tac.
apply: direct_image_exten; try rewrite dr sr'//; fprops.
move=> z zs; rewrite restr_ev => //.
by apply: sax.
Qed.

If all segments are numerable so is the whole set

Lemma segments_numerables r:
  let r' := fun x => induced_order r (segment r x) in
  worder r -> (forall x, inc x (substrate r)-> numerable (r' x)) ->
  numerable r.
Proof.
move=> r' wor aln.
set f:= (fun x => choose (fun y=> numeration (r' x) y)).
have fp: forall x, inc x (substrate r) -> numeration (r' x) (f x).
  by move=> x xsr; move: (aln _ xsr)=> [_ c];rewrite /f;apply: choose_pr.
set g:= fun x => range (f x).
have or: order r by fprops.
have restrp: forall x y, glt r y x ->
   f y = restr (f x) (substrate (r' y)).
  move=> x y ryx.
  have sss: sub (segment r x) (substrate r) by apply: sub_segment.
  have ssy: sub (segment r y) (substrate r) by apply: sub_segment.
  have p6: worder (r' y) by rewrite /r'; apply: induced_wor =>//.
  apply: (numeration_unique p6); first by apply: fp; order_tac.
  have <-: (segment (r' x) y) = (substrate (r' y)).
    rewrite /r'; aw; try apply: sub_segment; rewrite segment_induced //.
  have p1: worder (r' x) by rewrite /r'; apply: induced_wor =>//.
  have p2: numeration (r' x) (f x) by apply: fp; order_tac.
  have p3: inc y (substrate (r' x)) by rewrite /r'; aw; apply /segmentP.
  move: (sub_numeration p1 p2 p3) => p5.
  have di: induced_order (r' x) (segment (r' x) y) = r' y.
    rewrite /r' segment_induced // iorder_trans //.
    apply: segment_monotone =>//; order_tac.
  by rewrite di in p5.
have gp: forall x y, inc x (substrate r) -> glt r y x -> g y = Vg (f x) y.
  move=> x y xsr yx; rewrite/g.
  have ysr: (inc y (substrate r)) by order_tac.
  move: (fp _ xsr) => [fg df vf].
  move: df; rewrite /r' ; aw => df; last by apply: sub_segment.
  have ysrx: (inc y (segment r x)) by apply /segmentP.
  rewrite df in vf; rewrite (vf _ ysrx). rewrite (restrp _ _ yx).
  have p0: (segment (r' x) y) = (substrate (r' y)).
    rewrite /r'; aw; try apply: sub_segment; rewrite segment_induced //.
  rewrite p0.
  have gr: sgraph (restr (f x) (substrate (r' y))) by fprops.
  have fgr: fgraph (restr (f x) (substrate (r' y))) by fprops.
  have hh: sub (substrate (r' y)) (domain (f x)).
    rewrite df; rewrite /r' (iorder_sr or (@sub_segment r y)).
    apply:(segment_monotone or (proj1 yx)).
  set_extens u.
    move /(range_gP fgr); bw; move => [z pa pb]; apply /dirim_P; exists z => //.
    by move: pb; bw => ->; apply:(fdomain_pr1 fg); apply: hh.
  move /dirim_P => [z za zb];apply /(range_gP fgr); exists z; bw.
  move: (pr2_V fg zb); aw.
split =>//; exists (Lg (substrate r) g).
red; bw; split;fprops.
move=> x xsr; bw; rewrite {1} /g.
move: (fp _ xsr) => [ff df vf].
 move: df; rewrite /r' ; aw => df; last by apply: sub_segment.
have gf: sgraph (f x) by fprops.
have p0: sub (segment r x) (substrate r) by apply: sub_segment.
have fgL: fgraph (Lg (substrate r) g) by fprops.
set_extens t.
  move=> /(range_gP ff) [z pa pb]; apply /dirim_P; exists z; first ue.
  move: pa; rewrite df => /segmentP h; rewrite pb - (gp _ _ xsr h); apply: Lg_i.
  order_tac.
move /dirim_P => [z xs JL]; move: (p0 _ xs) => zs.
move /segmentP: (xs) => lt1.
move: (pr2_V fgL JL); aw; bw => ->; rewrite (gp _ _ xsr lt1).
by apply /(range_gP ff); exists z => //; ue.
Qed.

Any well-ordered is numerable

Lemma worder_numerable r:
  worder r -> numerable r.
Proof.
move=> wor; apply: segments_numerables =>//.
move=> x xsr.
set r' := fun x => induced_order r (segment r x).
set (A:= Zo (substrate r)(fun z=> ~numerable (r' z))).
case: (p_or_not_p (numerable (induced_order r (segment r x)))) =>//.
move => h.
have sA: (sub A (substrate r)) by rewrite /A; apply: Zo_S.
have neA: nonempty A by exists x; apply/Zo_P.
move: (wor)=> [or aux]; move: (aux _ sA neA)=> [y []]; aw=> ys yp.
have rec: forall z, glt r z y -> numerable (r' z).
  move=>z zy; case: (p_or_not_p (numerable (r' z))) =>// nnz.
  have zA: (inc z A) by rewrite /A; apply: Zo_i=>//; order_tac.
  move: (iorder_gle1 (yp _ zA)) => yz; order_tac.
move: ys => /Zo_P [ys ny]; case: ny.
have sss: sub (segment r y) (substrate r) by apply: sub_segment.
apply: segments_numerables.
  rewrite /r'; apply: induced_wor =>//.
rewrite /r'; aw; move=> z zy.
have rzy: glt r z y by apply /segmentP.
rewrite segment_induced // iorder_trans //.
   by apply: rec.
apply: segment_monotone =>//; order_tac.
Qed.

The previous result is obvious by transfinite_defined
Definition the_numeration r := transfinite_defined r target.

Lemma worder_numerable_bis r:
  worder r -> numeration r (graph (the_numeration r)).
Proof.
move=> wor.
move: (transfinite_defined_pr target wor) => [suf sf vf].
set f := (transfinite_defined r target).
have ff: function f by fct_tac.
have dg: (domain (graph f) = substrate r) by rewrite f_domain_graph.
split;fprops.
rewrite dg.
move=> x xsr; move: (vf _ xsr); rewrite /Vf; move=> ->.
rewrite /restriction_to_segment/ restriction1; aw.
Qed.

End VonNeumann.



Require Import ssete2 sset10b.

Lemma BZdvd_latticeD: distributive_lattice1 BZdvdordering.
Proof.
suff: forall a b g z, inc a BZps -> inc b BZps -> inc g BZps -> inc z BZps ->
 BZ_Bezout a b -> BZgcd z ((a *z b) *z g) %|z BZlcm (g *z a) (BZgcd (g *z b) z).
move => h.
  apply:(proj32 (Exercise1_16b BZdvd_lattice)).
  apply /(Exercise1_16cP BZdvd_lattice).
  move => x y z; rewrite BZdvdordering_sr => xs ys zs.
  rewrite (BZdvd_inf ys zs) (BZdvd_sup xs ys).
  move: (BZpsS_gcd ys zs) (BZpsS_lcm xs ys) (BZpsS_gcd xs ys)=> gs ls g1s.
  rewrite (BZdvd_inf zs ls) (BZdvd_sup xs gs).
  apply /BZdvdordering_gle; split; first by apply: (BZpsS_gcd zs ls).
    by apply: (BZpsS_lcm xs gs).
  move /BZps_iP: (xs)=> [xp xnz]; move: (sub_BZp_BZ xp) => xz.
  move /BZps_iP: (ys)=> [yp ynz]; move: (sub_BZp_BZ yp) => yz.
  move /BZps_iP: (g1s)=> [g1p g1nz]; move: (sub_BZp_BZ g1p) => g1z.
  move: (BZ_exists_Bezout3 xz yz (or_introl (y <> \0z) xnz)).
  move: (BZpS_quo xp g1p) (BZpS_quo yp g1p).
  rewrite (proj33 (BZlcm_prop1 xz yz)).
  move: (BZgcd_div xz yz) => [].
  set a := (x %/z BZgcd x y); set b := (y %/z BZgcd x y); set g := BZgcd x y.
  move => e1 e2 az bz; rewrite e1 e2.
  have ap: inc a BZps.
    by apply/BZps_iP; split => // aez; case: xnz; rewrite e1 aez; qw.
  have bp: inc b BZps.
    by apply/BZps_iP; split => // aez; case: ynz; rewrite e2 aez; qw.
  by apply: h.
move => a b g z azp bzp gzp zzp bzt.
set t := BZgcd g z.
move: (BZpsS_gcd gzp zzp); rewrite -/t => /BZps_iP [tp tnz].
move: (sub_BZps_BZ gzp) (sub_BZp_BZ tp) => gz tz.
move: (sub_BZps_BZ azp)(sub_BZps_BZ bzp)(sub_BZps_BZ zzp) => az bz zz.
move /BZps_iP: gzp => [gp gnz]; move /BZps_iP: azp => [ap anz].
move /BZps_iP: bzp => [_ bnz]; move: (BZSp az bz) => abz.
move: (BZSp gz az) (BZS_gcd (BZSp gz bz) zz) => pa pb.
move: (BZgcd_div gz zz).
move: (BZ_exists_Bezout3 gz zz (or_introl (z <> \0z) gnz)).
set g' := (g %/z t); set z' := (z %/z t); move => bz1 [eq1 eq2].
move: (BZS_quo gz tz) (BZS_quo zz tz); rewrite -/g' -/z'; move => g'z z'z.
move: (BZSp abz g'z) => abgz.
move: (BZS_gcd z'z bz) => gs1.
have ->: BZgcd z ((a *z b) *z g) = t *z BZgcd z' ((a *z b) *z g').
  rewrite eq1 {1} eq2 -/t (BZprodC _ g').
  rewrite (BZprodA abz g'z tz) (BZprodC _ t).
  rewrite (BZgcd_prodD z'z abgz tp); reflexivity.
have cp1:BZ_coprime z' g'
   by rewrite /BZ_coprime BZgcd_C;apply: (BZ_exists_Bezout2 g'z z'z bz1).
have ->: BZgcd z' ((a *z b) *z g') = BZgcd z' ((a *z b)).
   rewrite BZprodC; apply: (BZgcd_simp z'z g'z abz cp1).
move: (BZlcm_prop1 pa pb) => [_ _ ->].
have ->: BZgcd (g *z a) (BZgcd (g *z b) z) = t.
  rewrite /t (BZgcd_A (BZSp gz az)(BZSp gz bz) zz).
  rewrite (BZgcd_prodD az bz gp).
  move: (BZ_exists_Bezout2 az bz bzt); rewrite /BZ_coprime => ->.
  by rewrite (BZprod_1r gz).
have ->: ((g *z a) %/z t) = g' *z a.
  rewrite eq1 -/t.
  rewrite - (BZprodA tz (BZS_quo gz tz) az).
  by rewrite (BZdvds_pr5 tz (BZSp g'z az) tnz).
have ->: (BZgcd (g *z b) z %/z t) = BZgcd z' b.
  move: (BZSp g'z bz) => h.
  rewrite eq2 {1} eq1 -/t - (BZprodA tz g'z bz) (BZgcd_prodD h z'z tp) BZgcd_C.
  by rewrite (BZgcd_simp z'z g'z bz cp1) (BZdvds_pr5 tz gs1 tnz).
suff: BZgcd z' (a *z b) %|z ((g' *z a) *z BZgcd z' b).
  rewrite (BZprodC t).
  move: (BZS_gcd z'z abz) (BZSp (BZSp g'z az) (BZS_gcd z'z bz)) => r1 r2.
  by move/ (BZdvds_prod r1 r2 tz tnz).
rewrite - (BZprodA g'z az gs1).
apply: (@BZdvds_trans (a *z BZgcd z' b)).
  apply: (BZdvds_pr1 g'z (BZSp az gs1)); apply:BZprod_nz => //.
  by move => h1; move: (BZgcd_nz z'z bz h1) => [aa bb]; case: bnz.
rewrite - (BZgcd_prodD z'z bz ap).
have h1:(z' <> \0z \/ a *z b <> \0z) by right; apply:BZprod_nz.
have h2:((a *z z') <> \0z \/ a *z b <> \0z) by right; apply:BZprod_nz.
move: (BZgcd_prop3 z'z abz h1)=> [[p1 p2 _ ] _].
move: (BZgcd_prop3 (BZSp az z'z) abz h2)=> [[_ _ p3] _ ].
apply: p3; last by apply: p2.
apply: (@BZdvds_trans z'); last by exact.
apply: (BZdvds_pr1 az z'z).
by move => h; move /BZps_iP:zzp => [_]; rewrite eq2 h; qw.
Qed.

Module OrderType.

Bourbaki Exercices Order Types


Lemma oprod0r' x: ordinalp x -> x *o \0o = \0o.
Proof.
by move => ox; rewrite (oprod_rec_def ox OS0) setX_0r funI_set0.
Qed.

Lemma oprod0l' x: ordinalp x -> \0o *o x = \0o.
Proof.
by move => ox; rewrite (oprod_rec_def OS0 ox) setX_0l funI_set0.
Qed.

Lemma osum_assoc2 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=> oa ob oc.
have oab: order (order_sum2 a b) by fprops.
have obc: order (order_sum2 b c) by fprops.
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 ! orsum2_sr.
have Fv: F = canonical_du2 (canonical_du2 A B) C.
  by rewrite /F ! orsum2_sr.
move: TP_ne1 => nT.
move: TP_ne => nT1.
set f := fun z => Yo (Q z = C0) (J (J (P z) C0) C0)
          (Yo (Q (P z) = C0) (J (J (P (P z)) C1) C0) (J (P (P z)) C1)).
have p1: forall x, inc x E -> inc (f x) F.
  move => x; rewrite Ev Fv; move /candu2P => [px]; case.
   by move=> [PA Qa]; rewrite /f; Ytac0; apply: candu2_pra; apply: candu2_pra.
  move => [] /candu2P [pPx alt] Qb.
  have nQa: Q x <> C0 by rewrite Qb.
  rewrite /f; Ytac0.
  case: alt;move => [Ppx Qpx].
   by Ytac0; apply: candu2_pra; apply: candu2_prb.
   rewrite (Y_false); [ apply: candu2_prb => // | rewrite Qpx; fprops].
have p2: forall y, inc y F -> exists2 x, inc x E & y = f x.
  move => y; rewrite Ev Fv; move /candu2P => [px]; case.
    move=> [] /candu2P [pPy aux] Qpy; case: aux.
      move=> [PPa QP]; exists (J (P (P y)) C0).
        by apply: candu2_pra.
      rewrite /f pr2_pair; Ytac0; aw.
      apply: pair_exten =>//; fprops; aw; try ue.
    move=> [PPy QPy]; exists (J (J (P (P y)) C0) C1).
      by apply: candu2_prb; apply: candu2_pra.
    rewrite /f !(pr1_pair, pr2_pair); Ytac0; Ytac0.
    apply: pair_exten =>//; fprops; aw; try ue.
  move=> [Py Qy]; exists (J (J (P y) C1) C1).
     by apply: candu2_prb; apply: candu2_prb.
   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; move /candu2P => [px hx] /candu2P [py hy].
  rewrite /f;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;case: nT1; exact: (pr2_def(pr1_def h2)).
       move => h2;case: nT1; exact: (pr2_def h2).
   move => [] /candu2P [pPx auxx] Qx; rewrite Qx; Ytac0.
   case: hy.
     move=> [_ Qy]; Ytac0; Ytac h.
       move => h2;case: nT; exact: (pr2_def(pr1_def h2)).
     move => h2;case: nT; exact: (pr2_def h2).
  move=> [] /candu2P [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; case: nT1; exact: (pr2_def sf).
  case: auxy; move=> [_ Qpy].
     rewrite Qpx Qpy; Ytac0; Ytac0 => sf; case: 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 (Lf f E F); split;fprops;aw.
  split; aw;apply: lf_bijective => //.
red; rewrite lf_source;move=> x y xE yE; aw.
move: (xE); rewrite Ev ; move=> /candu2P [px hx].
move: (yE); rewrite Ev ; move=> /candu2P [py hy].
split.
  move /orsum2_gleP => [_ _ h]; apply /orsum2_gleP; rewrite orsum2_sr //.
  split => //; first by move: (p1 _ xE); rewrite Fv.
     by move: (p1 _ yE); rewrite Fv.
  case: h.
      move=> [Qx Qy le]; constructor 1; rewrite /f (Y_true Qx) (Y_true Qy).
      rewrite ! pr1_pair ! pr2_pair; split => //.
      apply /orsum2_gleP;split => //; last by aw; constructor 1.
         apply candu2_pra; order_tac.
      apply candu2_pra; order_tac.
    move => [hxa hxb] /orsum2_gleP [_ _].
    case: hx; move => [pxa qxa]; first by case: hxa.
    case: hy; move => [pya qya]; first by case: hxb.
    case; last first.
        by move => [sa sb]; constructor 3; rewrite /f; do 4 Ytac0; aw.
      by move => [sa sb sc];constructor 2; rewrite /f; do 4 Ytac0; aw.
    move => [sa sb sc]; constructor 1; rewrite /f; do 4 Ytac0; aw.
    case /candu2P: pxa => _ [] [ta tb]; last by case: nT; rewrite - sa - tb.
    case /candu2P: pya => _ [] [ta' tb']; last by case: nT; rewrite - sb - tb'.
    split => //; apply/orsum2_gleP; split => //.
        by apply: candu2_prb.
      by apply: candu2_prb.
    aw; by constructor 2.
  move=> [Qxa Qyb].
  case: hy; move => [pya qya]; first by case: Qyb.
  case: hx; move => [pxa qxa]; last by case: nT; ue.
  move /candu2P: pya =>[_]; case; move => [sa sb].
     constructor 1; rewrite /f; Ytac0; Ytac0; Ytac0; aw; split => //.
     apply /orsum2_gleP; split => //.
     - by apply candu2_pra.
     - by apply candu2_prb.
     - by constructor 3; aw.
  by constructor 3; rewrite /f sb; Ytac0; Ytac0; aw; Ytac0;aw.
move /orsum2_gleP => [_ _ h]; apply /orsum2_gleP.
rewrite orsum2_sr // -/A -/B -/C - Ev;split => //.
case: hx; move => [Px Qx].
  have fx: f x = (J (J (P x) C0) C0) by rewrite /f Y_true.
  case: hy; move => [Py Qy].
    have fy: f y = (J (J (P y) C0) C0) by rewrite /f Y_true.
    constructor 1; split => //.
    move: h; rewrite fx fy ! pr1_pair ! pr2_pair; case.
    - move=> [_ _] /orsum2_gleP [_ _]; case; aw; first by move => [_ _ s].
      + by move=> [_ bad _].
      + by move=> [_ bad].
    - by move=> [_ bad _].
    - by move=> [_ bad].
  constructor 3; rewrite Qx Qy; split; exact.
case: hy; move => [Py Qy].
  case: (nT); case: h.
    move=> [Qfx Qfy] /orsum2_gleP [Pfx Pfy].
      have -> : Q (P (f y)) = C0 by rewrite /f; Ytac0; aw.
      case; [ | move => [_ pa _] | move => [_ pa]]; try by case: pa.
      move=> [h1 _]; move: h1 Qfx; rewrite /f Qx (Y_false) //;Ytac ww; aw.
    by move => [_ pa _]; move: pa; rewrite /f; Ytac0; aw.
  by move => [ _ ]; rewrite /f; Ytac0; aw.
rewrite Qx Qy; constructor 2; split => //.
apply /orsum2_gleP; split => //.
move: Px Py => /candu2P [pPx hpx] /candu2P [pPy hpy].
case: hpx; move => [pa pb].
  case: hpy; move => [pc pd]; last by constructor 3; rewrite pd;split => //.
  constructor 1; split => //; move: h; rewrite /f Qx Qy; do 4 Ytac0.
  case; [move => [_ _ ba] | move => [ba _] | move=> [_ ba]]; move: ba; aw => //.
  move /orsum2_gleP => [_ _];rewrite !pr1_pair !pr2_pair.
  by case; [ move => [sa _] | move => [_ _] | move => [sa _]].
constructor 2; rewrite pb; move: h; rewrite /f Qx Qy pb.
Ytac0; Ytac0; Ytac0; case; first by move => [sa _]; move: sa; aw.
  Ytac ww; first by move => [_ qa _]; move: qa; aw.
  by move => [_ _]; aw.
by move => [sa _]; move: sa; aw.
Qed.

Lemma oprod_assoc2 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=> oa ob oc.
have oab: order (order_prod2 a b) by fprops.
have obc: order (order_prod2 b c) by fprops.
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 ! orprod2_sr.
have Fv: F = product2 C (product2 B A).
  by rewrite /F ! orprod2_sr.
have CB_pr: forall z, inc z (product2 C B) <->
   [/\ fgraph z, domain z = C2, inc (Vg z C0) C & inc (Vg z C1) B].
   by move=> z; apply /setX2_P.
have BA_pr: forall z, inc z (product2 B A) <->
   [/\ fgraph z, domain z = C2, inc (Vg z C0) B & inc (Vg z C1) A].
   by move=> z; apply /setX2_P.
set f := fun z => variantLc (Vg (Vg z C0) C0)
     (variantLc (Vg (Vg z C0) C1) (Vg z C1)).
have p01: forall x, inc x E -> inc (f x) F.
  move=> x; rewrite Ev Fv; move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3].
  rewrite /f; bw; apply /setX2_P; split => //; fprops; bw.
  apply /setX2_P; split => //; fprops; bw.
have p02: forall x y, inc x E -> inc y E -> f x = f y -> x = y.
  move=> x y; rewrite Ev; move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3].
  rewrite /f; move /setX2_P => [p1' p2' /setX2_P [p4' p5' p6' p7'] p3'] sf.
  move: (f_equal (Vg ^~ C0) sf) (f_equal (Vg ^~C1) sf); bw => sf1 sf2.
  move: (f_equal (Vg ^~C0) sf2) (f_equal (Vg ^~C1) sf2); bw => sf3 sf4.
  apply: fgraph_exten =>//; try ue.
  rewrite p2; move=> z zdx;try_lvariant zdx.
  apply: fgraph_exten =>//; try ue.
  rewrite p5; move=> zz zdx; try_lvariant zdx.
have p03: forall y, inc y F -> exists2 x, inc x E & y = f x.
  move=> y; rewrite Fv; move /setX2_P => [p1 p2 p3 /setX2_P [p4 p5 p6 p7]].
  exists (variantLc (variantLc (Vg y C0) (Vg (Vg y C1) C0))
       (Vg (Vg y C1) C1)).
     rewrite Ev;apply /setX2_P; split;fprops; bw.
     apply /setX2_P; split;fprops; bw.
  rewrite /f; symmetry;apply: fgraph_exten => //; bw; fprops.
  move=> x xtp; try_lvariant xtp.
  apply: fgraph_exten => //; bw ; [fprops | by symmetry | ].
  move=> z xtp; try_lvariant xtp.
exists (Lf f E F); split => //; fprops;aw.
  split; aw;apply: lf_bijective => //.
red; aw; move=> x y xE yE; aw.
move: (xE); rewrite Ev;move /setX2_P => [p1 p2 /setX2_P [p4 p5 p6 p7] p3].
move: (yE);rewrite Ev;move /setX2_P => [p1' p2' /setX2_P [p4' p5' p6' p7'] p3'].
split.
  move: (p01 _ xE)(p01 _ yE) => xF yF.
  move: xF; rewrite Fv; case /setX2_P=>[q1 q2 q3 /setX2_P [q4 q5 q6 q7]].
  move: yF; rewrite Fv; case /setX2_P=>[r1 r2 r3 /setX2_P [r4 r5 r6 r7]].
  have x1: inc (Vg (f x) C1) (product2 B A) by rewrite BA_pr.
  have y1: inc (Vg (f y) C1) (product2 B A) by rewrite BA_pr.
  set hi1:= inc (Vg (f x) C1) (product2 B A).
  set hi2:= inc (Vg (f y) C1) (product2 B A).
  move => tmp; apply /(orprod2_gleP oab oc).
  rewrite orprod2_sr // -/A -/B -/C -Fv;split => //; try apply: p01 => //.
  move: tmp => /(orprod2_gleP oa obc) [_ _]; case.
     move => [pa pb];left; split; first by rewrite /f; bw;ue.
     apply /(orprod2_gleP oa ob);split => //;left.
     by rewrite /f; bw;split => //; rewrite pa.
  move => [] /(orprod2_gleP ob oc) [_ _ aux'] nse.
  case: aux'; last by move=> aux2; right; rewrite /f; bw.
  move=> [Vaa Vba]; left; split; first by rewrite /f; bw.
  apply /(orprod2_gleP oa ob);split => //; right.
  rewrite /f; bw; split => //; dneg aux3.
  apply: fgraph_exten =>//; try ue.
  rewrite p5; move=> z zd; try_lvariant zd.
move /(orprod2_gleP oab oc) => [_ _ tmp].
apply/(orprod2_gleP oa obc); rewrite orprod2_sr // -/A -/B -/C -Ev;split => //.
have x1: inc (Vg x C0) (product2 C B) by rewrite CB_pr.
have y1: inc (Vg y C0) (product2 C B) by rewrite CB_pr.
case: tmp; last first.
  rewrite /f; bw; move=> [h1 h2]; right; split.
  apply /(orprod2_gleP ob oc);split => //; by right.
  by dneg eql; rewrite eql.
rewrite /f; bw; move => [xaa] /(orprod2_gleP oa ob) [fxb fxa]; bw.
case.
    move=> [sVab le]; left; split =>//.
    apply: fgraph_exten => //; first by ue.
    rewrite p5; move=> z zd; try_lvariant zd.
move=> [lt2 neq]; right;split; last by dneg aux; rewrite aux.
by apply /(orprod2_gleP ob oc);split => //; left.
Qed.

Lemma osum_distributive a b c:
  order a -> order b -> order c ->
  (order_prod2 c (order_sum2 a b))
  \Is (order_sum2 (order_prod2 c a) (order_prod2 c b)).
Proof.
move=> oa ob oc.
move: (orsum2_or oa ob) => oab.
move: (orprod2_or oc oa) => oca.
move: (orprod2_or oc ob) => ocb.
move: (orprod2_or oc oab) => ocab.
move:(orsum2_or oca ocb) => ocacb.
set (f := fun z => J (variantLc (P (Vg z C0)) (Vg z C1)) (Q (Vg z C0))).
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 orprod2_sr // orsum2_sr //.
have Fp: F = canonical_du2 (product2 A C)(product2 B C).
  rewrite /F orsum2_sr // !orprod2_sr //.
have Ev: forall x, inc x E <-> [/\ fgraph x, domain x = C2,
    pairp (Vg x C0),
     ((inc (P (Vg x C0)) A /\ Q (Vg x C0) = C0) \/
      (inc (P (Vg x C0)) B /\ Q (Vg x C0) = C1))
     &inc (Vg x C1) C].
  move=> x; rewrite Ep; split.
     move /setX2_P => [pa pb pc pd]; move/candu2P: pc => [pe] [] [pf pg];
     split => //; [left | right ]; split => //.
  by move => [pa pb pc pd pe]; apply /setX2_P;split => //; apply/candu2P.
have Fv: forall x, inc x F <-> [/\ pairp x, fgraph (P x),
    domain (P x) = C2, inc (Vg (P x) C1) C &
    ((inc (Vg (P x) C0) A /\ Q x = C0) \/
    (inc (Vg (P x) C0) B /\ Q x = C1))].
   move=> x; rewrite Fp; split.
     move /candu2P => [pa []] [] /setX2_P [pb pc pd pe] pf; split;fprops.
   move => [pa pb pc pd];case; move =>[pe pf];
    apply /candu2P;split => //; [left | right];
    split => //;apply /setX2_P; split; fprops.
have p1: forall x, inc x E -> inc (f x) F.
  move=> x /Ev [pa pb pc pd pe]; rewrite /f; apply/Fv.
  rewrite !pr1_pair !pr2_pair; bw; split;fprops.
have p2: forall x y, inc x E -> inc y E -> f x = f y -> x = y.
  move=> x y /Ev [fgx dx px hx qx] /Ev [fgy dy py hy qy].
  rewrite /f => sf; move: (pr1_def sf)(pr2_def sf) => r1 r2.
  move: (f_equal (Vg ^~C0) r1)(f_equal (Vg ^~C1) 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 -> exists2 x, inc x E & y = f x.
  move=> y /Fv [py fPy dPy Vby Vay].
  exists (variantLc (J (Vg (P y) C0) (Q y)) (Vg (P y) C1)).
    apply /Ev; bw; rewrite !pr1_pair !pr2_pair; split;fprops.
  rewrite /f; bw;aw; apply: pair_exten =>//; [ fprops | aw | aw].
  apply: fgraph_exten; [ exact| fprops | bw | bw].
  rewrite dPy; move=> x xtp; try_lvariant xtp.
  exists (Lf f E F); split => //; aw; first by split; aw;apply: lf_bijective.
red; aw;move=> x y xE yE; rewrite lf_V // lf_V //.
have r1: Q (f x) = Q (Vg x C0) by rewrite /f pr2_pair.
have r2: Q (f y) = Q (Vg y C0) by rewrite /f pr2_pair.
have r3: Vg (P (f x)) C0 = P (Vg x C0) by rewrite /f; aw; bw.
have r4: Vg (P (f y)) C0 = P (Vg y C0) by rewrite /f; aw; bw.
have r5: Vg (P (f x)) C1 = Vg x C1 by rewrite /f; aw; bw.
have r6: Vg (P (f y)) C1 = Vg y C1 by rewrite /f; aw; bw.
have pa: pairp (Vg x C0) by move /Ev: xE => [_ _ px _].
have pb: pairp (Vg y C0) by move /Ev:yE => [_ _ px _].
move: (xE) => /Ev [fgx dx px hx qx].
move: (yE) => /Ev [fgy dy py hy qy].
move: TP_ne => nab.
split.
  move /(orprod2_gleP oc oab) => [_ _ h]; apply /(orsum2_gleP).
  split; first by move: (p1 _ xE); rewrite /F orsum2_sr.
     by move: (p1 _ yE); rewrite /F orsum2_sr.
  rewrite r1 r2; case: h.
    move=> [q1 q2]; rewrite -q1.
    case: (equal_or_not (Q (Vg x C0)) C0)=> q3.
      case: hx; move=> [q4 q5]; last by case: nab ; rewrite - q3 - q5.
      constructor 1; rewrite q3; split => //.
      apply /(orprod2_gleP oc oa).
      split; first by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops.
         by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops; ue.
      left; rewrite r3 r4 r5 r6 q1; split =>//.
    constructor 2; split => //.
    case: hx; move=> [q4 q5]; first by case: q3.
    apply /(orprod2_gleP oc ob).
    split; first by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops.
      by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops; ue.
    left; rewrite r3 r4 r5 r6 -q1; split =>//.
  move => [] /(orsum2_gleP) [_ _ h1] h2; case: h1.
      move=> [q1 q2 q3]; constructor 1.
      split; [exact | exact | ].
      case: hx; move=> [q4 q5]; last by case: nab; rewrite -q1 -q5.
      case: hy; move=> [q4' q5']; last by case: nab; rewrite -q2 -q5'.
      apply /(orprod2_gleP oc oa).
      split; first by apply/setX2_P; rewrite /f pr1_pair; bw; split;fprops.
         by apply/setX2_P; rewrite /f pr1_pair; bw; split;fprops.
      right; rewrite r3 r4;split => //;dneg aux.
      apply: pair_exten => //; ue.
    move => [q1 q2 q3]; constructor 2.
    case: hx; move=> [q4 q5]; first by case: q1.
    case: hy; move=> [q4' q5']; first by case: q2.
    split; [exact | exact | ].
    apply /(orprod2_gleP oc ob).
    split; first by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops.
      by apply/setX2_P; rewrite /f pr1_pair; bw;split;fprops.
    right; rewrite r3 r4; split => // sP; case: h2.
    by apply: pair_exten => //; rewrite q5 q5'.
  move=> res; constructor 3; exact.
move/(orsum2_gleP) => [_ _ h]; apply /(orprod2_gleP oc oab).
split; first by move: xE; rewrite /E orprod2_sr //.
  by move: yE; rewrite /E orprod2_sr //.
have pc: inc (Vg x C0) (canonical_du2 (substrate a) (substrate b)).
  by move: xE => /Ev [_ _ px' etc _]; apply/candu2P.
have pd: inc (Vg y C0) (canonical_du2 (substrate a) (substrate b)).
  by move: yE => /Ev [_ _ px' etc _]; apply/candu2P.
case: h.
    move=> [q1 q2] /(orprod2_gleP oc oa) [q3 q4].
    rewrite r3 r4 r5 r6; case; move =>[q5 q6]; [left | right ].
      by split =>//; apply: pair_exten =>//; rewrite -r1 -r2 q1 q2.
    split =>//; last by dneg neq; rewrite neq.
    by apply /orsum2_gleP;split => //; constructor 1;rewrite -r1 -r2 q1 q2.
  move=> [q1 q2] /(orprod2_gleP oc ob) [q3 q4].
  case: hx; rewrite -r1; move => [_ sb]; first by case: q1.
  case: hy; rewrite -r2; move => [_ sb']; first by case: q2.
  rewrite r3 r4 r5 r6; case; move =>[q5 q6]; [left | right ].
    by split =>//; apply: pair_exten =>//; rewrite -r1 -r2 sb sb'.
  split =>//; last by dneg neq; rewrite neq.
  apply /orsum2_gleP;split => //; constructor 2; rewrite - r1 -r2;split => //.
move=> [q5 q6]; right; split.
  apply /orsum2_gleP;split => //; constructor 3; rewrite - r1 -r2;split => //.
by dneg neq; rewrite r2 -neq -r1.
Qed.

Lemma osum_increasing1 r f g:
  orsum_ax r f -> orsum_ax r g ->
  (forall x, inc x (domain f) -> order_le (Vg f x) (Vg g x)) ->
  order_le (order_sum r f) (order_sum r g).
Proof.
move => oa oa1 ale.
have o1: order (order_sum r f) by fprops.
have o2: order (order_sum r g) by fprops.
split => //; apply: (proj33 (order_le_alt o1 o2 _)).
set si:= fun j => choose (fun x => order_morphism x (Vg f j) (Vg g j)).
have sip: forall j, inc j (domain f) ->
       order_morphism (si j) (Vg f j) (Vg g j).
  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 (Lf (fun z => Vf f0 z) (substrate (Vg f j)) (substrate (Vg g j))).
have dfdg: domain f = domain g by move: oa oa1 => [_ s1 _] [_ s2 _]; ue.
set E := (substrate (order_sum r g)).
set F := (disjointU_fam (fam_of_substrates f)).
have p1: partition_w_fam F (substrate (order_sum r f)).
  bw;rewrite /F /sum_of_substrates; rewrite /disjointU.
  apply: partition_disjointU; rewrite /fam_of_substrates; fprops.
have p3: (domain F = domain f).
   rewrite /F/disjointU_fam /fam_of_substrates; bw.
set di:= fun i => ((substrate (Vg f i)) *s1 i).
set sj:= fun i => Lf (fun z => J (Vf (si i) (P z)) i) (di i) E.
have p0: forall i, inc i (domain f) ->
   lf_axiom (fun z => J (Vf (si i) (P z)) i) (di i) E.
  move=> i idf z zV.
  move: (sip _ idf) => [_ _ [ff sf tf] _].
  have aux: inc (Vf (si i) (P z) ) (substrate (Vg g i)).
    Wtac;move: zV => /indexed_P [_ Ps _]; ue.
  rewrite /E;bw; apply: disjoint_union_pi1 => //; ue.
have FP: forall i, inc i (domain f) -> Vg F i = di i.
  move=> i idf; rewrite /F /disjointU_fam/fam_of_substrates ; bw.
have p2: forall i, inc i (domain F) ->
   function_prop (sj i) (Vg F i) E.
  rewrite p3;move=> i idf; rewrite /sj FP => //; aw.
  by split;aw;apply: lf_function; apply: p0.
move: (extension_partition1 p1 p2).
  set G := common_ext _ _ _; move=> [[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)), pairp x,
   inc (P x)(substrate (Vg f (Q x))) & Vf G x = J (Vf(si (Q x)) (P 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 apply /indexed_P;split => //.
  split => //.
  move: (alg _ Qxd); rewrite /agrees_on; move=> [q1 q2 q3].
  move: (xdi); rewrite -FP // => q4.
  move: (q3 _ q4); rewrite /sj; rewrite lf_V; aw;apply: p0 => //.
exists G; split => //.
move=> x y xs ys.
move: (aux _ xs) (aux _ ys) => [Qx xdi px Px Wx][Qy ydi py Py Wy].
have qa: (sum_of_substrates f = source G) by rewrite sG; bw.
have qb: (sum_of_substrates g = target G) by rewrite tG /E; bw.
split; move /orsum_gleP =>[q1 q2 q3]; apply /orsum_gleP.
  rewrite qb;split=> //; try Wtac; rewrite Wx Wy;red;aw; case: q3; first by left.
  move=> [Qxx le1]; right; split => //.
  rewrite -Qxx; move: (sip _ Qx) => [_ _ [_ sf tf] orf].
  rewrite - orf //; rewrite sf //; ue.
move: q3; rewrite /order_sum_r Wx Wy !pr2_pair !pr1_pair.
move => q3; rewrite qa;split => //; case: q3; first by left.
move=> [Qxx]; rewrite - {1} Qxx => le1; right; split => //.
move: (sip _ Qx) => [_ _ [_ sf tf] orf].
apply /orf; rewrite ? sf //; ue.
Qed.

Lemma osum_increasing2 r f g: worder r ->
  substrate r = domain f -> substrate r = domain g ->
  (forall x, inc x (domain f) -> (Vg f x) <=o (Vg g x)) ->
  (ord_sum r f) <=o (ord_sum r g).
Proof.
move=> wor sf sg alo.
apply /ordinal_le_P0; apply /order_le_compatible1.
    apply: orsum_wor => //; bw.
    hnf; bw;move=> i idf; bw; fprops; move: (alo _ idf) => [aa bb _]; fprops.
  apply: orsum_wor => //;bw.
  hnf; bw;rewrite - sg sf; move=> i idf; bw.
  move: (alo _ idf) => [aa bb _]; fprops.
apply osum_increasing1.
- split => //;bw; fprops; hnf; bw.
  move=> i idf; bw; move: (alo _ idf) =>[aa bb _]; fprops.
- rewrite - sg sf;split;fprops;hnf; bw.
  move=> i idf; bw; move: (alo _ idf) =>[aa bb _]; fprops.
- rewrite - sg sf; bw => x xdf; move: (alo _ xdf) =>[aa bb le].
  bw; apply/order_le_compatible1; fprops.
  by rewrite (ordinal_o_o aa) (ordinal_o_o bb) ordinal_le_P0.
Qed.

Lemma osum_increasing3 r f j:
  orsum_ax r f ->
  sub j (domain f) ->
  order_le (order_sum (induced_order r j) (restr f j)) (order_sum r f).
Proof.
move=> oa jd.
move: (oa) => [or sr alo].
set (g:= Lg (domain f) (fun z => Yo (inc z j) (Vg f z) emptyset)).
have dfdg: domain f = domain g by rewrite /g; bw.
have oa': orsum_ax r g.
  split => //; first by ue.
  hnf;bw;rewrite - dfdg /g;move=> i idg; bw; Ytac ij;first by apply: alo.
   apply: set0_or.
have sjd': sub j (domain g) by ue.
have cz: (forall i, inc i ((domain g) -s j) -> Vg g i = \0o).
  by move=> i /setC_P; rewrite -dfdg /g; move=> [idf nij]; bw; Ytac0.
move: (osum_unit1 oa' sjd' cz).
have ->: (restr f j = restr g j).
  apply: Lg_exten => s sj;bw; rewrite /g; bw; [ by Ytac0 | by apply:jd ].
move=> oi1.
have oi2: order_isomorphic (order_sum r f) (order_sum r f).
  by apply: orderIR; apply: orsum_or.
apply /(order_le_compatible oi1 oi2).
apply: osum_increasing1 => //.
rewrite -dfdg; move=> x xdg; rewrite /g; bw.
Ytac xj; first by apply: order_leR=>//; apply: alo.
move: set0_or => eo.
split; fprops;exists (identity emptyset); exists emptyset.
have auw: sub emptyset (substrate (Vg f x)) by fprops.
split => //; split;fprops; aw.
- apply: (proj1 (iorder_osr _ auw)); fprops.
  split; aw; first by apply: identity_fb.
  by rewrite (proj2 set0_wor).
- apply: (alo _ xdg).
- by move=> u v; rewrite identity_s => /in_set0.
Qed.

Lemma osum_increasing4 r f j:
   worder_on r (domain f) -> sub j (domain f) -> ordinal_fam f ->
  (ord_sum (induced_order r j) (restr f j)) <=o (ord_sum r f).
Proof.
move => [wor 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 bw.
rewrite /ord_sum; apply /ordinal_le_P0; apply /order_le_compatible1.
   apply: orsum_wor.
     by apply: induced_wor => //; ue.
     by bw; aw;rewrite dr.
     by hnf; rewrite dr; bw; move=> i ij; bw; fprops.
  apply: orsum_wor => //; bw; hnf; bw; move=> i idf; bw; fprops.
set g:= (Lg (domain f) (fun z : Set => ordinal_o (Vg f z))).
have ->: (Lg (domain (restr f j)) (fun z => ordinal_o (Vg (restr f j) z)))
  = restr g j.
  bw;apply: Lg_exten.
  by rewrite /g;red; bw;move => x xj; bw; apply: sjf.
apply: osum_increasing3 => //.
rewrite /g;red; bw;split => //; hnf;bw; move=> i idf; bw; fprops.
rewrite /g; bw.
Qed.

Lemma oprod_increasing1 r f g:
  orprod_ax r f -> orprod_ax r g ->
  (forall x, inc x (domain f) -> order_le (Vg f x) (Vg g x)) ->
  order_le (order_prod r f) (order_prod r g).
Proof.
move => oa oa1 ale.
have o1: order (order_prod r f) by fprops.
have o2: order (order_prod r g) by fprops.
split => //; apply: (proj33 (order_le_alt o1 o2 _)).
set si:= fun j => choose (fun x => order_morphism x (Vg f j) (Vg g j)).
have sip: forall j, inc j (domain f) ->
       order_morphism (si j) (Vg f j) (Vg g j).
  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 (Lf (fun z => Vf f0 z) (substrate (Vg f j)) (substrate (Vg g j))).
have dfdg: domain f = domain g by move: oa oa1 => [_ s1 _] [_ s2 _]; ue.
set E:= substrate (order_prod r f).
set F := substrate(order_prod r g).
have Ep: E = (prod_of_substrates f) by apply: orprod_sr => //.
have Fp: F = (prod_of_substrates g) by apply: orprod_sr => //.
set h:= fun z => Lg (domain f) (fun i => Vf (si i) (Vg z i)).
have ta: lf_axiom h E F.
  rewrite Ep Fp ; move => t /prod_of_substratesP [fgt dt als].
  apply /prod_of_substratesP.
  rewrite - dfdg /h; bw;split;fprops;move=> i idf; bw.
  move: (sip _ idf) => [_ _ [fsi ssi tsi] _].
  by Wtac; rewrite ssi;apply: als.
have hi: forall u v, inc u E -> inc v E -> h u = h v -> u = v.
  rewrite Ep; move=> u v / prod_of_substratesP [fgu du alu]
     /prod_of_substratesP [fgv dv alv] sh.
  apply: fgraph_exten =>//; first by ue.
  rewrite du; move=> x xdf; move: (f_equal (Vg ^~x) sh); rewrite /h;bw => sW.
  move: (order_morphism_fi (sip _ xdf)) => [_ insi].
  move: (sip _ xdf) => [_ _ [fsi ssi tsi] _].
  apply: insi =>//; rewrite ssi; [ apply: alu => // |apply: alv => //].
exists (Lf h E F); red; aw; split => //.
  split; aw;by apply: lf_function.
red; aw; move=> x y xE yE; rewrite /h; aw.
have srdf: substrate r = domain f by move: oa => [_ sr _].
move: (xE); rewrite Ep; move /prod_of_substratesP => [fgx dx alx].
move: (yE); rewrite Ep; move /prod_of_substratesP => [fgy dy aly].
split.
  move /(orprod_gleP oa) => [_ _ aux]; apply /(orprod_gleP oa1).
  rewrite -Fp;split; [by apply: ta | by apply: ta |].
  case: aux; first by move=>->; left.
  move=> [j [jsr jlt jle]]; right; ex_tac.
    rewrite srdf in jsr;move: jlt; bw.
    move: (order_morphism_fi (sip _ jsr)) => [_ insi].
    move: (sip _ jsr) => [_ _ [fsi ssi tsi] jsrp].
    have vsx: inc (Vg x j) (source (si j)) by rewrite ssi; apply: alx => //.
    have vsy: inc (Vg y j) (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 /(orprod_gleP oa1) => [h1 h2 aux]; apply /(orprod_gleP oa).
rewrite -Ep; split=> //; case: aux.
  move => sh; left; apply: hi =>//.
move=> [j [jsr jlt jle]]; right; ex_tac.
rewrite srdf in jsr;move: jlt; bw.
move: (sip _ jsr) => [_ _ [fsi 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: (order_morphism_fi (sip _ idf)) =>[_ insi].
move: (sip _ idf) => [_ _ [fsi ssi tsi] jsrp].
apply: insi; rewrite ssi;[ apply: alx => // | apply: aly => //].
Qed.

Lemma oprod_increasing2 r f g: worder r ->
  substrate r = domain f -> substrate r = domain g ->
  (forall x, inc x (domain f) -> (Vg f x) <=o (Vg g x)) ->
  finite_set (substrate r) ->
  (ord_prod r f) <=o (ord_prod r g).
Proof.
move=> wor sf sg alo fse.
apply/ordinal_le_P0; apply /order_le_compatible1.
    apply: orprod_wor => //; [ split;bw | hnf; bw ].
    move=> i idf; bw; move: (alo _ idf) => [aa bb _]; fprops.
  apply: orprod_wor => //; [split; bw | hnf;bw ].
  rewrite - sg sf; move=> i idf; bw.
  by move: (alo _ idf) => [aa bb _]; fprops.
apply: oprod_increasing1.
    split => //;bw; hnf; bw => i idf; bw;move: (alo _ idf) =>[aa bb _];fprops.
  split => //; bw; hnf; bw; rewrite - sg sf.
  move => i idf; bw; move: (alo _ idf) =>[aa bb _]; fprops.
rewrite - sg sf; bw => x xdf; move: (alo _ xdf) =>[aa bb le].
bw; apply /order_le_compatible1; fprops.
by rewrite (ordinal_o_o aa) (ordinal_o_o bb) ordinal_le_P0.
Qed.

Lemma oprod_increasing3 r f j:
  orprod_ax r f ->
  sub j (domain f) ->
  (forall x, inc x ((domain f) -s j) ->
     substrate (Vg f x) <> emptyset) ->
  order_le (order_prod (induced_order r j) (restr f j)) (order_prod r f).
Proof.
move=> oa jd anot.
move: (oa) => [or sr alo].
set (g:= Lg (domain f) (fun z => Yo (inc z j) (Vg f z) (ordinal_o \1o))).
have dfdg: domain f = domain g by rewrite /g; bw.
have oa': orprod_ax r g.
  hnf; rewrite /order_fam /allf - dfdg;split => //.
   move=> i idg; rewrite /g; bw; Ytac ij; first by apply: alo.
  by apply: (ordinal_o_or).
have sjd': sub j (domain g) by ue.
have cz: (forall i, inc i ((domain g) -s j) ->
  singletonp (substrate (Vg g i))).
  move=> i /setC_P;rewrite -dfdg /g; move=> [idf nij]; bw; Ytac0.
  by rewrite (ordinal_o_sr); exists emptyset.
move: (oprod_unit1 oa' sjd' cz).
have ->: (restr f j = restr g j).
  apply: Lg_exten; bw; 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: orprod_or.
apply /(order_le_compatible oi1 oi2).
apply: oprod_increasing1 => //.
rewrite -dfdg; move=> x xdg; rewrite /g; bw.
Ytac nij; first by apply: order_leR=>//; apply: alo.
have p2: order (Vg f x) by move: oa => [q1 q2 q4]; apply: q4.
have [y yd]: nonempty (substrate (Vg f x)).
  case: (emptyset_dichot (substrate (Vg f x))) => // p1.
  have xcz: inc x ((domain f) -s j) by apply /setC_P.
  move: (anot _ xcz) => p4; contradiction.
have s1: sub (singleton y) (substrate (Vg f x)) by apply: set1_sub.
set h:= Lf (fun z => y) (singleton emptyset) (singleton y).
have ta: lf_axiom (fun _ : Set => y) (singleton emptyset) (singleton y).
   move=> t _ /=; fprops.
split => //; [fprops | exists h; exists (singleton y); split => //].
rewrite /h;split;fprops;bw; aw.
    apply (proj1 (iorder_osr p2 s1)).
  split; rewrite ? ordinal_o_sr;aw; apply: lf_bijective => //.
    by move=> u v /set1_P -> /set1_P ->.
  move=> u /set1_P ->; exists emptyset; [fprops | done].
move => u v;rewrite lf_source => aa bb; aw.
move: aa bb => /set1_P -> /set1_P ->.
split; move => _.
  by apply /iorder_gleP; fprops; order_tac.
rewrite / \1o/ \1c;apply /ordo_leP;split;fprops.
Qed.

Lemma oprod_increasing4 r f j:
  worder_on r (domain f) -> sub j (domain f) -> ordinal_fam f ->
  finite_set (substrate r) ->
  (forall x, inc x ((domain f) -s j) -> Vg f x <> \0o) ->
  (ord_prod (induced_order r j) (restr f j)) <=o (ord_prod r f).
Proof.
move => [wor sr] sjf alo fsr alnz.
have sjr: sub j (substrate r) by ue.
have or: order r by move: wor => [or _].
apply /ordinal_le_P0; apply /order_le_compatible1.
    apply: orprod_wor.
          split; bw;aw; apply: induced_wor => //; ue.
      hnf; bw; move=> i ij; bw; fprops.
    rewrite iorder_sr //; apply: (sub_finite_set sjr fsr).
  apply: orprod_wor => //; [ split;bw | hnf;bw ].
  move=> i idf; bw; fprops.
set g:= (Lg (domain f) (fun z : Set => ordinal_o (Vg f z))).
have ->: (Lg (domain (restr f j)) (fun z => ordinal_o (Vg (restr f j) z)))
    = restr g j.
    bw;apply: Lg_exten; rewrite /g; bw.
    by move => x xj /=; bw;apply: sjf.
apply: oprod_increasing3 => //.
    rewrite /g;split=> //;hnf; bw; move=> i idf; bw; fprops.
  rewrite /g; bw.
move => x; rewrite {1} /g; bw => xd; move: (alnz _ xd).
move: xd => /setC_P [xdf _]; move: (alo _ xdf) => ov.
by rewrite /g; bw; rewrite ordinal_o_sr.
Qed.

Parameter order_type: Set -> Set.
Axiom order_type_exists:
  forall x, order x -> order_isomorphic x (order_type x).
Axiom order_type_unique:
  forall x y, order_isomorphic x y -> (order_type x = order_type y).
Definition is_order_type x := exists2 y, order y & x = order_type y.

Definition order_type_le x y:=
   [/\ is_order_type x, is_order_type y &
   exists f z,
    sub z (substrate y) /\ order_isomorphism f x (induced_order y z)].

Notation "x <=t y" := (order_type_le x y) (at level 60).
Notation "x <=O y" := (order_le x y) (at level 60).

Lemma OT_ordinal_compat x: worder x ->
  order_type x = order_type (ordinal_o (ordinal x)).
Proof.
by move=> wor; apply: order_type_unique;move:(ordinal_o_is wor).
Qed.

Lemma OT_prop0 x: order x -> (order_type x) \Is x.
Proof. by move=> ox; apply: orderIS; apply: order_type_exists. Qed.

Lemma OT_prop1 x: order x -> is_order_type (order_type x).
Proof. by move=> ox; exists x. Qed.

Lemma OT_prop2 x: is_order_type x -> order x.
Proof.
move=> [y pa pb].
by move: (order_type_exists pa); rewrite -pb; move=> [f [oy ox _]].
Qed.

Lemma OT_prop3 x: order x -> order (order_type x).
Proof. by move => ox; apply: OT_prop2; apply: OT_prop1. Qed.

Lemma OT_prop4 x: order x ->
  order_type (order_type x) = order_type x.
Proof.
move => ox.
by apply: order_type_unique; apply: orderIS; apply: order_type_exists.
Qed.

Lemma order_le_alt4 r r': r <=O r' ->
   (exists f, order_morphism f r r').
Proof.
move=> [o1 o2 [f [z [sr [oa ob [[ [ff injf] sjf] sf tf] etc]]]]].
move: tf; aw => tf.
have ta: lf_axiom (Vf f) (substrate r) (substrate r').
   rewrite - sf; move=> t tsf; apply: sr; Wtac.
exists (Lf (Vf f) (substrate r) (substrate r')).
split => //;first split;aw.
  by apply: lf_function.
red; aw;move=> x y xsr ysr; aw; rewrite - sf in xsr ysr.
split => h; first by move/(etc _ _ xsr ysr): h => t; exact (iorder_gle1 t).
apply /(etc _ _ xsr ysr); apply /iorder_gleP => //; Wtac.
Qed.

Lemma order_le_alt3P r r':
  r <=O r' <-> (exists f, order_morphism f r r').
Proof.
split.
  apply: order_le_alt4.
 move => h; move: (h) => [_ [or or' _ _]].
by apply: order_le_alt.
Qed.

Lemma order_le_transitive x y z:
  x <=O y -> y <=O z -> x <=O z.
Proof.
move=> [ox oy [f [y1 [pa pb]]]] [_ oz [g [z1 [pc pd]]]].
split => //.
move: pb => [orx oix [[[ff injf] sjf] sf tf] etcf].
move: pd => [ory oiy [[[fg injg] sjg] sg tg] etcg].
move: tf tg; aw => tf tg.
set z2:= image_by_fun g y1.
have y1sg: sub y1 (source g) by ue.
have sz2z1: sub z2 z1 by rewrite - tg /z2; apply: fun_image_Starget1.
have sz2: sub z2 (substrate z) by apply: (sub_trans sz2z1).
set h:= Lf (fun t => (Vf g (Vf f t))) (substrate x) z2.
have ta: lf_axiom (fun t => Vf g(Vf f t)) (substrate x) z2.
  rewrite - sf;move=> t rx; apply /(Vf_image_P fg y1sg).
  exists (Vf f t) => //; Wtac.
move: (iorder_osr oz sz2) => [pa1 pb1].
exists h; exists z2; split => //; rewrite /h; split;fprops;aw.
  split; aw;apply: lf_bijective => //.
    rewrite - sf => u v ux vx sw; apply: injf => //.
    apply: injg =>//; rewrite sg; apply: pa; rewrite - tf;Wtac.
  move=> u /(Vf_image_P fg y1sg) [a ay1] ->.
  move: ay1; rewrite - tf => af; move: ((proj2 sjf) _ af).
  move=> [b bsf <-]; exists b => //; ue.
red; aw;move => a b asf bsf.
move: (ta _ asf) (ta _ bsf) => ta1 ta2; aw.
rewrite - sf in asf bsf.
have wa: inc (Vf f a) y1 by rewrite - tf; Wtac.
have wb: inc (Vf f b) y1 by rewrite - tf; Wtac.
have wa1: inc (Vf f a) (source g) by ue.
have wb1: inc (Vf f b) (source g) by ue.
set H1 := (etcf _ _ asf bsf); set Hb := (etcg _ _ wa1 wb1).
split.
 move /H1 => p1; apply /iorder_gleP => //.
 move: (iorder_gle1 p1); move /Hb => p2; exact :(iorder_gle1 p2).
move => p2; apply /H1;apply /iorder_gleP => //; apply /Hb.
move: (iorder_gle1 p2) => p1.
by apply /iorder_gleP => //; apply: sz2z1.
Qed.

Lemma OTorder_le_altP r r':
  r <=t r' <-> [/\ is_order_type r, is_order_type r' &
    exists f, order_morphism f r r'].
Proof.
split;move=> [o1 o2 etc]; split => //.
  apply /order_le_alt3P.
  by split => //; by apply: OT_prop2.
by move: (order_le_alt (OT_prop2 o1)(OT_prop2 o2) etc) => [_ _].
Qed.

Lemma OTorder_le_compat1 r: order r ->
  r <=O (order_type r).
Proof.
move=> or; apply /order_le_alt3P.
move: (order_type_exists or) => [f oi]; exists f => //.
by apply: order_isomorphism_w.
Qed.

Lemma OTorder_le_compat2 r: order r ->
  (order_type r) <=O r.
Proof.
move=> or; apply /order_le_alt3P.
move: (OT_prop0 or) => [f oi]; exists f => //.
by apply: order_isomorphism_w.
Qed.

Lemma OTorder_le_compatP r r': order r -> order r' ->
  (r <=O r' <-> (order_type r) <=O (order_type r')).
Proof.
move=> or or'.
split => h.
  apply: (@order_le_transitive _ r).
   apply: OTorder_le_compat2 => //.
  apply: (@order_le_transitive _ r') => //.
  apply: OTorder_le_compat1 => //.
apply: (@order_le_transitive _ (order_type r)).
   apply: OTorder_le_compat1 => //.
  apply: (@order_le_transitive _ (order_type r')) => //.
apply: OTorder_le_compat2 => //.
Qed.

Lemma OT_order_le_reflexive x: is_order_type x -> x <=t x.
Proof.
move=> ox; split => //; exists (identity (substrate x)); exists (substrate x).
split; first by fprops.
move: (OT_prop2 ox) => orx.
rewrite (iorder_substrate orx); exact: (identity_is orx).
Qed.

Lemma OTorder_le_alt2P r r':
  r <=t r' <-> [/\ is_order_type r, is_order_type r' & r <=O r'].
Proof.
split; first by move /OTorder_le_altP => [pa pb /order_le_alt3P pc].
by move => [pa pb /order_le_alt3P pc]; apply /OTorder_le_altP.
Qed.

Lemma OT_order_le_transitive x y z:
  x <=t y -> y <=t z -> x <=t z.
Proof.
move /OTorder_le_alt2P => [pa pb pc] /OTorder_le_alt2P [pd pe pf].
apply /OTorder_le_alt2P.
split => //; apply: (order_le_transitive pc pf).
Qed.

Definition OT_sum r g :=
   order_type (order_sum r (Lg (domain g) (fun z => (order_type (Vg g z))))).
Definition OT_prod r g :=
   order_type (order_prod r (Lg (domain g) (fun z => (order_type (Vg g z))))).
Definition OT_sum2 a b :=
  order_type (order_sum2 (order_type a) (order_type b)).
Definition OT_prod2 a b :=
  order_type (order_prod2 (order_type a) (order_type b)).

Notation "x +t y" := (OT_sum2 x y) (at level 50).
Notation "x *t y" := (OT_prod2 x y) (at level 40).

Lemma OT_sum2_pr a b:
  a +t b = OT_sum canonical_doubleton_order (variantLc a b).
Proof.
rewrite /OT_sum2 /OT_sum /order_sum2.
by rewrite variantLc_comp.
Qed.

Lemma OT_prod2_pr a b:
  a *t b = OT_prod canonical_doubleton_order (variantLc b a).
Proof.
rewrite /OT_prod2 /OT_prod /order_prod2.
by rewrite variantLc_comp.
Qed.

Lemma OT_sum_ordertype r g:
  order r -> substrate r = domain g -> order_fam g ->
   is_order_type (OT_sum r g).
Proof.
move=> or sr alo; apply: OT_prop1.
apply: orsum_or; bw; split => //; bw.
by hnf; bw; move=> i idg; bw; apply: OT_prop3; apply: alo.
Qed.

Lemma OT_prod_ordertype r g:
  worder r -> substrate r = domain g -> order_fam g
  -> is_order_type (OT_prod r g).
Proof.
move=> or sr alo; apply: OT_prop1.
apply: orprod_or; split => //; hnf;bw.
by move=> i idg; bw;apply: OT_prop3; apply: alo.
Qed.

Lemma OT_sum2_ordertype a b: is_order_type a -> is_order_type b ->
  is_order_type (a +t b).
Proof.
move=> wo1 wo2;rewrite /OT_sum2; apply: OT_prop1.
by apply: orsum2_or;apply: OT_prop3; apply: OT_prop2.
Qed.

Lemma OT_prod2_ordertype a b: is_order_type a -> is_order_type b ->
  is_order_type (a *t b).
Proof.
move=> wo1 wo2;rewrite /OT_prod2; apply: OT_prop1.
by apply: orprod2_or; apply: OT_prop3; apply: OT_prop2.
Qed.

Lemma OT_sum_invariant3 r g:
  order r -> substrate r = domain g -> order_fam g ->
  order_type (order_sum r g) =
    OT_sum r (Lg (substrate r) (fun i => order_type (Vg g i))).
Proof.
move => or sr alo.
rewrite /OT_sum;apply: order_type_unique.
apply: orsum_invariant2; fprops;bw.
rewrite sr;move=> i isr ; bw; move: (alo _ isr) => oi.
by rewrite OT_prop4 //; apply: order_type_exists.
Qed.

Lemma OT_prod_invariant3 r g:
  worder r -> substrate r = domain g -> order_fam g ->
  order_type (order_prod r g) =
    OT_prod r (Lg (substrate r) (fun i => order_type (Vg g i))).
Proof.
move => or sr alo.
rewrite /OT_prod;apply: order_type_unique.
apply: orprod_invariant2;fprops;bw.
rewrite sr;move=> i isr ; bw; move: (alo _ isr) => oi.
by rewrite OT_prop4 //; apply: order_type_exists.
Qed.

Lemma OT_sum_invariant5 a b c: order a -> order b -> order c ->
  (order_sum2 a b) \Is c ->
  (order_type a) +t (order_type b) = order_type c.
Proof.
move=> oa ob oc => h.
rewrite /ord_sum2; apply: order_type_unique.
rewrite OT_prop4 // OT_prop4 //.
by apply: (@orderIT (order_sum2 a b)) => //;
   apply: orsum_invariant4;apply: OT_prop0.
Qed.

Lemma OT_prod_invariant5 a b c: order a -> order b -> order c ->
  (order_prod2 a b) \Is c ->
  (order_type a) *t (order_type b) = order_type c.
Proof.
move=> oa ob oc => h.
rewrite /ord_sum2; apply: order_type_unique.
rewrite OT_prop4 // OT_prop4 //.
by apply: (@orderIT (order_prod2 a b)) => //;
   apply: orprod_invariant4;apply: OT_prop0.
Qed.

Definition order_type_fam g := (allf g is_order_type).

Lemma OT_sum_assoc1 r g r' g':
  order r -> substrate r = domain g -> order_type_fam g ->
  order r' -> substrate r' = domain g' -> order_fam g' ->
  r = order_sum r' g' ->
  let order_sum_assoc_aux :=
    fun l =>
    OT_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in
  OT_sum r g = OT_sum r' (Lg (domain g') (order_sum_assoc_aux)).
Proof.
move=> wor sr alB wor' sr' alw oal osa.
rewrite /OT_sum.
have oa': orsum_ax r' g' by [].
apply: order_type_unique.
set g'' := (Lg (domain g) (fun z => order_type (Vg g z))).
have oa: orsum_ax r g''.
  rewrite /g'';red; bw; split => //;hnf;bw; move=> i idg; bw.
  by move: (OT_prop3 (OT_prop2 (alB _ idg))).
move: (orsum_assoc_iso oa oa' oal) => /=.
set aux' := fun l =>
    order_sum (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g'' (J i l))).
set f:= Lf _ _ _.
move => oi1; move: (oi1) => [o1 o2 _ _].
apply: (@orderIT (order_sum r' (Lg (domain g') aux'))); first by exists f.
apply: orsum_invariant2 =>//; bw; fprops.
rewrite sr';move=> i isr; bw; rewrite /osa /OT_sum; bw.
set s := order_sum _ _.
have os: order s.
  rewrite /s; apply: orsum_or; split => //; bw; first by apply: alw.
  hnf; bw;move=> j js; bw.
  have jdg: inc (J j i) (domain g).
    by rewrite - sr oal (orsum_sr oa'); apply: disjoint_union_pi1.
  apply: (OT_prop3 (OT_prop2 (alB _ jdg))).
have -> : (aux' i = s).
  rewrite /aux' /s; apply: f_equal.
  apply: Lg_exten => //;move=> j js.
  have pd: inc (J j i) (domain g).
    by rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1.
  rewrite /g''; bw.
by rewrite OT_prop4 //; apply: order_type_exists.
Qed.

Lemma OT_prod_assoc1 r g r' g':
  worder r -> substrate r = domain g -> order_type_fam g ->
  worder r' -> substrate r' = domain g' -> worder_fam g' ->
  r = order_sum r' g' ->
  (forall i, inc i (domain g') -> finite_set (substrate (Vg g' i))) ->
  let order_prod_assoc_aux :=
    fun l =>
    OT_prod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g (J i l))) in
  OT_prod r g = OT_prod r' (Lg (domain g') order_prod_assoc_aux).
Proof.
move=> wor sr alB wor' sr' alw oal alfs osa.
rewrite /OT_prod.
have oa': orsum_ax r' g'.
  by split;fprops; move => t ta; move: (proj1 (alw _ ta)).
apply: order_type_unique.
set g'' := (Lg (domain g) (fun z => order_type (Vg g z))).
have oa: orprod_ax r g''.
  rewrite /g'';red; bw;split => //; hnf;bw; move=> i idg; bw.
  apply: (OT_prop3 (OT_prop2 (alB _ idg))).
move: (orprod_assoc_iso oa oa' oal wor' alw) => /=.
set aux' := fun l =>
    order_prod (Vg g' l) (Lg (substrate (Vg g' l)) (fun i => Vg g'' (J i l))).
set f:= Lf _ _ _.
move => oi1; move: (oi1) => [o1 o2 _ _].
apply: (@orderIT (order_prod r' (Lg (domain g') aux')));
    first by exists f.
apply: orprod_invariant2 =>//; bw; fprops.
rewrite sr';move=> i isr; bw; rewrite /osa /OT_prod; bw.
set s:= order_prod _ _.
have -> : (aux' i = s).
  rewrite /aux' /s; apply: f_equal.
  apply: Lg_exten => //;move=> j js.
  have pd: inc (J j i) (domain g).
    by rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1.
  rewrite /g''; bw.
have os: order s.
  rewrite /s; apply: orprod_or; split;bw; first fprops.
  hnf; bw;move=> j js; bw.
  have jdg: inc (J j i) (domain g).
    rewrite - sr oal (orsum_sr oa'); by apply: disjoint_union_pi1.
  apply: (OT_prop3 (OT_prop2 (alB _ jdg))).
by rewrite OT_prop4 //; apply: order_type_exists.
Qed.

Lemma OT_sum_assoc3 a b c:
  is_order_type a -> is_order_type b -> is_order_type c ->
  a +t (b +t c) = (a +t b) +t c.
Proof.
move => oa ob oc.
have xoa: order (order_type a) by apply: OT_prop3; apply: OT_prop2.
have xob: order (order_type b) by apply: OT_prop3; apply: OT_prop2.
have xoc: order (order_type c) by apply: OT_prop3; apply: OT_prop2.
rewrite/OT_sum2; apply: order_type_unique.
have pa: order (order_sum2 (order_type b) (order_type c)).
  by apply: orsum2_or.
have pb: order (order_sum2 (order_type a) (order_type b)).
  by apply: orsum2_or.
rewrite OT_prop4 // OT_prop4 //.
apply: (@orderIT
    (order_sum2 (order_type a) (order_sum2 (order_type b) (order_type c)))).
  apply: orsum_invariant4; [by apply: orderIR | by apply: OT_prop0 ].
apply: (@orderIT
  (order_sum2 (order_sum2 (order_type a) (order_type b))(order_type c))).
apply: osum_assoc2; fprops.
apply: orsum_invariant4; [ by apply: order_type_exists | by apply: orderIR].
Qed.

Lemma OT_prod_assoc3 a b c:
  is_order_type a -> is_order_type b -> is_order_type c ->
  a *t (b *t c) = (a *t b) *t c.
Proof.
move => oa ob oc.
have xoa: order (order_type a) by apply: OT_prop3; apply: OT_prop2.
have xob: order (order_type b) by apply: OT_prop3; apply: OT_prop2.
have xoc: order (order_type c) by apply: OT_prop3; apply: OT_prop2.
rewrite/OT_prod2; apply: order_type_unique.
have pa: order (order_prod2 (order_type b) (order_type c)).
  by apply: orprod2_or.
have pb: order (order_prod2 (order_type a) (order_type b)).
  by apply: orprod2_or.
rewrite OT_prop4 // OT_prop4 //.
apply: (@orderIT
 (order_prod2 (order_type a) (order_prod2 (order_type b) (order_type c)))).
  apply: orprod_invariant4; [ by apply: orderIR |by apply: OT_prop0 ].
apply: (@orderIT
  (order_prod2 (order_prod2 (order_type a) (order_type b))(order_type c))).
apply: oprod_assoc2; fprops.
apply: orprod_invariant4; [ by apply: order_type_exists | by apply: orderIR].
Qed.

Lemma OT_sum_distributive3 a b c:
  is_order_type a -> is_order_type b -> is_order_type c ->
  c *t (a +t b) = (c *t a) +t (c *t b).
Proof.
move => oa ob oc.
rewrite /OT_sum2 /OT_prod2; apply: order_type_unique.
have xoa: order (order_type a) by apply: OT_prop3; apply: OT_prop2.
have xob: order (order_type b) by apply: OT_prop3; apply: OT_prop2.
have xoc: order (order_type c) by apply: OT_prop3; apply: OT_prop2.
have pa: order (order_prod2 (order_type c) (order_type a)).
  by apply: orprod2_or.
have pb: order (order_prod2 (order_type c) (order_type b)).
  by apply: orprod2_or.
have pc: order (order_sum2 (order_type a) (order_type b)).
  by apply: orsum2_or.
rewrite OT_prop4 // OT_prop4 // OT_prop4 //.
apply: (@orderIT
  (order_prod2 (order_type c) (order_sum2 (order_type a) (order_type b)))).
  apply: orprod_invariant4; [ by apply: orderIR | by apply: OT_prop0].
apply: (@orderIT
     (order_sum2
        (order_prod2 (order_type c) (order_type a))
        (order_prod2 (order_type c) (order_type b)))).
  apply: osum_distributive => //.
by apply: orsum_invariant4;apply: order_type_exists.
Qed.

Lemma OT_sum_increasing2 r f g: order r ->
  substrate r = domain f -> substrate r = domain g ->
  (forall x, inc x (domain f) -> (Vg f x) <=t (Vg g x)) ->
  (OT_sum r f) <=t (OT_sum r g).
Proof.
move=> wor sf sg alo.
have Xa: orsum_ax r (Lg (domain f) (fun z : Set => order_type (Vg f z))).
  split => //;hnf; bw; move=> i isf; bw.
  move: (alo _ isf) => [pa pb _].
  by apply: OT_prop3; apply: OT_prop2.
have Xb: orsum_ax r (Lg (domain g) (fun z : Set => order_type (Vg g z))).
  split => //; hnf;bw; rewrite - sg sf.
  move=> i isf; bw;move: (alo _ isf) => [pa pb _].
  by apply: OT_prop3; apply: OT_prop2.
have pa:order (order_sum r (Lg (domain f) (fun z => order_type (Vg f z)))).
  by apply: orsum_or.
have pb:order (order_sum r (Lg (domain g) (fun z => order_type (Vg g z)))).
  by apply: orsum_or.
have pc: is_order_type (OT_sum r f) by apply: OT_prop1.
have pd: is_order_type (OT_sum r g) by apply: OT_prop1.
apply / OTorder_le_altP;split =>// ; apply: order_le_alt4.
apply /(OTorder_le_compatP pa pb); apply:osum_increasing1 => //.
bw; move=> x xdf; bw; last by rewrite - sg sf.
move: (alo _ xdf); move /OTorder_le_alt2P=> [ot1 ot2].
by move /(OTorder_le_compatP (OT_prop2 ot1) (OT_prop2 ot2)).
Qed.

Lemma OT_prod_increasing2 r f g: worder r ->
  substrate r = domain f -> substrate r = domain g ->
  (forall x, inc x (domain f) -> (Vg f x) <=t (Vg g x)) ->
  (OT_prod r f) <=t (OT_prod r g).
Proof.
move=> wor sf sg alo.
have Xa: orprod_ax r (Lg (domain f) (fun z : Set => order_type (Vg f z))).
  split => //;hnf ;bw; move=> i isf; bw.
  move: (alo _ isf) => [pa pb _].
  by apply: OT_prop3; apply: OT_prop2.
have Xb: orprod_ax r (Lg (domain g) (fun z : Set => order_type (Vg g z))).
  split => //; hnf;bw; rewrite - sg sf.
  move=> i isf; bw;move: (alo _ isf) => [pa pb _].
  by apply: OT_prop3; apply: OT_prop2.
have pa:order (order_prod r (Lg (domain f) (fun z => order_type (Vg f z)))).
  by apply: orprod_or.
have pb:order (order_prod r (Lg (domain g) (fun z => order_type (Vg g z)))).
  by apply: orprod_or.
have pc: is_order_type (OT_prod r f) by apply: OT_prop1.
have pd: is_order_type (OT_prod r g) by apply: OT_prop1.
apply /OTorder_le_altP;split => //; apply: order_le_alt4.
apply /(OTorder_le_compatP pa pb).
apply: oprod_increasing1 => //.
bw; move=> x xdf; bw; last by rewrite - sg sf.
move: (alo _ xdf); move /OTorder_le_alt2P=> [ot1 ot2].
by move /(OTorder_le_compatP (OT_prop2 ot1)(OT_prop2 ot2)).
Qed.

Lemma OT_sum_increasing4 r f j: order r ->
  substrate r = domain f ->
  sub j (domain f) -> order_type_fam f ->
  (OT_sum (induced_order r j) (restr f j)) <=t (OT_sum r f).
Proof.
move => or sr sjf alo.
have sjr: sub j (substrate r) by ue.
have dr: (domain (restr f j)) = j by rewrite restr_d //.
have Xa: orsum_ax r (Lg (domain f) (fun z => order_type (Vg f z))).
  split => //; hnf; bw;move=> i isf; bw;move: (alo _ isf) => iot.
  by apply: OT_prop3; apply: OT_prop2.
have pa:order (order_sum r (Lg (domain f) (fun z => order_type (Vg f z)))).
  by apply: orsum_or.
have pc: is_order_type (OT_sum r f) by apply: OT_prop1.
have dj: j = domain (restr f j) by rewrite restr_d.
move: (iorder_osr or sjr) => [pa' pb'].
have p2: orsum_ax (induced_order r j)
     (Lg (domain (restr f j)) (fun z : Set => order_type (Vg (restr f j) z))).
  split;fprops;bw;aw; hnf; bw; move=> i idf; bw.
  move: (sjr _ idf); rewrite sr => i1; move: (alo _ i1) => iot.
  by apply: OT_prop3; apply: OT_prop2.
have pb: order (order_sum (induced_order r j)
        (Lg (domain (restr f j)) (fun z => order_type (Vg (restr f j) z)))).
  by apply: orsum_or.
have pd: is_order_type (OT_sum (induced_order r j) (restr f j)).
  by apply: OT_prop1.
apply /OTorder_le_altP; split => //; apply: order_le_alt4.
apply /(OTorder_le_compatP pb pa).
set g:= (Lg (domain f) (fun z : Set => order_type (Vg f z))).
have fgg: fgraph g by rewrite /g; fprops.
have sjdg: sub j (domain g) by rewrite /g; bw; ue.
have ->: (Lg (domain (restr f j)) (fun z => order_type (Vg (restr f j) z)))
   = restr g j.
  by apply: fgraph_exten;fprops; bw;rewrite /g; move => k kj /= ;bw; apply: sjf.
apply: osum_increasing3 => //.
Qed.

Lemma OT_prod_increasing4 r f j: worder r ->
  substrate r = domain f ->
  sub j (domain f) -> order_type_fam f ->
  (forall x, inc x ((domain f) -s j) ->
     substrate (Vg f x) <> emptyset) ->
  (OT_prod (induced_order r j) (restr f j)) <=t (OT_prod r f).
Proof.
move => or sr sjf alo alne .
have sjr: sub j (substrate r) by ue.
have dr: (domain (restr f j)) = j by rewrite restr_d //.
have Xa: orprod_ax r (Lg (domain f) (fun z => order_type (Vg f z))).
  split => //; hnf;bw; move=> i isf; bw;move: (alo _ isf) => iot.
  by apply: OT_prop3; apply: OT_prop2.
have pa:order (order_prod r (Lg (domain f) (fun z => order_type (Vg f z)))).
  by apply: orprod_or.
have pc: is_order_type (OT_prod r f) by apply: OT_prop1.
have dj: j = domain (restr f j) by rewrite restr_d.
have odr: order r by move: or => [ok _].
have p2: orprod_ax (induced_order r j)
     (Lg (domain (restr f j)) (fun z : Set => order_type (Vg (restr f j) z))).
  have woi: worder (induced_order r j) by apply:induced_wor.
  split => //; bw; aw; hnf; bw=> i idf; bw.
  move: (sjr _ idf); rewrite sr => i1; move: (alo _ i1) => iot.
  by apply: OT_prop3; apply: OT_prop2.
have pb: order (order_prod (induced_order r j)
        (Lg (domain (restr f j)) (fun z => order_type (Vg (restr f j) z)))).
  by apply: orprod_or.
have pd: is_order_type (OT_prod (induced_order r j) (restr f j)).
  by apply: OT_prop1.
apply/OTorder_le_altP; split => //; apply: order_le_alt4.
apply /(OTorder_le_compatP pb pa).
set g:= (Lg (domain f) (fun z : Set => order_type (Vg f z))).
have fgg: fgraph g by rewrite /g; fprops.
have sjdg: sub j (