Library ssete2

Theory of Sets : Exercises

Copyright INRIA (2009-2012) Apics/Marelle Team (Jose Grimm).

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset13 ssete1.

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

We start with some results that are not in the main files

Module Exercise2_aux.

There is a distribution law between powerset and intersection2

Lemma union_monotone3 A B:
  sub A B -> sub (union A) (union B).
Proof.
move=> sAB t /setU_P [y ty yA]; apply/setU_P;exists y => //; fprops.
Qed.

Lemma intersection_greatest A B x:
   sub x A -> sub x B -> sub x (A \cap B).
Proof. move=> xA xB t tx; apply /setI2_P; split;fprops. Qed.

Lemma powerset_inter A B:
   powerset (A \cap B) = (powerset A) \cap (powerset B).
Proof.
apply: extensionality.
  apply: intersection_greatest.
     apply: powerset_mono; apply: subsetI2l.
  apply: powerset_mono; apply:subsetI2r.
move=> x /setI2_P[] /setP_P xpA /setP_P xpB; apply /setP_P.
by apply: intersection_greatest.
Qed.

The following gives a well-ordering on doubleton a b, even when a=b

Definition example_worder a b := (tripleton (J a a) (J b b) (J a b)).

Lemma example_worder_gleP a b x y:
    related (example_worder a b) x y <->
    [\/ (x = a /\ y = a), (x = b /\ y = b) | (x = a /\ y = b)].
Proof.
split; first by case /set3_P => h;rewrite(pr1_def h)(pr2_def h); in_TP4.
case => [] [-> ->]; apply /set3_P; in_TP4.
Qed.

Lemma example_is_worder a b:
  worder_on (example_worder a b) (doubleton a b).
Proof.
have gc:sgraph (example_worder a b).
  move => t /set3_P; case => ->; fprops.
have subs: substrate (example_worder a b) = doubleton a b.
  set_extens x.
    case/(substrate_P gc)=> [] [y].
      move / (example_worder_gleP a b x y); case; case => ->; fprops.
    move /(example_worder_gleP a b y x); case; case => _ ->; fprops.
  case /set2_P=> h; have aux: (related (example_worder a b) x x)
    by apply/(example_worder_gleP a b x x); in_TP4.
    substr_tac.
  substr_tac.
have pa: related (example_worder a b) a a by apply/example_worder_gleP; in_TP4.
have pb: related (example_worder a b) b b by apply/example_worder_gleP; in_TP4.
have pc: related (example_worder a b) a b by apply/example_worder_gleP; in_TP4.
have oc: (order (example_worder a b)).
  split => //.
    by red;rewrite subs => y /set2_P [] ->.
  move=> x y z; move /example_worder_gleP; case; move => [ -> ->]//.
    move /example_worder_gleP; case; move => [ h ->] //.
  move=> x y; move /example_worder_gleP; case;move => [ -> ->] //.
  by move /example_worder_gleP; case; case.
split; [split; [ exact | ] | exact ].
move => x xab nex.
case: (inc_or_not a x)=> hyp.
  exists a; red; rewrite (iorder_sr oc xab); split=>//.
    move=> y yx; apply /(iorder_gleP _ hyp yx); apply /example_worder_gleP.
    move: (xab _ yx); rewrite subs; case /set2_P; in_TP4.
move: nex=> [y yx]; exists y; red;rewrite (iorder_sr oc xab); split=>//.
move => z zx; apply /(iorder_gleP _ yx zx); apply /example_worder_gleP.
rewrite subs in xab.
move: (xab _ yx); case /set2_P => yb; first by case: hyp; rewrite -yb.
move: (xab _ zx); case /set2_P => zb; first by case: hyp; rewrite - zb.
in_TP4.
Qed.

Two examples of inductive sets

Lemma inductive_example1 A F: sub A (powerset F) ->
  (forall S, (forall x y, inc x S -> inc y S -> sub x y \/ sub y x) ->
    inc (union S) A) ->
  inductive (sub_order A).
Proof.
move=> Ap ih X Xs [oX tX];exists (union X).
move: (sub_osr A) => [oi si].
move: tX; aw => tX;rewrite si in Xs;
have uA: inc (union X) A.
  by apply: ih; move=> x y xX yX; move: (tX _ _ xX yX); case =>h;
   move: (iorder_gle1 h) => /sub_gleP [_ _ h1]; [left | right].
split; first by rewrite si.
move=> y yX; apply /sub_gleP;split => //;first by apply: Xs.
by apply: setU_s1.
Qed.

Lemma inductive_graphs a b:
  inductive (opp_order (extension_order a b)).
Proof.
have [or ssi] := (extension_osr a b).
have [ooi oos]:= (opp_osr or).
hnf; rewrite oos ssi => X Xs toX.
have sXs :sub X (substrate (extension_order a b)) by rewrite ssi.
have Ha:forall i, inc i X -> function i by move=> i /Xs /sfun_set_P [].
have Hb:forall i, inc i X -> target i = b by move=> i /Xs /sfun_set_P [_].
move: toX=> [orX]; aw => tor; last by ue.
set si:= Lg X source.
have Hd: forall i j, inc i (domain si) -> inc j (domain si) ->
    agrees_on ((Vg si i) \cap (Vg si j)) i j.
   rewrite /si; bw; move=> i j iX jX; bw.
   split; [by apply: subsetI2l | by apply: subsetI2r | ].
   move=> t /setI2_P [ti tj].
   case: (tor _ _ iX jX)=> h; move: (iorder_gle1 h)=> h'.
     apply: (extension_order_pr h' ti).
  symmetry; apply: (extension_order_pr h' tj).
have He:forall i, inc i (domain si) -> function_prop i (Vg si i) b.
   rewrite /si; bw; move=> i iX; red; bw;split;fprops.
move: (extension_covering He Hd) => [[fg sg tg] _ _ agg].
set g:= (common_ext si id b).
have gs: (inc g (sub_functions a b)).
  apply /sfun_set_P;split => // t tsg.
  rewrite sg in tsg; move: (setUf_hi tsg)=> [v].
  rewrite {1}/si; bw => vx; rewrite /si; bw => tv.
  by move: (Xs _ vx) => /sfun_set_P [_ sv _]; apply: sv.
exists g; red; rewrite oos ssi; split=>//.
move: agg; rewrite /si; bw => agg y yX.
move: (Xs _ yX) (agg _ yX)=> ys ag.
have fy: function y by move: ys; bw; fprops.
apply /igraph_pP; apply/extension_order_P1;split => //.
rewrite (sub_function fy fg).
move: ag; rewrite /agrees_on; bw;move=> [p1 p2 p3]; split => //.
by move=> u; symmetry; apply: p3.
Qed.

Exercise 5.3 of Bourbaki (see part 1)

Lemma exercise5_3 X i j (I:= domain X) (n := cardinal I)
   (ssI := fun k => subsets_with_p_elements k I)
   (uH := fun H => unionb (restr X H))
   (iH := fun H => intersectionb (restr X H))
   (iuH := fun k => intersectionf (ssI k) uH)
   (uiH := fun k => unionf (ssI k) iH):
   fgraph X -> inc n Bnat -> inc i Bnat -> inc j Bnat ->
   (((i = j \/ j <> \0c) -> i +c j <=c succ n -> sub (iuH i) (uiH j))
   /\ (succ n <=c i +c j -> (i = j \/ j <=c n) -> sub (uiH i) (iuH j))).
Proof.
move => fgX nB iB jB.
split.
  move => spec le1 t hyp.
  case: (equal_or_not j \0c) => jnz.
    have i0: i = \0c by case: spec => // ->.
    move: hyp; rewrite /iuH /uiH /ssI jnz i0.
    have re: (restr X emptyset) = emptyset.
      apply /set0_P => z /funI_P [a []]; case; case.
    have ->: (subsets_with_p_elements \0c I) = singleton emptyset.
      apply set1_pr.
        by apply/Zo_P; rewrite cardinal_set0;split => //; apply/setP_P; fprops.
      move => z /Zo_P [_]; apply:cardinal_nonemptyset.
    by rewrite setUf_1 setIf_1 /uH /iH re setUb_0 setIb_0.
  set A := Zo I (fun z => ~ inc t (Vg X z)); set B := I -s A.
  have AI: sub A I by apply : Zo_S.
  move: (cardinal_setC2 AI); rewrite -/n -/B.
  rewrite -(csum2_pr2b A) -(csum2_pr2a A) => eq1.
  have bp: forall z, inc z B -> inc t (Vg X z).
    move => z /setC_P [zI] /Zo_P h; ex_middle tv; case: h;split => //.
  have cbb: cardinalp (cardinal B) by fprops.
  have cba: cardinalp (cardinal A) by fprops.
  have cbB: inc (cardinal B) Bnat.
     by move: nB; rewrite eq1 => h; move: (Bnat_in_sum cbb h).
  have caB: inc (cardinal A) Bnat.
     by move: nB; rewrite eq1 => h; move: (Bnat_in_sum2 cba h).
  case: (card_le_to_el (CS_Bnat jB) cbb) => jcb.
    have [C [CB cC]]: exists C, sub C B /\ cardinal C = j.
       move: jcb; rewrite -(card_card (CS_Bnat jB)) => jcb.
       move: (proj2 (eq_subset_cardP _ _) (cardinal_le_aux1 jcb)).
       by move => [C c1 c2]; exists C;split => //; apply /card_eqP; eqsym.
     have CI: sub C I by move => s sC; move:(CB _ sC);move /setC_P => [].
     apply /setUf_P; exists C.
       by apply/ Zo_P; split => //; apply/setP_P.
     apply /setIb_P.
       apply/domain_set0P;bw; apply /nonemptyP => ce.
       by move: cC; rewrite ce cardinal_set0; apply:nesym.
     by bw;move => l lC; bw; apply: bp; apply: CB.
  have: n <c cardinal A +c j.
    rewrite eq1; rewrite csumC (csumC _ j); apply:csum_Mlteq => //.
  move /(card_le_succ_ltP _ nB) => le2.
  move: (card_leT le1 le2); rewrite csumC (csumC _ j) => eq2.
  move:(csum_le_simplifiable jB iB caB eq2) => icA.
  have [C CB cC]: exists2 C, sub C A & cardinal C = i.
     move: icA; rewrite -(card_card (CS_Bnat iB)) => icA.
     move: (proj2 (eq_subset_cardP _ _) (cardinal_le_aux1 icA)).
     by move => [C c1 c2]; exists C=> //; apply /card_eqP; eqsym.
  have CI: sub C I by move => s sC; move:(CB _ sC); apply: AI.
  have dsi:inc C (ssI i) by apply /Zo_i => //; apply /setP_P.
  move:(setIf_hi hyp dsi)=> /setUb_P [y]; rewrite restr_d.
  by move => yC; bw; move: (CB _ yC) => /Zo_P [].
move => le hij.
move => t /setUf_P [y pa pb]; apply /setIf_P.
  case: hij => jn; first by rewrite - jn; exists y.
  move: (BS_le_int jn nB) => kB.
  rewrite /ssI; apply /nonemptyP => he.
  move: (subsets_with_p_elements_pr nB kB (refl_equal n)); rewrite he.
  by rewrite cardinal_set0; move: (binom_pr3 nB kB jn).
move => z /Zo_P[/setP_P szi cz].
move /Zo_P:pa => [/setP_P syi cy].
case: (emptyset_dichot (y \cap z)) => di.
  move: (sub_smaller (setU2_12S syi szi)); rewrite (csum2_pr5 di).
  rewrite -(csum2_pr2b y) cz -(csum2_pr2a y) cy -/n.
  move => le1; move: (card_leT le le1) (card_lt_succ nB) => l1 l2; co_tac.
move: di => [l /setI2_P [jz jy]].
apply/setUf_P; exists l; bw.
have jr: inc l (domain (restr X y)) by bw.
move: (setIf_hi pb jr); bw.
Qed.

Alternate proof of Cantor Bernstein. First, any increasing function on powerset E has a fix-point. Second, assume f: E-> F and g: F-> E are injections. There is a set M such that E-M = g(F- f(M)) . The function that maps t to f(t) if t is not in this set, to the unique y in F-f(M) such that t = g(y) is a bijection E-> F.

Lemma Cantor_Bernstein_aux E (g: fterm)
  (m:= union (Zo (powerset E)(fun x=> sub x (g x)))):
  (forall x, sub x E -> sub (g x) E) ->
  (forall x y, sub x y -> sub y E -> sub (g x) (g y)) ->
  (sub m E /\ g m = m).
Proof.
move=> p1 p2; rewrite /m; set (A := Zo _ _).
have su: (sub (union A) E).
  by apply: setU_s2 => y /Zo_P [q1 q2]; apply /setP_P.
have p3: (forall x, inc x A -> sub x (g (union A))).
  move=> x /Zo_P [q1 q2];apply: (sub_trans q2); apply: p2 =>//.
  by apply setU_s1; apply: Zo_i.
have p4: (sub (union A) (g (union A))).
  by move=> t /setU_P [y ty yA]; move: (p3 _ yA) =>q; apply: q.
split => //; apply: extensionality => //.
move=> t tg;move: (p1 _ su) => p5; move: (p2 _ _ p4 p5) => p6.
by apply: (setU_i tg); apply: Zo_i => //; apply /setP_P.
Qed.

Lemma Cantor_Bernstein2_full f g
  (E:= source f) (F:= source g)
  (h:= fun x => E -s (image_by_fun g (F -s (image_by_fun f x))))
  (m:= union (Zo (powerset E) (fun x : Set => sub x (h x))))
  (T:= image_by_fun g (F -s (image_by_fun f m)))
  (p := fun a y => [/\ inc y F, ~ inc y (image_by_fun f m) & a = Vf g y])
  (f2:= Lf (fun a =>Yo (inc a T) (select (p a) F) (Vf f a)) E F):
  injection f -> injection g -> source f = target g -> source g = target f ->
  bijection_prop f2 (source f)(source g).
Proof.
move=> [ff injf] [fg injg] sf sg.
have p1: (forall x, sub x E -> sub (h x) E) by move=> x xE; apply: sub_setC.
have p2: (forall x y, sub x y -> sub y E -> sub (h x) (h y)).
  move=> x y xy yE; rewrite /h => t /setC_P [tE ti].
  apply /setC_P;split => //; dneg aux.
  have q1: sub x (source f) by apply: sub_trans yE.
  have pa: sub (F -s image_by_fun f y) (source g) by apply:sub_setC.
  have pb: sub (F -s image_by_fun f x) (source g) by apply:sub_setC.
  move /(Vf_image_P fg pa): aux => [u] /setC_P [uF nuy] Wu.
  apply /(Vf_image_P fg pb); exists u => //;apply /setC_P;split =>//; dneg aux2.
  move /(Vf_image_P ff q1): aux2 => [s sx ->]; apply /(Vf_image_P ff yE).
  by exists s=> //; apply: xy.
move: (Cantor_Bernstein_aux p1 p2) => [].
rewrite -/m /h -/T => mE hm.
have sc: sub (F -s (image_by_fun f m)) (source g) by apply: sub_setC.
set Pa := (Vf_image_P fg sc); set Pb := (Vf_image_P ff mE).
have TE: (sub T E) by move=> t /Pa [u] /setC_P [uF _] ->; rewrite /E sf; Wtac.
move: (setC_K TE); rewrite hm => cEm.
have sp: forall a, inc a T -> p a (select (p a) F).
  move => a aT; apply: (proj1 (select_pr _ _)).
    move: aT => /Pa [u] /setC_P [uF num] Wu;ex_tac.
  split => //.
  move =>x y xF [_ _ xa] yF [_ _ ya].
  by apply: injg => //; rewrite -xa -ya.
rewrite /f2/bijection_prop; aw; split => //; apply: lf_bijective.
+ move=> z zE /=;Ytac zT; [ exact (proj31 (sp _ zT)) | rewrite /F; Wtac].
+ move=> u v uE vE; rewrite /f2; Ytac uT; Ytac vT=> aux.
      move: (sp _ uT) (sp _ vT); move=> [_ _ W1] [_ _ W2]; by rewrite W1 W2 aux.
    move: (sp _ uT) => [f1u nf1i Wf1] ; case: nf1i; apply /Pb.
    by rewrite aux;exists v => //; rewrite -hm;apply /setC_P.
   move: (sp _ vT) => [f1u nf1i Wf1]; case: nf1i; apply /Pb.
     by rewrite -aux;exists u => //; rewrite -hm;apply /setC_P.
   by apply: injf.
+ move=> y yF; case: (inc_or_not y (image_by_fun f m)).
    move /Pb => [u um Wy]; exists u; first by apply: (mE).
    by rewrite /f2 Y_false //; move: um; rewrite - hm => /setC_P [].
  move=> aux; exists (Vf g y); first by rewrite /E; Wtac.
  have wt: inc (Vf g y) T by apply /Pa; exists y => //; apply /setC_P.
  rewrite /f2; Ytac0; move: (sp _ wt) => [q1 q2 q3].
  symmetry; by apply: injg.
Qed.

Lemma Cantor_Bernstein2 f g:
  injection f -> injection g -> source f = target g -> source g = target f ->
  equipotent (source f)(source g).
Proof.
move => pa pb pc pd.
move:(Cantor_Bernstein2_full pa pb pc pd).
by set f0 := Lf _ _ _ => fp; exists f0.
Qed.

Direct proof of the transfinite principle

Theorem transfinite_principle_bis r (p:property):
  worder r ->
  (forall x, inc x (substrate r) ->
    (forall y, inc y (substrate r) -> glt r y x -> p y) -> p x) ->
  forall x, inc x (substrate r) -> p x.
Proof.
move => [or wor] hyp x xsr; ex_middle npx.
set (X:=Zo (substrate r) (fun x => ~ p x)).
have neX: (nonempty X) by exists x; apply: Zo_i.
have Xsr: sub X (substrate r) by apply: Zo_S.
move:(wor _ Xsr neX)=> [y []]; aw => /Zo_P [ysr npy] yle.
case: npy; apply: hyp =>//.
move=> t tsr ty; ex_middle npt.
move: (iorder_gle1 (yle _ (Zo_i tsr npt))) => nty; order_tac.
Qed.

Let E be an ordered set and ssub F the set of strict upper bounds of F. Cantor says that E is well-ordered if E has a least element and, for any non-empty subset F, if ssub F is not empty, it has a least element. This agrees with the standard definition

Lemma cantor_worder r
   (ssub := fun E => Zo (substrate r)(fun z => forall x, inc x E -> glt r x z)):
   order r -> nonempty (substrate r) ->
   ( worder r <->
    ( (exists x, least r x)
     /\ (forall F, sub F (substrate r) -> nonempty F -> nonempty (ssub F) ->
       (exists x, least (induced_order r (ssub F)) x)))).
Proof.
move => or nesr; split.
  move => [_ wor ]; split;first by apply: worder_least.
  move => F sfr nef nef1; apply: wor => //; apply: Zo_S.
move => [[y [ysr ly]] pb]; split => //.
move => x xsr [x0 x0x].
case: (inc_or_not y x).
  move => yx; exists y; red; rewrite (iorder_sr or xsr); split => //.
  by move => t tx; apply /iorder_gleP => //; apply: ly; apply: xsr.
move => nyx.
set F:= Zo (substrate r) (fun z => forall t, inc t x -> glt r z t).
have sf1: sub F (substrate r) by apply: Zo_S.
have yf1: inc y F.
  apply: Zo_i => // t tx; split; [ apply: (ly _ (xsr _ tx)) | dneg yt; ue].
set G := ssub F.
have pa : sub x G.
  move => t tx; apply: Zo_i; first by apply: xsr.
  by move => tv /Zo_P [_ aux]; apply: aux.
have neG: nonempty G by exists x0; apply: pa.
have neF: nonempty F by exists y.
have sg: sub (ssub F) (substrate r) by apply: Zo_S.
move: (pb _ sf1 neF neG) => [a []]; rewrite (iorder_sr or sg) => aG h.
exists a; red; rewrite (iorder_sr or xsr).
have qa: forall t, inc t x -> gle r a t.
  move => t tx.
  move: (h _ (pa _ tx)) => cp1; exact (iorder_gle1 cp1).
case: (inc_or_not a x) => iax.
  by split => //; move => t tx; apply /iorder_gleP => //; apply: qa.
have aF: inc a F.
  apply: Zo_i; [by apply: sg | move => t tx; split;[ by apply: qa| dneg ta;ue]].
by move: aG => /Zo_P [_ p]; move: (p _ aF) => [_].
Qed.

We study some properties that are forbidden by the axiom of fundation

Lemma afa_ex1 x: x = powerset x -> False.
Proof.
set A := Zo x (fun z => ~ inc z z) => h.
have aux: ~(inc A A).
  move /Zo_P => [pa pb]; apply: (pb); apply/Zo_P; split => //.
apply: (aux); apply/Zo_P; split => //; rewrite h; apply /setP_P; apply:Zo_S.
Qed.

Lemma afa_ex2 a b: a = singleton b -> b = doubleton emptyset a ->
  a = singleton (powerset a).
Proof. by move => pa pb; rewrite {2} pa setP_1 - pa - pb. Qed.

Lemma afa_ex3 a b c d: a = singleton b ->
  b = (doubleton emptyset (singleton emptyset)) +s1 c +s1 d ->
  c = doubleton emptyset a -> d = singleton a ->
  a = singleton (powerset (powerset a)).
Proof.
move => pa pb pc pd; rewrite pa setP_1 {1} pb -pa; congr (singleton _).
set_extens t.
  move => h; apply/setP_P; case /setU1_P :h.
    case /setU1_P.
      case /set2_P => ->; fprops;apply : set1_sub; fprops.
    move => ->; rewrite -pc; fprops.
  move => ->; rewrite pd; apply : set1_sub; fprops.
move /setP_P => h.
case: (inc_or_not emptyset t) => ta; case: (inc_or_not a t) => tb.
- apply /setU1_P; left; apply /setU1_P; right; rewrite pc.
  by apply: extensionality => // => s; case /set2_P => ->.
- apply /setU1_P; left; apply /setU1_P; left; apply /set2_P; right.
  apply set1_pr => // s st; move: (h _ st); case /set2_P => // sa; case: tb; ue.
- apply /setU1_P; right; rewrite pd; apply set1_pr => // s st.
  move: (h _ st); case /set2_P => // sa; case: ta; ue.
- apply /setU1_P; left; apply /setU1_P; left; apply /set2_P; left.
  apply /set0_P => // s st; move: (h _ st); case /set2_P => sa.
    case: ta; ue.
  case: tb; ue.
Qed.

Lemma afa_ex4 x: x = gfunctions emptyset x <-> x = singleton emptyset.
Proof.
have aux: inc emptyset (gfunctions emptyset x).
  apply /graphset_P1;split;fprops.
     apply: fgraph_set0.
   by rewrite domain_set0.
have aux2: forall z, inc z (gfunctions emptyset x) -> z = emptyset.
  by move => z /graphset_P1 [_ pa _]; apply/ domain_set0_P.
split => h.
  by rewrite h;apply set1_pr.
symmetry; rewrite {2} h; apply /set1_pr => //.
Qed.

Lemma afa_ex5 X A: X = gfunctions X A <->
  (exists a f, [/\ A = singleton a, X = singleton f & f = singleton (J f a)]).
Proof.
split; last first.
  move => [a [f [Aa Xf fv]]].
  symmetry; rewrite {2} Xf.
  have fgg: fgraph f.
    rewrite fv; split.
    move => t /set1_P ->; fprops.
    move => s t /set1_P -> /set1_P -> ; aw.
  apply set1_pr.
    apply /graphset_P1;split => //.
      by rewrite fv domain_set1 Xf.
    move => t; rewrite fv Aa Xf => /set1_P => ->; apply: setXp_i; fprops.
  move => e /graphset_P1 [pa pb pc]; rewrite fv.
  apply: set1_pr1.
    apply /domain_set0P; rewrite pb Xf; fprops.
  move => z ze; move: (pc _ ze); rewrite Aa Xf.
  by move /setX_P => [qa ] /set1_P qb/set1_P qc; rewrite - qa qb qc.
move => xsg.
case: (emptyset_dichot X) => xne.
  empty_tac1 emptyset; rewrite {2} xsg xne.
  apply /graphset_P1;split;fprops.
    apply: fgraph_set0.
  by rewrite domain_set0.
move: xne => [f fX].
move: (fX); rewrite xsg; move => /graphset_P2 [pa pb pc].
set a := Vg f f.
have aA: inc a A.
  apply: pc; apply /range_gP => //; rewrite pb; ex_tac.
case: (equal_or_not A (singleton a)) => Aa.
  have pd: gfunctions X A = singleton f.
    apply: set1_pr; first by ue.
    move => z /graphset_P2 [qa qb qc].
    apply: fgraph_exten => //; first by ue.
    move => t td /=.
    have : inc (Vg z t) A.
      apply qc; apply /range_gP => //; rewrite qb; exists t => //; ue.
    have : inc (Vg f t) A.
      apply pc; apply /range_gP => //; rewrite pb; exists t => //; ue.
    by rewrite Aa; move => /set1_P -> /set1_P ->.
  exists a; exists f;split => //.
  apply: set1_pr; first by apply: fdomain_pr1 => //; rewrite pb.
  move => e zf; rewrite (in_graph_V pa zf).
  by move: (domain_i1 zf); rewrite pb xsg pd => /set1_P ->.
have [b bA ba]: exists2 b, inc b A & b <> a.
  ex_middle bad; case: Aa; apply: set1_pr => // z zA.
  ex_middle h; case: bad; ex_tac.
set F := Lg X (fun z => Yo (Vg z z = a) b a).
have fgf: fgraph F by rewrite /F; fprops.
have df: domain F = X by rewrite /F; bw.
have fx: inc F X.
  rewrite xsg; apply /graphset_P2;split => //.
  by move => t /(range_gP fgf) [x qa ->]; rewrite /F; bw; try ue; Ytac h.
case: (equal_or_not (Vg F F) a) => eq1.
   by case: ba; move: (eq1); rewrite {1} /F; bw; Ytac0.
by move: (eq1); rewrite {1} /F; bw; Ytac0; case.
Qed.

Lemma afa_ex6 X: X = gfunctions X X <->
  (exists2 x, X = singleton x & x = singleton (J x x)).
Proof.
split.
  move/afa_ex5 => [a [f [pa pb pc]]]; exists a => //.
  by rewrite pa in pb; rewrite {1 2} (set1_inj pb).
by move => [x pa pb]; apply /afa_ex5; exists x; exists x.
Qed.

Lemma afa_ex7 X: X = gfunctions X X <->
   X = singleton (singleton (singleton X)).
Proof.
apply (iff_trans (afa_ex6 X)).
have pa: forall t, J t t = singleton (singleton t).
  by move => t; rewrite Pair.kprE /kpair /singleton.
split.
  move => [a ab]; rewrite pa => s.
  by rewrite {1} ab; congr (singleton _); rewrite ab.
move => h; exists (singleton (singleton X)) => //.
by rewrite (pa (singleton (singleton X))) -h.
Qed.

Lemma afa_ex8 X: X = singleton X -> X = gfunctions X X.
Proof. by move => h; apply /afa_ex7; rewrite -h -h. Qed.

Lemma afa_ex9 X A: X = functions X A <->
  (exists a f, [/\ A = singleton a, X = singleton f & f = Lf (fun _ => a) X A]).
Proof.
have res: forall A a f t,
     A = singleton a -> function f -> target f = A ->
     inc t (source f) -> Vf f t = a.
  move => B a f t sf pb pc pd;move: (Vf_target pb pd).
  by rewrite pc sf => /set1_P.
split; last first.
  move => [a [f [Aa Xf fv]]].
  symmetry; rewrite {2} Xf.
  have la: lf_axiom (fun _ : Set => a) X A by move => t _; rewrite Aa; fprops.
  have aux: function (Lf (fun _ : Set => a) X A) by apply: lf_function.
  apply: set1_pr.
    apply /fun_set_P; rewrite fv;red;aw;split => //.
  move => e /fun_set_P [pa pb pc]; rewrite fv.
  apply function_exten => //; aw => z ze; aw; last by ue.
  exact: (res A a e z Aa pa pc ze).
move => xsg.
case: (emptyset_dichot X) => xne.
  move: (empty_function_tg_function A).
  set f := empty_function_tg A; move => aux.
  by empty_tac1 f; rewrite xsg xne; apply /fun_set_P.
move: xne => [f fX].
move: (fX); rewrite xsg; move => /fun_set_P [pa pb pc].
set a := Vf f f.
have aA: inc a A by rewrite -pc /a; Wtac.
case: (equal_or_not A (singleton a)) => Aa.
  have pd: functions X A = singleton f.
    apply: set1_pr; first by ue.
    move => z /fun_set_P [qa qb qc].
    apply: function_exten => //; try ue.
    move => t td /=.
    have tx: inc t (source f) by rewrite pb - qb.
    rewrite (res A a f t Aa pa pc tx).
    by rewrite (res A a z t Aa qa qc td).
  have pe: lf_axiom (fun _ => a) (functions X A) A by move => t _ /=.
  exists a; exists f;split => //.
  apply: function_exten => //.
  - by apply lf_function.
  - by aw; rewrite -xsg.
  - aw.
  - move => t tf /=; aw; first by exact: (res A a f t Aa pa pc tf).
    by move: tf; rewrite pb - xsg.
have [b bA ba]: exists2 b, inc b A & b <> a.
  ex_middle bad; case: Aa; apply: set1_pr => // z zA.
  ex_middle h; case: bad; ex_tac.
set F := Lf (fun z => Yo (Vf z z = a) b a) X A.
have ta: lf_axiom (fun z => Yo (Vf z z = a) b a) X A by move => t tX /=; Ytac h.
have fx: inc F X.
  rewrite xsg; apply /fun_set_P;rewrite /F;red;aw;split => //.
  by apply: lf_function.
case: (equal_or_not (Vf F F) a) => eq1.
   by case: ba; move: (eq1); rewrite {1} /F; aw; Ytac0.
by move: (eq1); rewrite {1} /F; aw; Ytac0; case.
Qed.

Lemma afa_ex10 X : X = functions X X <->
  (exists2 f, X = singleton f & f = triple X X (singleton (J f f))).
Proof.
have xx: forall f, X = singleton f -> f = triple X X (singleton (J f f))
    -> f = Lf (fun _ => f) X X.
  move => f Xf; set g := (singleton (J f f)) => fg.
  have fgg: fgraph g.
      split; first by move => t /set1_P ->; fprops.
    move => s t /set1_P -> /set1_P ->; aw.
  rewrite fg; apply function_exten; aw.
  + apply: function_pr => //.
      rewrite /g range_set1 - Xf; fprops.
      by rewrite domain_set1.
  + apply: lf_function => t _; rewrite -fg Xf; fprops.
  + move => t tx /=; aw; rewrite /Vf; aw.
    rewrite - fg; move: tx; rewrite Xf => /set1_P => ->.
    have pb: inc (J f f) g by rewrite /g; fprops.
    by move: (in_graph_V fgg pb); aw =>h; rewrite - (pr2_def h).
    move => _ _ /=; rewrite - fg Xf; fprops.
apply: (iff_trans (afa_ex9 X X)); split.
  move => [a [f [xa xb xc]]]; exists f => //.
  have pa: lf_axiom (fun _ => a) X X by move => t _ /=; rewrite xa; fprops.
  set g := (singleton (J f f)).
  have fgg: fgraph g.
      split; first by move => t /set1_P ->; fprops.
    move => s t /set1_P -> /set1_P ->; aw.
  rewrite xc;apply function_exten; aw.
      by apply: lf_function.
    apply: function_pr => //.
      rewrite /g range_set1 - xb; fprops.
    by rewrite domain_set1.
  move => t tx /=; aw; rewrite /Vf; aw.
  have pb: inc (J f f) g by rewrite /g; fprops.
  move: (in_graph_V fgg pb); aw =>h; move: (pr2_def h).
  move: (tx); rewrite xb => /set1_P => <- <-.
  by move: (tx); rewrite xa => /set1_P => <-.
by move => [f cf tf]; exists f; exists f;split => //; apply: xx.
Qed.

Lemma afa_ex11 X : X = functions X X <->
  X = singleton (singleton (singleton (singleton (singleton X)))).
Proof.
split; last first.
  move => h; apply /afa_ex10.
  exists (singleton (singleton (singleton (singleton X)))).
     exact.
  rewrite /triple Pair.kprE /kpair.
  by rewrite -! /(singleton _) -h -! /(singleton _).
move /afa_ex10 => [f pa pb].
have fa: f = singleton (singleton (singleton (singleton (singleton f)))).
  move: pb; rewrite pa.
  by rewrite /triple Pair.kprE /kpair - !/(singleton _).
by rewrite {1} pa fa -pa.
Qed.

Lemma afa_ex12 X : X = singleton X -> X = functions X X.
Proof. by move => h; apply /afa_ex11; rewrite -!h. Qed.

Lemma ord_div_nonzero_b a b c:
  ordinalp a -> ordinalp b -> ordinalp c ->
  a <o (ord_prod2 b c) -> b <> \0o.
Proof.
move=> oa ob oc ale.
move: (ord_gt_ne0 ale) => pz.
dneg x; rewrite x oprod0l //; apply: ordinal_pr10.
Qed.

Lemma ord_div_nonzero_b_bis a b:
  ordinalp a -> \0o <o b ->
  exists2 c, ordinalp c & a <o (b *o c).
Proof.
move=> oa bp.
move: (oprod_M1le bp (OS_succ oa)) (ord_succ_lt oa);rewrite -(ord_succ_pr oa).
move=> p1 p2; exists (a +o \1o) => //;ord_tac.
Qed.

Lemma odivision_exists_alt a b c:
  ordinalp a -> ordinalp b -> ordinalp c ->
  a <o (ord_prod2 b c) ->
  exists q r, ord_div_pr1 a b c q r.
Proof.
move=> oa ob oc.
move => [] /ordinal_le_P0; rewrite /ord_prod2.
set pbc:= (order_prod2 (ordinal_o b) (ordinal_o c)) => qa qb.
move: (conj qa qb) => a_bc; clear qa qb.
have obc: worder pbc by rewrite /pbc; fprops.
move: (ordinal_lt_pr2 obc a_bc) => [f [x [xsp rgx om]]].
have orb: order (ordinal_o b) by fprops.
have orc: order (ordinal_o c) by fprops.
have ora: order (ordinal_o a) by fprops.
move: (ordinal_o_sr b) (ordinal_o_sr c) => sb sc.
move: (xsp); rewrite orprod2_sr // setX2_P.
rewrite sb sc;move=> [fgx dx xa xb].
have [w wsb wle]: exists2 w, inc w b &
  (forall t, inc t b -> gle (ordinal_o b) w t).
  have nesb: nonempty (substrate (ordinal_o b)) by rewrite sb;ex_tac.
  move: (worder_least (ordinal_o_wor ob) nesb)=> [w [p1 p2]].
  rewrite sb in p1 p2; ex_tac.
set y := variantLc (Vg x C0) w.
have ysp: inc y (substrate pbc).
  rewrite orprod2_sr //; apply /setX2_P; rewrite sb sc /y; bw; split;fprops.
set r := (Vg x C1) ; set q := (Vg x C0).
have lt_rb: r <o b by apply /ord_ltP0; split => //; ord_tac0.
have lt_qc: q <o c by apply /ord_ltP0; split => //; ord_tac0.
have oq: ordinalp q by move: lt_qc => [[oq _] _].
have odr: ordinalp r by move: lt_rb => [[odr _] _].
have worr: worder (ordinal_o r) by fprops.
have orq: order (ordinal_o q) by fprops.
have sq :=(ordinal_o_sr q).
have sqc: sub q c by move: lt_qc => [[_ _ h] _].
have srb: sub r b by move: lt_rb => [[_ _ h] _].
exists q, r; rewrite /ord_div_pr1 /ord_div_pr0; split => //.
split => //.
have rsub: forall r A u v, order r -> sub A (substrate r) ->
  (gle (induced_order r A) u v <-> [/\ inc u A, inc v A & gle r u v]).
  move=> r0 A0 u v or Asr; split.
    move /setI2_P => [pa] /setXp_P [ua va];split => //.
  by move=> [uA vA rr]; apply /iorder_gleP.
set A:= segment pbc y.
have iuA: A = product2 q b.
  have pa: inc C0 (doubleton C0 C1) by fprops.
  have pb: inc C1 (doubleton C0 C1) by fprops.
  set_extens u.
    move /segmentP => [] /(orprod2_gleP orb orc).
    rewrite sb sc variant_V_ca variant_V_cb.
    move=> [pc v2p h] unv.
    move: pc => /setX2_P [fgu du ua ub]; apply /setX2_P => //.
    case: h;last by move /(ordo_ltP oc ua xa).
    move=> [r1 r2]; move: (wle _ ub) => r3.
    have Wv: w = (Vg u C1) by order_tac.
    case: unv;rewrite /y;apply: fgraph_exten => //; [fprops | bw |].
    rewrite du; move=> x0 x0d; try_lvariant x0d; ue.
  move /setX2_P => [fgu du ua ub].
  have uc:inc (Vg u C0) c by apply: sqc.
  apply /segmentP; split; last first.
     move => uy; case: (ordinal_irreflexive oq).
     move: ua; rewrite uy /y variant_V_ca //.
  apply /(orprod2_gleP orb orc); rewrite sb sc;split => //.
      by apply /setX2_P.
  rewrite /y;apply /setX2_P;bw;split;fprops.
  right; rewrite variant_V_ca; apply /(ordo_ltP oc uc) => //.
have ss3: substrate pbc = product2 c b by rewrite orprod2_sr // sb sc.
have ss2: sub A (substrate pbc) by apply: sub_segment.
have sA: sub A (product2 c b) by ue.
have wo2: worder (induced_order pbc A) by apply: induced_wor.
have obq: ordinalp (ord_prod2 b q) by fprops.
have ->:ord_prod2 b q = ordinal (induced_order pbc A).
  symmetry; apply: ordinal_o_isu2 => //.
  set r1 := (order_prod2 (ordinal_o b) (ordinal_o q)).
  have wo1: worder r1 by rewrite /r1; fprops.
  apply: orderIT (ordinal_o_is wo1).
  have or2:order (induced_order pbc A) by fprops.
  have or1:order r1 by fprops.
  suff: r1 = (induced_order pbc A) by move=> ->; apply: orderIR.
  apply: order_exten => // u v; split.
    move /(orprod2_gleP orb orq);rewrite sb sq; move => [pa pb pc].
    apply /iorder_gleP; try ue; apply /(orprod2_gleP orb orc).
    rewrite sb sc; split => //; try( apply :sA ; ue).
    case: pc; [ by left | move => [ /ordo_leP [sa ssb ssc] sd] ; right ].
    split => //;apply /ordo_leP;split;fprops.
  move => /iorder_gle5P [uA vA] /(orprod2_gleP orb orc) [_ _ h].
  apply /(orprod2_gleP orb orq); rewrite sb sq;split => //; try ue.
  case: h; [by left | move=> [/ordo_leP [sa ssb ssc] sd]; right].
  move: uA vA;rewrite iuA;move /setX2_P => [_ _ uq _] /setX2_P [_ _ vq _].
  split => //;apply /ordo_leP;split;fprops.
set C := induced_order pbc (segment pbc x).
have oraC: order_isomorphic C (ordinal_o a).
  have injf:= (order_morphism_fi om).
  move: om=> [o1 o2 [ff sf tf] mof].
    apply: orderIS; rewrite /C -rgx.
  have sr: sub (range (graph f)) (substrate pbc).
     rewrite - tf; fprops; apply: f_range_graph =>//.
  have o3:= (proj1(iorder_osr o2 sr)).
  have aux: (source (restriction1 f (source f))) = source f.
     rewrite /restriction1; aw.
  exists (restriction1 f (source f)); split => //.
    red; rewrite - sf; aw; split => //; first by apply: restriction1_fb.
    rewrite /restriction1; aw; rewrite -image_by_fun_source //.
  red; rewrite aux => u v usf vsf;rewrite restriction1_V // restriction1_V //.
  rewrite /pbc mof // rsub //; split; last by move => [_ _].
  move=> Wuv; split => //; Wtac.
rewrite - (ordinal_o_o oa) -(ordinal_o_o odr).
have opbc: order pbc by fprops.
symmetry;apply: orsum_invariant5 => //.
apply: orderIT oraC.
set fo:= order_sum2 _ _.
have sfo: substrate fo = canonical_du2 A r.
  by rewrite /fo orsum2_sr ;aw; fprops; rewrite ordinal_o_sr.
have ysp': inc y (product2 c b) by ue.
have xsp': inc x (product2 c b) by ue.
have lexy: gle pbc y x.
  apply /(orprod2_gleP orb orc); rewrite sb sc /y;bw; split => //; left.
  by split => //;apply: wle.
have ltAx: forall t, inc t A -> glt pbc t x.
   move =>t /segmentP lttxy; order_tac.
have rprop: forall z, inc z r -> inc (variantLc (Vg x C0) z) (product2 c b).
  move=> z zB; apply /setX2_P; bw; split;fprops.
have p1: forall z, inc z r -> gle pbc y (variantLc (Vg x C0) z).
  move=> z zB; apply /(orprod2_gleP orb orc); rewrite sb sc; split;fprops.
  by rewrite /y;bw;left; split => //; apply: wle; apply: srb.
set g := fun z => Yo (Q z = C0) (P z) (variantLc (Vg x C0) (P z)).
have ssx: sub (segment pbc x) (substrate pbc) by apply: sub_segment.
have srC: substrate C = (segment pbc x) by rewrite /C; aw.
have ta: forall z, inc z (substrate fo) -> inc (g z) (substrate C).
  move=> z; rewrite sfo; move /candu2P=> [pz xx].
  rewrite srC; apply /segmentP;case :xx.
    by move => [Pz Qz]; rewrite /g; Ytac0;apply: ltAx => //.
  move => [Pz Qz]; rewrite /g Qz; Ytac0; split; last first.
    move => bad; case: (ordinal_irreflexive odr); rewrite {1} /r -bad; bw.
  apply /(orprod2_gleP orb orc); rewrite sb sc.
  move /(ordo_ltP ob (srb _ Pz) xb): (Pz) => [pa pb].
  split; [ by apply: rprop | exact | left].
  by rewrite variant_V_ca variant_V_cb.
have bg: bijection (Lf g (substrate fo) (substrate C)).
  apply: lf_bijective => //.
    move=> u v; rewrite sfo /g; move /candu2P => [pu p3] /candu2P [pv p4].
    case: p3; case: p4; move=> [p5 p6][p7 p8];rewrite p6 p8; Ytac0; Ytac0=> aux.
    + by apply: pair_exten =>//; ue.
    + move/segmentP: p7 => lt1;move:(p1 _ p5);rewrite -aux => lt2; order_tac.
    + move/segmentP:p5 => lt1; move:(p1 _ p7); rewrite aux => lt2; order_tac.
    + by apply: pair_exten => //; [ move: (f_equal (Vg ^~ C1) aux); bw | ue ].
  move=> v; rewrite srC => /segmentP hyp.
  case: (p_or_not_p (glt pbc v y)) => aux.
    exists (J v C0); last by rewrite /g; aw; Ytac0.
    rewrite sfo; apply /candu2P; split;fprops;left.
    by aw; split => //; apply /segmentP.
  move: hyp aux => [] /(orprod2_gleP orb orc); rewrite sb sc.
  move => [vp xp aux] nvx cvy.
  case: aux; last first.
    move=> aux2; case: cvy.
    split; last by rewrite /y;move: aux2 =>[_ vx]; dneg ww; rewrite ww; bw.
    apply /(orprod2_gleP orb orc); rewrite sb sc.
    by split => //;rewrite /y; bw; right.
  move=> [sva leva].
  have vpr: v = variantLc (Vg x C0) (Vg v C1).
    move: vp => /setX2_P [a1 a2 a3 a4].
    apply: fgraph_exten => //;[ fprops | bw |].
    rewrite a2; move => z zd; try_lvariant zd.
  have ltva:glt (ordinal_o b) (Vg v C1) (Vg x C1).
    split => //; clear cvy; dneg ww; rewrite vpr ww.
    symmetry; move:xp => /setX2_P [a1 a2 _ _].
    apply: fgraph_exten => //;[ fprops | bw |].
    rewrite a2; move => z zd; try_lvariant zd.
  exists (J (Vg v C1) C1); last by rewrite /g; aw; rewrite -vpr; Ytac0.
  rewrite sfo;apply: candu2_prb => //.
  move /ordo_leP: leva => [pa pb pc].
  by apply /(ordo_ltP ob pa pb).
exists (Lf g (substrate fo) (substrate C)).
  apply: total_order_isomorphism; rewrite ? lf_source ? lf_target //.
    rewrite /fo;apply: orsum2_totalorder => //.
      apply: total_order_sub => //;apply: worder_total => //.
      apply: worder_total => //.
  apply: (proj1 (iorder_osr opbc ssx)).
rewrite sfo; rewrite sfo in ta.
have oiA: order (induced_order pbc A) by fprops.
have oor: order (ordinal_o r) by fprops.
move=> u v uc vc /=; rewrite lf_V // lf_V // /fo /C rsub //.
move /orsum2_gleP => [_ _ h]; rewrite - srC;split => //; try (apply: ta => //).
rewrite /g; case: h.
    move=> [h1 h2 h3]; Ytac0; Ytac0; apply: (iorder_gle1 h3).
  move=> [h1 h2 h3]; Ytac0; Ytac0.
  apply /(orprod2_gleP orb orc); rewrite sb sc; bw.
  move /ordo_leP: h3 => [h3 h4 h5].
  split; [by apply: rprop | by apply: rprop | left; split => //].
  by apply /ordo_leP; split => //; apply: srb.
move => [h1 h2]; Ytac0; Ytac0.
move/candu2P: uc => [_]; case; last by move => [_ bad]; case: TP_ne1; ue.
move => [/segmentP [pa _] _].
move/candu2P: vc => [_];case; [ by move=> [_] | move=> [/p1 h0 _]; order_tac].
Qed.

Lemma odiff_pr_alt a b
  (c := ordinal (induced_order (ordinal_o b) (b -s a))):
  a <=o b -> (ordinalp c /\ b = a +o c).
Proof.
move => [oa ob ab].
set F:= b -s a.
set B := ordinal_o b.
have wB: worder B by rewrite /B;fprops.
move: (ordinal_o_sr b); rewrite -/B => sB.
have Es: sub a (substrate B) by ue.
have Fs: sub F (substrate B) by rewrite sB; apply: sub_setC.
set r := induced_order B a.
set r' := induced_order B F.
have wor: worder r by apply: induced_wor.
have wor': worder r' by apply: induced_wor.
have -> : c = ordinal r' by done.
set A:= ordinal r; set C := ordinal r'.
have oA: ordinalp A by apply: OS_ordinal.
have oC: ordinalp C by apply: OS_ordinal.
split; first by exact.
have ra : r = ordinal_o a.
  apply: order_exten; fprops.
  move => x y; split => le1.
    move: (iorder_gle3 le1) => [p1 p2].
    move: (iorder_gle1 le1) => /ordo_leP [_ _ h]; apply /ordo_leP;split => //.
  move /ordo_leP: le1 => [pa pb pc]; apply /iorder_gleP => //.
  apply /ordo_leP;split;fprops.
have <-: A = a by rewrite /A ra; apply: ordinal_o_o.
rewrite /A/C - (ordinal_o_o ob).
symmetry; apply: orsum_invariant5 => //.
have orb: order B by fprops.
have or: order r by fprops.
have or': order r' by fprops.
have sr: substrate r = a by rewrite /r; aw.
have sr': substrate r' = F by rewrite /r'; aw.
have ta: forall x, inc x (substrate (order_sum2 r r'))
   -> inc (P x) (substrate B).
  move=> x; rewrite orsum2_sr // => /candu2P; rewrite sr sr'.
  by move=> [_ ]; case; move=> [pqx _]; [apply: Es |apply: Fs].
exists (Lf P (substrate (order_sum2 r r')) (substrate B)).
have xxa: total_order (order_sum2 r r').
  by apply: orsum2_totalorder; apply: worder_total.
have xxb:bijection (Lf P (substrate (order_sum2 r r')) (substrate B)).
  apply: lf_bijective => //.
    move=> x y;rewrite orsum2_sr //;move /candu2P=> [px h1] /candu2P [py h2] sp.
    apply: pair_exten =>//.
    case: h1; case: h2; move=> [Px Qx][Py Qy];rewrite Qx Qy //.
      by move: Px Py; rewrite sr sr' /F - sp; move /setC_P => [].
      by move: Px Py; rewrite sr sr' /F - sp => aux; move /setC_P => [].
  move=> y ysb; case: (inc_or_not y a) => yE.
    exists (J y C0); last by aw.
    by rewrite orsum2_sr //; apply candu2_pra; rewrite sr.
  have yF: inc y F by rewrite /F - sB; apply /setC_P; split.
  exists (J y C1); last by aw.
  by rewrite orsum2_sr //; apply :candu2_prb; rewrite sr'.
apply: total_order_isomorphism => //; aw.
move=> x y xsr ysr /=; rewrite lf_V // lf_V //.
move: xsr ysr; rewrite orsum2_sr //; move=> xsr ysr => ha.
move /orsum2_gleP:ha => [_ _ h]; case: h.
    by move=> [_ _ h1]; move: (iorder_gle1 h1).
  by move=> [_ _ h1]; move: (iorder_gle1 h1).
move => [qxa qyb].
move: xsr ysr => /candu2P [px h1] /candu2P [py h2].
case: h1; last by move=> [_]; rewrite qxa => aux; case: TP_ne.
case: h2; first by move=> [_ xx]; rewrite xx in qyb; case: qyb.
rewrite sr sr'; move=> [Py _] [Px _ ].
move: (worder_total wB)=> [_ tob].
have xb: inc (P x) (substrate B) by apply: Es.
have yb: inc (P y) (substrate B) by apply: Fs.
case: (tob _ _ xb yb) => //.
move: Py => /setC_P [_ nya] /ordo_leP [iyb ixb xy]; case: nya.
case: (ordinal_sub (ordinal_hi ob iyb) (ordinal_hi ob ixb) xy).
  by move=> ->.
apply: (ordinal_transitive oa Px).
Qed.

Lemma odiff_wrong_alt a b
  (c := ordinal (induced_order (ordinal_o b) (b -s a))):
  b <=o a -> c = \0c.
Proof.
rewrite /c; move=> [oa ob ab].
rewrite (setC_T ab).
have oon: order (ordinal_o b) by apply: ordinal_o_or.
apply: ordinal0_pr1; aw; last by fprops.
apply: (proj1 (iorder_osr oon _)); fprops.
Qed.

Lemma osum_limit_alt x y: ordinalp x -> limit_ordinal y ->
  limit_ordinal (x +o y).
Proof.
move=> ox ly.
move:(proj31 ly) => oy.
case: (ord_zero_dichot ox) => xz; first by rewrite xz osum0l //.
move /limit_ordinal_P3:ly => [ ynz yl].
move: (@osum_Meqlt \0o y x ynz ox); rewrite (osum0r ox) => lt0.
apply /limit_ordinal_P3; split; first by ord_tac.
move => z lt1.
have y1: \1o <o y by rewrite - succ_o_zero; apply: yl.
have oz: ordinalp z by ord_tac.
rewrite - (ord_succ_pr oz).
case: (ord_le_to_ee oz ox) => zx.
  exact (ord_le_ltT (osum_Mleeq zx OS1) (osum_Meqlt y1 ox)).
move: (odiff_pr zx) => [pd pe].
rewrite pe in lt1.
move: (yl _ (osum_Meqltr pd oy ox lt1)).
rewrite - (ord_succ_pr pd) => pg.
by move: (osum_Meqlt pg ox); rewrite (osumA ox pd OS1) -pe.
Qed.

Injectivity of cardinal successor, according to Bourbaki

Lemma succ_injective2 a b: cardinalp a -> cardinalp b ->
  a +c \1c = b +c \1c -> a = b.
Proof.
move=> ca cb hyp.
suff: equipotent a b.
  by move/card_eqP; rewrite (card_card ca) (card_card cb).
move: (disjointU2_pr4 a card_one) => eq1.
move: (disjointU2_pr4 b card_one) => eq2.
rewrite -hyp in eq2; clear hyp.
move: (equipotentS eq1) => [f [bf sf tf]] {eq1}.
move: (equipotentS eq2)=> [g [bg sg tg]] {eq2}.
set (A0:= image_by_fun f (a *s1 C0)).
set (B0:= image_by_fun g (b *s1 C0)).
rewrite /card_one in sf sg.
set xA:= J emptyset C0; set xB:= J emptyset C1.
have main: (forall c h, bijection h -> source h =
    (c *s1 C0) \cup ((singleton emptyset) *s1 C1) ->
    let w:= image_by_fun h (c *s1 C0) in
      let v:= Vf h xB in
       [/\ ~(inc v w), target h = w \cup (singleton v) & c \Eq w]).
  move=> c h bh sh w v.
  move: (bij_function bh)=> fh.
  have sh1:sub (c *s1 C0) (source h) by rewrite sh; apply: subsetU2l.
  have sh2: inc xB (source h).
    rewrite sh; apply: subsetU2r; rewrite /xB;apply /indexed_P;aw;split;fprops.
  split.
    move /(Vf_image_P fh sh1) => [u vs vw].
    have uW: (u = xB).
      by move: bh=> [[ _ ih] _]; apply: ih=>//; apply: sh1.
   move: vs; rewrite uW; move /indexed_P=> [_ _]; rewrite /xB; aw;fprops.
    set_extens t.
      move:bh => [_ sjh] tt; move:((proj2 sjh) _ tt)=> [y ys hy].
      rewrite sh in ys; case /setU2_P: ys => p.
        apply /setU2_P; left; rewrite -hy; apply /(Vf_image_P fh sh1); ex_tac.
      have yp: y = xB.
        move:p => /indexed_P; aw; move => [py Py Qy].
        by apply: pair_exten; rewrite /xB; aw;fprops; move /set1_P: Py.
      rewrite -hy yp -/v; apply /setU2_P; right; fprops.
    case /setU2_P.
      move /(Vf_image_P fh sh1)=> [u us ->]; Wtac.
    move /set1_P=> ->; rewrite /v; Wtac.
  eqtrans (c *s1 C0).
  exists (restriction1 h (c *s1 C0));split.
    by apply: restriction1_fb; move: bh => [ih _].
    rewrite /restriction1; aw.
    rewrite /restriction1; aw.
move: (main _ _ bf sf) (main _ _ bg sg); clear main.
simpl; fold A0 B0.
move=> [nWxfA0 tfA aA0][nWxfB0 tgB bB0].
have tfg: target f = target g by ue.
suff: equipotent A0 B0 by move=> h;eqtrans A0; eqtrans B0; eqsym.
case: (equal_or_not (Vf f xB) (Vf g xB))=> efg.
  suff: (A0 = B0) by move=> ->; fprops.
  set_extens t => ts.
    have : (inc t (target f)) by rewrite tfA; apply: subsetU2l.
    rewrite tfg tgB;case /setU2_P =>//.
    move /set1_P;rewrite -efg =>tv; case: nWxfA0; ue.
  have : (inc t (target f)) by rewrite tfg tgB; apply: subsetU2l.
  rewrite tfA; case /setU2_P =>//.
  move /set1_P; rewrite efg =>tv; case: nWxfB0; ue.
set (C0:= A0 \cap B0).
have A0v: (A0 = C0 \cup (singleton (Vf g xB))).
  set_extens t => ts.
     have : (inc t (target f)) by rewrite tfA;apply: subsetU2l.
     rewrite tfg tgB; case /setU2_P.
     by move=> tB; apply :setU2_1; apply: setI2_i.
     move /set1_P => ->; apply /setU2_P; right; fprops.
  case /setU2_P: ts; first by move/ setI2_P => [].
  move /set1_P => tu.
  have: (inc t (target f)).
       rewrite tfg tgB; apply: setU2_2; aw; ue.
  by rewrite tfA; case/setU2_P =>// /set1_P tw; case: efg; rewrite -tu -tw.
have B0v: (B0 = C0 \cup (singleton (Vf f xB))).
  set_extens t => ts.
     have : (inc t (target g)) by rewrite tgB;apply: setU2_1.
     rewrite -tfg tfA; case /setU2_P.
       by move=> tB; apply: setU2_1; apply: setI2_i.
     move /set1_P => ->; apply /setU2_2; fprops.
  case /setU2_P: ts; first by move /setI2_P => [].
  move /set1_P => tu.
  have: (inc t (target f)).
       rewrite tfA; apply: setU2_2; aw; ue.
  rewrite tfg tgB; case /setU2_P =>// /set1_P tw.
  by case: efg; rewrite -tu -tw.
rewrite A0v B0v.
apply: equipotent_disjointU2; try apply:set1_equipotent; fprops;
   apply /set0_P; move=> y; aw.
move /setI2_P => [] /setI2_P [qa qb] /set1_P qc; case: nWxfB0; ue.
move /setI2_P => [] /setI2_P [qa qb] /set1_P qc; case: nWxfA0; ue.
Qed.

End Exercise2_aux.

Module Exercise2.

Section 1

Exercise 1.1: Example of a non-order

Lemma Exercise1_1 r (E:= substrate r)
     (R := fun x y => [/\ inc x E, inc y E & glt r x y]) :
    order r -> (exists x y, x <> y /\ related r x y)
    -> [/\ transitive_r R, antisymmetric_r R & ~(reflexive_rr R)].
Proof.
move=> or [x [y [xy rxy]]]; split => //.
+ move => a b c [aE bE ab] [_ cE bc];split => //; order_tac.
+ move => a b [aE bE [ab nab]] [_ _ ba]; order_tac.
+ have sxy : R x y by red; rewrite /E;split => //; try substr_tac; split.
  by move => ref; move: (ref _ _ sxy) => [_ [_ _ [_]]].
Qed.


Exercise 1.2: Quotient of a preorder relation r by an equivalence s
We start with some auxiliary definitions

Definition Ex1_2_strong_l r s:=
  (forall x x' y, gle r x y -> related s x x' -> gle r x' y).
Definition Ex1_2_strong_r r s:=
   (forall x y y', gle r x y -> related s y y' -> gle r x y').
Definition Ex1_2_hC r s:=
  forall x y x', gle r x y -> related s x x' -> exists2 y',
    related s y y' & gle r x' y'.

Definition Ex1_2_hC' r s:=
  forall x y z, gle r x y -> gle r y z -> related s x z -> related s x y.
Definition Ex1_2_hD r f :=
   forall x y x', gle r x y -> inc x' (source f) -> Vf f x = Vf f x' ->
    exists y', [/\ inc y' (source f), gle r x' y' & Vf f y = Vf f y'].
Definition Ex1_2_hD' r r' f :=
  forall x y, inc x (source f) -> inc y (source f) ->
    gle r' (Vf f x) (Vf f y) -> exists x' y',
     [/\ Vf f x = Vf f x', Vf f y = Vf f y' & gle r x' y'].

Definition preorder_quo_axioms r s:=
  [/\ preorder r, equivalence s & substrate s = substrate r].
Definition weak_order_compatibility r s:=
  preorder_quo_axioms r s /\ Ex1_2_hC r s.

Definition increasing_pre f r r':=
 [/\ preorder r, preorder r', function_prop f (substrate r) (substrate r')
  & fincr_prop f r r'].

Definition preorder_isomorphism f r r' :=
 [/\ preorder r, preorder r', bijection_prop f (substrate r) (substrate r')
  & fiso_prop f r r'].

We can always endow the quotient with a preorder.

Definition quotient_order_r r s X Y :=
  [/\ inc X (quotient s), inc Y (quotient s) &
  forall x, inc x X -> exists2 y, inc y Y & gle r x y].

Definition quotient_order r s := graph_on (quotient_order_r r s) (quotient s).

Lemma Exercise1_2a r s:
  preorder_quo_axioms r s -> preorder_r (quotient_order_r r s).
Proof.
move=> [ [gr rr tr] es sssr]; split.
  move=> a b c [aq bq abp] [_ cq bcp];split => //.
  move => x /abp [y /bcp [z zc yz] xy]; ex_tac; apply: tr xy yz.
move=> a b [aq bq abp].
by split; split => //; move=> x xs; ex_tac; apply: rr; rewrite - sssr;
  apply: (inc_in_setQ_sr es xs).
Qed.

Lemma quotient_orderP r s x y:
  related (quotient_order r s) x y <-> quotient_order_r r s x y.
Proof.
split; [by move /Zo_hi; aw | move => h; move: (h) => [pa pb _] ].
by apply/Zo_P; aw; split => //; apply /setXp_P.
Qed.

Lemma quotient_is_preorder r s:
  preorder_quo_axioms r s -> preorder (quotient_order r s).
Proof.
by move=> h; apply: preorder_from_rel; apply: Exercise1_2a.
Qed.

Lemma substrate_quotient_order r s:
  preorder_quo_axioms r s -> substrate (quotient_order r s) = quotient s.
Proof.
move=> h;move: (quotient_is_preorder h)=> pq.
move: h => [po es ssr].
set_extens x.
  by move /(preorder_reflexivity _ pq) /quotient_orderP=> [xs _].
move=> xs; apply /(preorder_reflexivity _ pq) /quotient_orderP.
split => //; move=> y yx; ex_tac; apply /(preorder_reflexivity _ po).
rewrite - ssr; apply: (inc_in_setQ_sr es yx xs).
Qed.

Strong compatibility implies weak compatibility. Weak compatibilility says that g: E/S -> F is increasing if and only if it composition with the canonical projection is increasing E -> F.

Lemma Exercise1_2b1 r s g r':
  preorder_quo_axioms r s ->
  function g -> quotient s = source g ->
  increasing_pre (g \co (canon_proj s)) r r' ->
  increasing_pre g (quotient_order r s) r'.
Proof.
move=> [_ es sssr] fg qs [pr pr' [fc sq sr'] ale].
split => //.
    apply: quotient_is_preorder =>//.
  red; aw; rewrite substrate_quotient_order//.
  split => //; rewrite - sr'; aw.
have cc: (g \coP (canon_proj s)) by split;fprops; aw; ue.
move => x y /quotient_orderP [xq yq h].
move: (h _ (setQ_repi es xq)) => [y0 y0y aux].
have h1: (inc y0 (substrate s)) by rewrite sssr; order_tac.
have h2: (inc (rep x) (substrate s)) by rewrite sssr; order_tac.
have h0: source (canon_proj s) = substrate s by aw.
move: (ale _ _ aux); aw; try ue.
rewrite - (class_eq1 es (related_rep_in_class es yq y0y)).
by rewrite (class_rep es xq) (class_rep es yq).
Qed.

Lemma strong_order_compatibility r s:
  preorder_quo_axioms r s -> Ex1_2_strong_l r s ->
  weak_order_compatibility r s.
Proof.
move=> h1 h2; split => //.
move: h1 => [po eq ss] x y x' xy sxx'; exists y; last by apply: h2 xy sxx'.
apply: reflexivity_e => //; red in xy;rewrite ss; substr_tac.
Qed.

Lemma compatibility_proj_increasing r s:
  preorder_quo_axioms r s ->
  (weak_order_compatibility r s <->
    increasing_pre (canon_proj s) r (quotient_order r s)).
Proof.
move=> h; move: (quotient_is_preorder h) => pq.
move:(h) => [pr es sr].
rewrite /increasing_pre - sr substrate_quotient_order //; aw.
have gs: sgraph s by fprops.
split.
  move=> [_ woc]; split;fprops.
    split; fprops; aw.
  move=> x y lexy.
  have xss: inc x (substrate s) by rewrite sr; order_tac.
  have yss: inc y (substrate s) by rewrite sr; order_tac.
  apply /quotient_orderP; rewrite /quotient_order_r; aw; split;fprops.
  move=> z /(class_P es) => xz; move: (woc _ _ _ lexy xz) => [y' syy' rzy'].
  by exists y' => //;apply /(class_P es).
move=>[fc [_ _ _ _ ci]]; split => //.
move=> x y x' rxy sxx'; move: (ci _ _ rxy).
move /quotient_orderP; rewrite /quotient_order_r; move => [_ _].
have xss: inc x (substrate s) by rewrite sr; order_tac.
have yss: inc y (substrate s) by rewrite sr; order_tac.
move: sxx' => /(class_P es) sxx'.
by aw => h1; move: (h1 _ sxx') => [y'] /(class_P es) => pa pb; exists y'.
Qed.

The equivalence P x = P y is weakly compatible with order-product; In general it is not strongly compatible (unless all elements of the second set are related by the preorder).

Lemma Exercise1_2c1 r1 r2:
  preorder r1 -> preorder r2 ->
  weak_order_compatibility (order_product2 r1 r2)
  (first_proj_eq (substrate r1) (substrate r2)).
Proof.
move=> p1 p2; split;first split => //.
- by apply: order_product2_preorder.
- apply: first_proj_equivalence.
- rewrite first_proj_sr order_product2_sr1 //.
- move=> x y x' /order_product2_P [s1 s2 [rp rq]].
  move /first_proj_eq_related_P => [_ s3 sp].
  move: (s1)(s2)(s3) => /setX_P [px px1 qx2] /setX_P [py py1 qy2]
   /setX_P [px' px'1 qx'2].
  exists (J (P y) (Q x')).
    by apply /first_proj_eq_related_P; aw;split => //; apply /setXp_P.
  apply /order_product2_P; aw;split => //; first by apply /setXp_P.
  by split => //; [ ue | apply /preorder_reflexivity].
Qed.

Lemma Exercise1_2c2 r1 r2 (p :=first_proj_eq (substrate r1) (substrate r2)) :
  preorder r1 -> preorder r2 -> nonempty (substrate r1) ->
  (Ex1_2_strong_l (order_product2 r1 r2) p \/
   Ex1_2_strong_r (order_product2 r1 r2) p) ->
  r2 = coarse (substrate r2).
Proof.
move=> p1 p2 [x xr1] cp.
have p3: (preorder (order_product2 r1 r2)) by apply: order_product2_preorder.
set_extens t => ts.
  have pt: (pairp t) by move:p2=> [g1 _ _ ]; apply: g1.
  apply /setX_P;split => //; substr_tac.
move: ts => /setX_P [pt ps qs].
set (x1:= J x (Q t)); set (x2:= J x (P t)).
have x1p:inc x1 ((substrate r1) \times (substrate r2)) by rewrite /x1; fprops.
have x2p:inc x2 ((substrate r1) \times (substrate r2)) by rewrite /x2; fprops.
have r11: (gle (order_product2 r1 r2) x1 x1).
    apply /(preorder_reflexivity _ p3); rewrite order_product2_sr1 //.
have r22: (gle (order_product2 r1 r2) x2 x2).
    apply /(preorder_reflexivity _ p3); rewrite order_product2_sr1 //.
have s12: (related p x1 x2).
  apply /first_proj_eq_related_P; split => //;rewrite /x1 /x2;aw.
have s21: (related p x2 x1).
  apply /first_proj_eq_related_P; split => //;rewrite /x1 /x2;aw.
case: cp => cp.
  move: (cp _ _ _ r11 s12) => /order_product2_P [_ _ [_] ].
    by rewrite /x1 /x2; aw; rewrite - {3} pt.
  move: (cp _ _ _ r22 s21) => /order_product2_P [_ _ [_]].
    by rewrite /x1 /x2; aw; rewrite - {3} pt.
Qed.

We define here a preorder isomorphism. If P = f \co phi , where phi is the canonical projection then f is an isomorphism

Lemma Exercise1_2c4 r1 r2 f
   (s := first_proj_eq (substrate r1) (substrate r2))
   (r:= order_product2 r1 r2) :
  function f -> source f = quotient s -> target f = (substrate r1) ->
  preorder r1 -> preorder r2 -> nonempty (substrate r2) ->
  f \co (canon_proj s)=(first_proj (product (substrate r1) (substrate r2)))
  -> preorder_isomorphism f (quotient_order r s) r1.
Proof.
move=> ff sf tf p1 p2 [z zE2] cp.
set (E1:= substrate r1) in *; set (E2:= substrate r2) in *.
have sr :substrate r = E1 \times E2.
  by rewrite /r order_product2_sr1.
have ss:substrate s = E1 \times E2 by rewrite /s first_proj_sr.
have es :equivalence s by rewrite /s; apply: first_proj_equivalence.
have cpa: f \coP (canon_proj s) by split => //;aw; apply: canon_proj_f.
have pr: preorder r by rewrite /r; apply: order_product2_preorder.
have sc: (source (canon_proj s)= E1 \times E2) by aw.
have pqa: preorder_quo_axioms r s by split => //; ue.
have sq: substrate (quotient_order r s) = source f.
  rewrite substrate_quotient_order//.
have bf: bijection f.
  split.
    split; first (by exact); move => x y xs ys sW.
    have xqs: (inc x (quotient s)) by rewrite - sf //.
    have yqs: (inc y (quotient s)) by rewrite - sf //.
    have pa: inc (rep x) (substrate s) by fprops.
    have pb: inc (rep y) (substrate s) by fprops.
    apply /(related_rr_P es xqs yqs).
    apply /first_proj_eq_related_P;split => //; try ue.
    move: (pa)(pb); rewrite ss => pc pd.
    move: (pa)(pb); rewrite ss - sc=> rsx rsy.
    move: (compf_V cpa rsx) (compf_V cpa rsy).
    rewrite cp first_proj_V // first_proj_V // => -> ->.
    by aw; rewrite (class_rep es xqs) (class_rep es yqs).
  split => //.
  rewrite tf => y ye1.
  have Js: (inc (J y z) (source (canon_proj s))) by ue.
  have ->: (source f = target (canon_proj s)) by aw.
  exists (Vf (canon_proj s) (J y z)); fprops.
  rewrite - (compf_V cpa Js) cp first_proj_V //; [ aw| ue].
split => //; first by apply: quotient_is_preorder => //; ue.
move=> x y xsf ysf.
set (u:= Vf f x); set (v:= Vf f y).
have xqs: (inc x (quotient s)) by rewrite - sf //.
have yqs: (inc y (quotient s)) by rewrite - sf //.
have pa: inc (rep x) (substrate s) by fprops.
have pb: inc (rep y) (substrate s) by fprops.
move: (pa)(pb); rewrite ss => rxp ryp.
move: (pa)(pb); rewrite ss - sc=> rsx rsy.
move: (compf_V cpa rsx) (compf_V cpa rsy).
rewrite cp first_proj_V // first_proj_V //.
aw; rewrite (class_rep es xqs) (class_rep es yqs) -/u -/v => pc pd.
have rx: (inc (rep x) x) by apply: (setQ_repi es xqs).
split.
  move/quotient_orderP => [_ _ h].
  move: (h _ rx) => [w wy].
  move /order_product2_P => [rpx wp [le1 le2]].
  move: (is_class_pr es wy yqs) => yc.
  have ws: (inc w (substrate s)) by apply:(inc_in_setQ_sr es wy yqs).
  move: (related_rep_class es ws).
  by rewrite -yc -pc -pd ; move /first_proj_eq_related_P => [_ rys <-].
move=> h; apply/quotient_orderP; split => // w wx.
move: (inc_in_setQ_sr es wx xqs); rewrite ss.
move=> wpr; move: (wpr) => /setX_P [pw Pw Qw].
have JP: (inc (J v (Q w)) ((substrate r1) \times (substrate r2))).
  apply /setXp_P;split => //; rewrite /v -/E1 -tf; Wtac.
exists (J v (Q w)).
  rewrite - (class_rep es yqs); apply /(class_P es).
  apply /first_proj_eq_related_P; split => //; aw.
apply /order_product2_P; split => //; aw;split; last first.
  by move: p2=> [_ aa _]; apply: aa.
move: (is_class_pr es wx xqs) => xc.
have ws: (inc w (substrate s)) by apply: (inc_in_setQ_sr es wx xqs).
move:(related_rep_class es ws).
rewrite -xc; move /first_proj_eq_related_P => [_ _ ->];ue.
Qed.

We give here a sufficient condition for the quotient to be an order

Lemma Exercise1_2d r s:
  equivalence s -> order r -> substrate s = substrate r ->
  Ex1_2_hC' r s ->
  order (quotient_order r s).
Proof.
move => es or ss qoa.
move: (order_preorder or) => pr.
have pqa: preorder_quo_axioms r s by split => //.
move: (quotient_is_preorder pqa) => [p1 p2 p3].
split => //.
suff sxy: forall x y, related (quotient_order r s) x y ->
   related (quotient_order r s) y x -> sub x y.
  move=> x y xs ys; apply: extensionality; apply: sxy => //.
move=> x y /quotient_orderP [xs ys q1] /quotient_orderP [_ _ q2] t tx.
move: (q1 _ tx) => [z zy tz] ; move: (q2 _ zy) => [w wt zw].
have tw: (related s t w).
  by apply /(in_class_relatedP es); exists x; split => //; apply /(setQ_P es).
rewrite (is_class_pr es zy ys);apply /(class_P es); apply: (symmetricity_e es).
exact: (qoa _ _ _ tz zw tw).
Qed.

Bourbaki says: there are examples of totally ordered sets E with four elements such that the quotient is ordered, and none of the two conditions is satisfied. We first show that E/S is isomorphic to a subset of E (two classes compare the same as their greatest element). If a < b < c, the equivalence relation that relates a and c, but is otherwise trivial satisfies none of the two conditions.

Lemma Exercise1_2e1 r s:
  equivalence s -> total_order r -> substrate s = substrate r ->
  finite_set (substrate r) ->
  total_order (quotient_order r s).
Proof.
move => eqs tor ssr fs.
move: (proj1 tor) => or.
move: (order_preorder or) => pr.
move: (quotient_is_preorder (And3 pr eqs ssr)) => [p1 p2 p3].
pose gr x := (the_greatest (induced_order r x)).
have gp: forall x, sub x (substrate r) -> nonempty x ->
  (inc (gr x) x /\ forall y, inc y x -> gle r y (gr x)).
  move => x xsr nex.
  have fsx: finite_set x by exact(sub_finite_set xsr fs).
  move: (finite_subset_torder_greatest tor fsx xsr nex) => h.
  move:(iorder_osr or xsr) => [pa' pb'].
  move: (the_greatest_pr pa' h).
  rewrite -/ (gr x); move => []; rewrite pb'.
  move => pa pb; split => // y yx; exact (iorder_gle1 (pb _ yx)).
have gp1: forall x, inc x (quotient s) ->
  (inc (gr x) x /\ forall y, inc y x -> gle r y (gr x)).
  move => x xq; apply: gp.
     move => t tx; rewrite - ssr; apply: (inc_in_setQ_sr eqs tx xq).
  exact (setQ_ne eqs xq).
have paP: forall x y, related (quotient_order r s) x y <->
  [/\ inc x (quotient s),inc y (quotient s) & gle r (gr x) (gr y)].
  move => x y; apply: (iff_trans (quotient_orderP r s x y)).
  split; move => [pa pb pc];split => //.
    move: (gp1 _ pa) (gp1 _ pb)=> [qa _][_ qd].
    move: (pc _ qa); move => [z zy le1];move: (qd _ zy) => l2; order_tac.
  move => t tx.
  move: (gp1 _ pa) (gp1 _ pb)=> [_ qb][qc _]; ex_tac.
  move: (qb _ tx) => le1; order_tac.
split.
  split => //.
  move => x y /paP [xq yq le1] /paP [_ _ le2].
  have sv: (gr x) = (gr y) by order_tac.
  move: (gp1 _ xq) (gp1 _ yq) => [xs _] [ys _].
  by rewrite (is_class_pr eqs xs xq) (is_class_pr eqs ys yq) sv.
rewrite (substrate_quotient_order (And3 pr eqs ssr)) => x y xsr ysr.
move: (gp1 _ xsr) (gp1 _ ysr) => [xs _] [ys _].
move: (inc_in_setQ_sr eqs xs xsr) ; rewrite ssr => x1.
move: (inc_in_setQ_sr eqs ys ysr) ; rewrite ssr => y1.
by case: (proj2 tor _ _ x1 y1) =>h; [left | right]; apply /paP.
Qed.

Lemma Exercise1_2e2 r a b c (E:= substrate r)
  (s := (diagonal E) \cup (doubleton (J a c) (J c a))):
  order r -> glt r a b -> glt r b c ->
  [/\ equivalence s, substrate s = substrate r,
  ~ ( weak_order_compatibility r s) &
  ~ ( Ex1_2_hC' r s)].
Proof.
move => or lab lbc.
have asr: inc a (substrate r) by order_tac.
have csr: inc c (substrate r) by order_tac.
have gs: sgraph s.
  move => t; case /setU2_P; first by move /diagonal_i_P => [].
  case /set2_P => ->; fprops.
have pa: forall u v, inc (J u v) s -> (inc u E /\ inc v E).
  move => u v; case /setU2_P; first by move /diagonal_pi_P => [pa <-].
  by case /set2_P => h; rewrite (pr1_def h) (pr2_def h).
have pb: forall t, inc t E -> inc (J t t) s.
  by move => t te; apply /setU2_P; left; apply /diagonal_pi_P.
have sr: substrate s = E.
  set_extens t.
    by move /(substrate_P gs);case;move => [y js]; move: (pa _ _ js) => [qa qb].
  move => te; move: (pb _ te) => h; substr_tac.
have es: equivalence s.
  split => //.
      red; rewrite sr => t; apply pb.
    move => x y z => aux.
    move: (aux); case /setU2_P;[by move /diagonal_pi_P => [_ <-] | move => sxy].
    case /setU2_P; first by move /diagonal_pi_P => [_ <-].
    move => sxz; case /set2_P: sxy => h; rewrite (pr1_def h);
       case /set2_P: sxz => h1; rewrite (pr2_def h1); try (apply:pb => //);
         apply /setU2_P; right; fprops.
  move => x y; case /setU2_P => h; apply /setU2_P.
    by move /diagonal_pi_P: h => [p1 <-]; left; apply /diagonal_pi_P.
  right;case /set2_P: h => h; rewrite (pr1_def h) (pr2_def h);fprops.
have ra: related s a c by apply /setU2_P; right; fprops.
have pc: ~ weak_order_compatibility r s.
  move => [_ pc]; move: (pc a b c (proj1 lab) ra) => [z].
  case /setU2_P; first by move /diagonal_pi_P => [_ <-] => cb; order_tac.
  case /set2_P => h; first by case: (proj2 lab); rewrite (pr1_def h).
  by case: (proj2 lbc); rewrite (pr1_def h).
have pd //: ~ Ex1_2_hC' r s.
  move => hh; move: (hh a b c (proj1 lab) (proj1 lbc) ra).
  case /setU2_P => h;first by case:(proj2 lab);move /diagonal_pi_P :h => [_ <-].
  case /set2_P: h => h; first by case: (proj2 lbc); rewrite (pr2_def h).
  by case: (proj2 lab); rewrite (pr2_def h).
Qed.

Lemma Exercise1_2e3 E: \3c <=c cardinal E ->
  exists a b c,
  [/\ inc a E, inc b E, inc c E & [/\ a <> b, a <> c & b <> c]].
Proof.
rewrite /card_three - (card_card (CS_succ \2c)) (succ_of_Bnat BS2).
move /eq_subset_cardP1 /eq_subset_ex_injP => [f [[ff injf] sf tf]].
exists (Vf f \0c); exists (Vf f \1c); exists (Vf f \2c).
have zs: inc \0c (source f).
  by rewrite sf; apply /setU1_P; left; apply /set2_P; left.
have os: inc \1c (source f).
  by rewrite sf; apply /setU1_P; left; apply /set2_P; right.
have ts: inc \2c (source f) by rewrite sf; apply /setU1_P; right.
rewrite -tf;split; fprops; split=> h.
by move: (injf _ _ zs os h); fprops.
by move: (injf _ _ zs ts h); fprops.
by move: (injf _ _ os ts h); fprops.
Qed.

Lemma Exercise1_2e4 r: total_order r ->
  \3c <=c cardinal (substrate r) ->
  exists a b c, glt r a b /\ glt r b c.
Proof.
move => [or tor] c3; rewrite /glt.
move: (Exercise1_2e3 c3) => [a [b [c [ae be ce [ab bc ac]]]]].
case: (tor _ _ ae be) => h1; case: (tor _ _ be ce) => h2.
      by exists a; exists b; exists c.
    case: (tor _ _ ae ce) => h3.
      exists a; exists c; exists b; fprops.
    exists c; exists a; exists b; fprops.
  case: (tor _ _ ae ce) => h3.
    exists b; exists a; exists c;fprops.
  exists b; exists c; exists a; fprops.
exists c; exists b; exists a; fprops.
Qed.

Lemma Exercise1_2e5 r:
  total_order r -> finite_set (substrate r) ->
  \3c <=c cardinal (substrate r) ->
  exists s,
  [/\ equivalence s, substrate s = substrate r,
    total_order (quotient_order r s),
  ~ ( weak_order_compatibility r s) &
  ~ ( Ex1_2_hC' r s) ].
Proof.
move => tor fso c3.
move: (Exercise1_2e4 tor c3) => [a [b [c [ab bc]]]].
move: (Exercise1_2e2 (proj1 tor) ab bc).
set s := union2 _ _; move => [es ss pa pb]; exists s;split => //.
by apply: Exercise1_2e1.
Qed.

Consider the equivalence induced by an increasing function f:E -> F. The second condition is alwats true; the first is equivalent to some condition CC. If f = g \co phi is the canonical decomposition then g: E/S -> f(E) is an isomorphism iff CC and DD hold

Lemma Exercise1_2f1 r r' f: increasing_fun f r r' ->
  Ex1_2_hC' r (equivalence_associated f).
Proof.
move => [or or' [ff sr sr'] icf].
move=> x y z xy yz.
move: (icf _ _ xy)(icf _ _ yz) => fxy fyz.
move /(ea_relatedP ff) => [xsf ysf sw]; apply /(ea_relatedP ff).
rewrite - sw in fyz; rewrite sr; split => //;order_tac.
Qed.

Lemma Exercise1_2f2 r r' f: increasing_fun f r r' ->
  (weak_order_compatibility r (equivalence_associated f) <->
  (Ex1_2_hD r f)).
Proof.
move => [or or' [ff sr sr'] icf].
rewrite /weak_order_compatibility.
split.
  move=> [[pr ea sea] ch] x y x' xy x'sf sW.
  have aux: (related (equivalence_associated f) x x').
    apply /ea_relatedP => //; split => //.
     rewrite sr; order_tac.
  move: (ch _ _ _ xy aux) => [y' eay' x'y'].
  move: aux eay'=> _ /(ea_relatedP ff) [pa pb pc].
  by exists y'.
move=> ch; split; first split.
      by apply: order_preorder.
    by apply: graph_ea_equivalence.
  by rewrite graph_ea_substrate.
move=> x y y' xy /(ea_relatedP ff) [xsf ysf sv].
move: (ch _ _ _ xy ysf sv) => [z [zf y'z sv1]].
exists z=> //; apply /(ea_relatedP ff);split => //; rewrite sr; order_tac.
Qed.

Lemma Exercise1_2f3 r r' f g:
  increasing_fun f r r' ->
  composable g (canon_proj (equivalence_associated f)) ->
  f = compose g (canon_proj (equivalence_associated f)) ->
  (order_morphism g (quotient_order r (equivalence_associated f)) r'
    <-> (Ex1_2_hD r f /\ Ex1_2_hD' r r' f)).
Proof.
move => incf cgf fc.
move: (Exercise1_2f1 incf) => qoa.
set (s:= equivalence_associated f) in *.
move: incf => [or or' [ff sr sr'] icf].
have es : equivalence s by rewrite /s; apply: graph_ea_equivalence.
have ss: substrate s = substrate r by rewrite /s graph_ea_substrate.
have pr :preorder r by apply: order_preorder.
have qp: forall x, inc x (quotient s) -> (inc (rep x) (source f) /\
    Vf f (rep x) = Vf g x).
  move=> x xq; move: (rep_i_sr es xq) => rxs.
  split; first by rewrite sr - ss.
  move: (canon_proj_V rxs); rewrite class_rep // => cpv.
  have rsc: inc (rep x) (source (canon_proj s)) by aw.
  have: (Vf g (Vf (canon_proj s) (rep x)) = Vf g x) by rewrite cpv.
     rewrite - compf_V // -fc //.
have bpP :forall x, inc x (quotient s) -> forall a,
   (inc a x <-> [/\ inc (rep x) (source f), inc a (source f) &
     Vf f (rep x) = Vf f a]).
  move=> x xq a; split.
   by move=> ax; move: (related_rep_in_class es xq ax); move /(ea_relatedP ff).
  move=> h;rewrite -(class_rep es xq); apply /(class_P es).
  by apply /(ea_relatedP ff).
split.
  move=> om.
  have p1: forall x y x', inc x (source f) -> inc y (source f) ->
      gle r' (Vf f x) (Vf f y) -> inc x' (class s x) ->
      exists y', [/\ inc y' (source f), gle r x' y' & Vf f y = Vf f y'].
    move=> x y x' xsf yxsf lext x'x.
    have xs: (inc x (substrate s)) by rewrite ss - sr.
    have csxq: (inc (class s x) (quotient s)) by fprops.
    have: (inc x (class s x)) by apply: inc_itself_class.
    move /(bpP _ csxq) => [p3 p4 p5]; move: (qp _ csxq) =>[p1 p2].
    rewrite -p5 p2 in lext.
    have ys: (inc y (substrate s)) by rewrite ss - sr.
    have csyq: (inc (class s y) (quotient s)) by fprops.
    have: (inc y (class s y)) by apply: inc_itself_class.
    move / (bpP _ csyq) => [p3' p4' p5']; move: (qp _ csyq) => [p1' p2'].
    rewrite -p5' p2' in lext.
    move: om => [q1 q2 [q3 q4 q5]].
    rewrite /fiso_prop; rewrite q4 substrate_quotient_order // => q6P.
    move: lext => /(q6P _ _ csxq csyq) /quotient_orderP [_ _ q7].
    move: (q7 _ x'x) => [u ucy xu]; exists u.
    move: ucy => /(bpP _ csyq) [q8 q9 q10].
    by rewrite p5' in q10.
  split.
    move => x y x' xy x'sf sW.
    move: (icf _ _ xy); rewrite sW => fxy.
    have xc: (inc x'(class s x')) by apply:inc_itself_class=>//;rewrite ss - sr.
    have yc: (inc y (source f)) by rewrite sr; order_tac.
    apply: p1 x'sf yc fxy xc.
  move=> x y xsf ysf leW.
  have xc: (inc x (class s x)) by apply: inc_itself_class=>//; rewrite ss - sr.
  move: (p1 _ _ _ xsf ysf leW xc) => [x0 [p0 p2 p3]].
  by exists x; exists x0.
move=> [CCt DDt].
have oq: (order (quotient_order r s)) by apply: Exercise1_2d.
have sg: (source g = quotient s) by move: cgf => [_ _ ->]; aw.
have tg: substrate r' = target g by rewrite - sr' fc; aw.
have sqo: substrate (quotient_order r s) = source g.
  by rewrite sg substrate_quotient_order.
have icgP: (forall x y, inc x (source g) -> inc y (source g) ->
    (gle (quotient_order r s) x y <-> gle r' (Vf g x) (Vf g y))).
  rewrite sg;move=> x y xsg ysg.
  move: (qp _ xsg) (qp _ ysg) => [rxs Wrx][rys Wry].
  rewrite -Wrx -Wry; split.
    move /quotient_orderP => [_ _ aux].
    move: (aux _ (setQ_repi es xsg)) => [z zy lerxz].
    by move: zy => /(bpP _ ysg) [q1 q2 q3]; rewrite q3; apply: icf.
  move => h; apply /quotient_orderP; split => //; move=> z.
  move /(bpP _ xsg) => [p4 p5 p6].
  move: (DDt _ _ rxs rys h) => [x' [y' [p1 p2 p3]]].
  rewrite p1 in p6.
  move: (CCt _ _ _ p3 p5 p6) => [t [p7 p8 p9]].
  exists t=> //;apply /(bpP _ ysg); split => //; ue.
have fg: function g by fct_tac.
done.
Qed.


Exercise 1.3: properties of ordinal sum

Section Exercise1_3a.
Variables r g: Set.
Definition E13_F:= order_sum r g.
Definition E13_sF:= sum_of_substrates g.
Definition E13_lam := second_proj E13_sF.
Definition E13_S:= equivalence_associated (second_proj E13_sF).
Definition E13_H1:= orsum_ax r g.
Definition E13_H2:= sgraph g /\
   forall i, inc i (domain g) -> nonempty (substrate (Vg g i)).

We know thar order_sum is an ordering under condition E13_H1. Let E(i) denote the i-th sustbrate and F(i) its image in the disjoint union E13_sF. If E13_H2 holds, then F(i) form a partition of the disjoint union; moreover the second projection Q (more precisely E13_lam) is surjective.

Lemma Exercise1_3a0: function E13_lam.
Proof. rewrite /E13_lam; apply: second_proj_f =>//. Qed.

Lemma Exercise1_3a1: sgraph E13_sF.
Proof.
move=> t /setUb_P [y]; rewrite /fam_of_substrates.
rewrite Lg_domain; bw; move => yd; rewrite /disjointU_fam; bw.
by move /indexed_P => [].
Qed.

Lemma Exercise1_3a2: surjection E13_lam.
Proof.
split; first by apply: Exercise1_3a0.
rewrite /E13_lam => y.
rewrite {1 2}/second_proj; aw; move /(rangeP Exercise1_3a1) => [x h].
ex_tac; rewrite second_proj_V //; aw.
Qed.

Lemma Exercise1_3a3: E13_H2 -> domain g = target E13_lam.
Proof.
move=> [gg alne]; rewrite /E13_lam /second_proj; aw.
move: Exercise1_3a1 => gE.
set_extens t.
  move=> tg;move: (alne _ tg) => [u us]; apply /(rangeP gE).
  exists u; apply: disjoint_union_pi1 =>//.
by move /(rangeP gE) => [x Je]; move: (du_index_pr1 Je); aw; move => [].
Qed.

Lemma Exercise1_3a3': substrate E13_S = E13_sF.
Proof.
rewrite/ E13_S graph_ea_substrate /second_proj; aw; apply: second_proj_f.
Qed.

Lemma Exercise1_3a3'': substrate E13_S = source E13_lam.
Proof. rewrite Exercise1_3a3'/E13_lam/second_proj; aw. Qed.

Lemma Exercise1_3a4: E13_H1 -> E13_H2 -> increasing_fun E13_lam E13_F r.
Proof.
move=> h1 h2; move:(h1) => [p2 p3 p4]; split => //.
    apply: (orsum_or h1).
  split => //.
      apply: Exercise1_3a0.
    by rewrite (orsum_sr h1) /E13_lam /second_proj /E13_F; aw.
  rewrite -(Exercise1_3a3 h2) //.
move=> x y h3; move: (orsum_gle_id h1 h3).
move: h3 => /orsum_gleP [xs ys xy] h4.
rewrite / E13_lam second_proj_V // second_proj_V //.
Qed.

We consider the function disjointU_function f that maps i to F(i); and the associated equivalence (two elements are related if they are in the same F(i)). We show that this the equivalence associated to E13_lam and two elements are related if they have the same second projection

Definition disjointU_function f :=
  triple (domain f)(range (disjointU_fam f))(disjointU_fam f).

Lemma disjointU_function_pr f:
  function (disjointU_function f) /\
  graph (disjointU_function f) = (disjointU_fam f).
Proof.
rewrite / disjointU_function /disjointU_fam.
split; last (by aw); apply: function_pr; [ fprops | fprops | bw].
Qed.

Lemma Exercise1_3a5P x y (f := fam_of_substrates g) :
  related (partition_relation (disjointU_function f) (disjointU f))
  x y <-> [/\ inc x E13_sF, inc y E13_sF & Q x = Q y].
Proof.
rewrite / E13_sF -/f.
move: (disjointU_function_pr f) => [p1 p2].
have p3:partition_w_fam (graph (disjointU_function f)) (disjointU f).
  rewrite p2; apply: partition_disjointU; apply: fos_graph.
apply: (iff_trans (isc_rel_P p1 p3 x y)).
rewrite /in_same_coset/Vf/disjointU/disjointU_function; aw.
rewrite /disjointU_fam; split.
  move=> [i [idf]]; bw; rewrite /sum_of_substrates -/f.
  move=> /indexed_P [px pxv qx] /indexed_P [py pyv qy].
  rewrite qx qy -px -py; split => //; apply: disjointU_pi; ue.
have ->: domain f = domain g by rewrite /f/fam_of_substrates; bw.
move=> [xsg ysg sq].
move: (du_index_pr1 xsg) (du_index_pr1 ysg)=> [qxd pxs px][_ pys py].
rewrite /f/fam_of_substrates;exists (Q x).
split => //; bw; apply /indexed_P;split => //; ue.
Qed.

Lemma Exercise1_3a6P x y:
  related E13_S x y <-> [/\ inc x E13_sF, inc y E13_sF & Q x = Q y].
Proof.
move: Exercise1_3a1 Exercise1_3a0 => gs fl.
have ss: (source (second_proj E13_sF) = E13_sF) by rewrite /second_proj; aw.
apply: (iff_trans (ea_relatedP fl x y)); rewrite ss.
split; move=> [xs ys]; rewrite !second_proj_V //.
Qed.

We show that E13_S is an equivalence, satisfying the two conditions of the previous Exercise. Let E13_lam = g \co phi be the canonical decomposition, where phi is the canonical projection of E13_S. Then g is an order isormorphism (its target is the set of indices i).

Lemma Exercise1_3a7: equivalence E13_S.
Proof. rewrite /E13_S; apply: graph_ea_equivalence; apply: Exercise1_3a0. Qed.

Lemma indexed_p2 a b c: inc a (b *s1 c) -> Q a = c.
Proof. by move /indexed_P => [_ _]. Qed.

Lemma Exercise1_3a8P a: E13_H2 ->
  (inc a (quotient E13_S) <-> exists2 i,
    inc i (domain g) & a = (Vg (fam_of_substrates g) i) *s1 i).
Proof.
move: Exercise1_3a7 => es h2.
have df : domain (fam_of_substrates g) = domain g.
   by rewrite /fam_of_substrates;bw.
have aux: forall i, inc i (domain g) ->
  (Vg (fam_of_substrates g) i = substrate (Vg g i)).
  move=> i idg; rewrite /fam_of_substrates;aw; bw.
split.
  move => aq; set y := rep a.
  have ysf: (inc y E13_sF) by rewrite -Exercise1_3a3'; apply: (rep_i_sr es aq).
  move: (disjointU_hi ysf); rewrite df; move => [Qx Px px];ex_tac.
  move/(setQ_P es): aq => aq.
  set_extens t.
    move => ta; move: (rel_in_class es aq ta) => /Exercise1_3a6P.
    move=> [_ tsf Qyt]; move: (disjointU_hi tsf)=> [Qt Pt pt].
    rewrite Qyt; apply /indexed_P;split => //.
  move /indexed_P => [pt Pt Qt]; apply/ (rel_in_class2 es aq).
  apply /Exercise1_3a6P;split => //; rewrite - pt Qt.
  by apply:disjoint_union_pi1 => //;rewrite - aux.
move=> [i idg ap]; rewrite (aux _ idg) in ap; apply /(setQ_P es).
have sa: sub a E13_sF.
  move=> t; rewrite ap => /indexed_P [pt Pt Qt].
  rewrite - pt Qt; apply: disjoint_union_pi1=> //.
have ra: inc (rep a) a.
  apply: rep_i; exists (J (rep (substrate (Vg g i))) i); rewrite ap.
  by apply: indexed_pi; apply: rep_i; apply: (proj2 h2).
split; first by rewrite Exercise1_3a3'; apply: sa.
have qa : Q (rep a) = i by rewrite {2} ap in ra; move: (indexed_p2 ra).
set_extens t.
  move => ta; apply /(class_P es) /Exercise1_3a6P;split;fprops.
  by rewrite ap in ta; rewrite (indexed_p2 ta).
move/ (class_P es) /Exercise1_3a6P => [pa pb pc]; rewrite ap.
move: (disjointU_hi pb) => [pd pe <-]; rewrite -pc qa.
by apply : indexed_pi; rewrite - aux // -qa pc.
Qed.

Lemma Exercise1_3a9: function (fun_on_quotient E13_S E13_lam).
Proof.
move: Exercise1_3a0 => aux.
by apply: foqc_f => //;[ apply: Exercise1_3a7 | rewrite Exercise1_3a3''].
Qed.

Lemma Exercise1_3a10:
  (fun_on_quotient E13_S E13_lam) \coP (canon_proj E13_S).
Proof.
split => //; first by apply: Exercise1_3a9.
  apply: canon_proj_f; apply: Exercise1_3a7.
rewrite /fun_on_quotient/section_canon_proj; aw.
Qed.

Lemma Exercise1_3a11:
  E13_lam = (fun_on_quotient E13_S E13_lam) \co (canon_proj E13_S).
Proof. apply: (canonical_decomposition_surj2 Exercise1_3a2). Qed.

Lemma Exercise1_3a12 x: E13_H2 ->
  inc x (quotient E13_S) -> exists i,
    [/\ inc i (domain g), x = (Vg (fam_of_substrates g) i) *s1 i &
    Vf (fun_on_quotient E13_S E13_lam) x = i].
Proof.
move: Exercise1_3a0 Exercise1_3a7 => fl es h2 xq.
move : (xq) => /(Exercise1_3a8P x h2) [i idg xp].
ex_tac.
have sl: source E13_lam = substrate E13_S by rewrite Exercise1_3a3''.
rewrite foqc_V //.
have <-: (Q (rep x) = Vf E13_lam (rep x)).
  by rewrite /E13_lam second_proj_V // -Exercise1_3a3'; apply: rep_i_sr.
have:(inc (rep x) x) by apply: (rep_in_class es); apply /(setQ_P es).
by rewrite {2} xp; move /indexed_P => [_ _].
Qed.

Lemma Exercise1_3a13: E13_H2 -> bijection (fun_on_quotient E13_S E13_lam).
Proof.
move => h2.
have sfoq: source (fun_on_quotient E13_S E13_lam) = quotient E13_S.
  by rewrite /fun_on_quotient /section_canon_proj; aw.
move: Exercise1_3a9=> ffoq.
split.
  split => //; rewrite sfoq => x y xq yq.
  move: (Exercise1_3a12 h2 xq) (Exercise1_3a12 h2 yq).
  by move => [i [_ p1 p2]] [j [_ p3 p4]]; rewrite p2 p4 p1 p3; move => ->.
split => // y.
rewrite sfoq {1} /fun_on_quotient; aw; rewrite -(Exercise1_3a3 h2) => yd.
set (a:= Vg (fam_of_substrates g) y *s1 y).
have aq: (inc a (quotient E13_S)) by apply /(Exercise1_3a8P _ h2); ex_tac.
ex_tac.
move: (Exercise1_3a12 h2 aq) => [i [idg p1 ->]].
have h:= (setQ_repi Exercise1_3a7 aq).
rewrite -(indexed_p2 h).
by rewrite {2} p1 in h; rewrite -(indexed_p2 h).
Qed.

Lemma Exercise1_3a14: E13_H1 -> E13_H2 ->
  [/\ Ex1_2_hC E13_F E13_S, Ex1_2_hC' E13_F E13_S,
  Ex1_2_hD E13_F E13_lam & Ex1_2_hD' E13_F r E13_lam].
Proof.
move=> h1 h2.
move: (orsum_sr h1); rewrite -/E13_sF -/E13_F => s1.
move: (orsum_or h1) => o1.
have pa: Ex1_2_hC E13_F E13_S.
  move => x y z r1 r2.
  move: r2 => /Exercise1_3a6P [xs sz qxz].
  have ys: inc y E13_sF by rewrite - s1; order_tac.
  case: (equal_or_not (Q x) (Q y)) => qxy.
    exists z; last by order_tac; rewrite s1.
    apply /Exercise1_3a6P;split => //; ue.
  exists y; first by apply /Exercise1_3a6P.
  apply /orsum_gleP; split => //; left; rewrite -qxz; split; last by exact.
  exact (orsum_gle_id h1 r1).
have pb:Ex1_2_hC' E13_F E13_S.
  move => x y z r1 r2.
  move: (orsum_gle_id h1 r1) (orsum_gle_id h1 r2) => q1 q2.
  move: r1 r2 => /orsum_gleP [_ ys _] _ /Exercise1_3a6P [xs _ sq].
  apply /Exercise1_3a6P; split => //; move: h1 => [or _ _].
  rewrite - sq in q2; order_tac.
rewrite /Ex1_2_hD /Ex1_2_hD' -Exercise1_3a3'' Exercise1_3a3'.
split => //.
  move=> x y x' => /orsum_gleP [xs ys lexy] x's.
  have r1: (Vf E13_lam x = Q x) by rewrite /E13_lam second_proj_V.
  have r2: (Vf E13_lam x' = Q x') by rewrite /E13_lam second_proj_V.
  have r3: (Vf E13_lam y = Q y) by rewrite /E13_lam second_proj_V.
  rewrite r1 r2 r3;move=> sq; case: lexy.
     rewrite sq; move=> lt; exists y;split => //; apply /orsum_gleP.
     by split => //; left.
  move=> [p1 p2]; exists x'; split => //; last by rewrite r2 - sq -p1.
  order_tac; ue.
move => x y xs ys lxy.
exists x; case: (equal_or_not (Vf E13_lam x) (Vf E13_lam y)).
  move=> h; exists x; split => //; order_tac; rewrite orsum_sr //.
move=> h; exists y; split => //; apply /orsum_gleP; split => //; red.
have <-: (Vf E13_lam x = Q x) by rewrite /E13_lam second_proj_V.
have <-: (Vf E13_lam y = Q y) by rewrite /E13_lam second_proj_V.
by left; split.
Qed.

Lemma Exercise1_3a15: E13_H1 -> E13_H2 ->
  order_isomorphism (fun_on_quotient E13_S E13_lam)
  (quotient_order E13_F E13_S) r.
Proof.
move=> h1 h2; move: (Exercise1_3a14 h1 h2) => [pa pb pc pd].
move: Exercise1_3a1 => gg.
have oo: (order (order_sum r g)) by fprops.
move; move: Exercise1_3a13 => bf.
suff : (order_morphism (fun_on_quotient E13_S E13_lam)
    (quotient_order E13_F (equivalence_associated E13_lam)) r).
  move => [p1 p2 [p3 p4 p5] p6]; split => //.
  by split => //; apply: bf.
by rewrite Exercise1_2f3; [| apply: Exercise1_3a4 =>// | apply: Exercise1_3a10 |
      apply: Exercise1_3a11].
Qed.

End Exercise1_3a.

The ordinal sum is associative, not commutative. Associativity has been proved in the main text. A example of non-commutatitivity is that omega+1 and 1+omega are non-equal. We show here that if a sum of two sets has a greatest element, then the second one has a greatest element, and give a simple example

Lemma orsum2_greatest r r' x: order r -> order r' ->
  nonempty (substrate r') ->
  greatest (order_sum2 r r') x -> greatest r' (P x).
Proof.
move=> or or' [y ysr] [xsp xgr].
move: TP_ne1 => D.
have Js: (inc (J y C1) (substrate (order_sum2 r r'))).
  by rewrite (orsum2_sr or or'); apply: candu2_prb.
move: (xgr _ Js) => /orsum2_gleP; aw.
move=> [_ p1 p2].
move: p1 => /candu2P [px]; case.
  by move=> [_ qx];case: p2; move => [p1 p3];[case: D| case: p3| case: D].
move=> [pxs qxb]; split => // x0 x0sr.
have Js': (inc (J x0 C1) (substrate (order_sum2 r r'))).
  by rewrite (orsum2_sr or or'); apply:candu2_prb.
move: (xgr _ Js') => /orsum2_gleP; aw.
move=> [q1 q2];case ; by case.
Qed.

Lemma image_of_greatest r r' f x:
  order_isomorphism f r r' -> greatest r x ->
  greatest r' (Vf f x).
Proof.
move => [or or' [sf tf bf] incf] [xs xg].
rewrite - tf in xs.
split; first by Wtac; fct_tac.
rewrite - bf;move => y ysr.
move: (bij_surj sf ysr)=> [z zsf <-].
rewrite - (incf _ _ zsf xs);apply: xg; ue.
Qed.

Lemma orsum2_nc: exists r r',
  [/\ order r, order r' & ~ ( (order_sum2 r r') \Is (order_sum2 r' r))].
Proof.
move: (diagonal_osr (singleton emptyset))=> []; set r1 := diagonal _ => or1 sr1.
move: (diagonal_osr (doubleton C0 C1))=> []; set r2 := diagonal _ => or2 sr2.
have ns2: nonempty (substrate r2).
  have jp: inc (J C0 C0) r2 by apply /diagonal_pi_P;split;fprops.
  exists C0; substr_tac.
have ng2: forall x, greatest r2 x -> False.
  move => x [_]; rewrite sr2; aw => h2.
  case: TP_ne.
  move: (h2 _ (set2_1 C0 C1)) (h2 _ (set2_2 C0 C1)).
  by move /diagonal_pi_P => [_ ->] /diagonal_pi_P [_ ->].
have g1: greatest r1 emptyset.
 red; rewrite sr1; split;fprops.
  move => x /set1_P ->; apply/diagonal_pi_P;split;fprops.
have g2: greatest (order_sum2 r2 r1) (J emptyset C1).
  move: g1 => [pa pb].
  have xx:inc (J emptyset C1) (canonical_du2 (substrate r2) (substrate r1)).
     by apply: candu2_prb.
  red; rewrite (orsum2_sr or2 or1); split; first exact.
  move => x xd; apply /orsum2_gleP; split ; [exact | exact | ].
  move/candu2P: xd => [px]; case; move => [l1 l2].
    constructor 3; aw; split;fprops.
  constructor 2; aw; rewrite l2;split;fprops.
exists r2; exists r1;split => //; move => [f isf].
move: (orsum2_greatest or1 or2 ns2 (image_of_greatest isf g2)) => eg.
by case: (ng2 (P (Vf f (J emptyset C1)))).
Qed.

Conditions under which an ordinal sum is totally ordered, directed, a lattice

Section Exercise13b.
Variables r g: Set.
Hypothesis oa: orsum_ax r g.
Definition orsum_ax2:=
 (forall i, inc i (domain g) -> nonempty (substrate (Vg g i))).

Lemma orsum_pr0: orsum_ax2 ->
  forall i, inc i (substrate r) ->
  exists2 y, inc y (Vg (fam_of_substrates g) i) &
    inc (J y i) (sum_of_substrates g).
Proof.
move=> h i idg.
move: oa => [or sr alo]; rewrite sr in idg.
move: (h _ idg) => [j js].
exists j; last by apply: disjoint_union_pi1.
rewrite /fam_of_substrates; bw.
Qed.

Lemma orsum_pr1: orsum_ax2 ->
  forall i, inc i (domain g) ->
  exists2 y, inc y (Vg (fam_of_substrates g) i) &
    inc (J y i) (substrate (order_sum r g)).
Proof.
move: (oa) => [_ sr _] h i idg; rewrite - sr in idg.
rewrite orsum_sr //; apply: (orsum_pr0 h idg).
Qed.

Lemma orsum_directed: orsum_ax2 ->
  (right_directed (order_sum r g) <-> (right_directed r /\
    forall i, maximal r i -> right_directed (Vg g i))).
Proof.
move=> alne.
move: (oa) => [or sr alo].
have os: order (order_sum r g) by fprops.
split.
  move /right_directedP; bw; move=> [oor h]; split.
    apply /right_directedP;split => //.
    move => x y xsr ysr.
    move: (orsum_pr0 alne xsr) => [x0 p1 p2].
    move: (orsum_pr0 alne ysr) => [y0 p3 p4].
    move: (h _ _ p2 p4) => [z [zs zx zy]].
    move: (orsum_gle_id oa zx) (orsum_gle_id oa zy); aw=> q1 q2.
    by exists (Q z); split => //; move:(du_index_pr1 zs); rewrite sr; case.
  move=> i [isr im].
  rewrite sr in isr.
  apply /right_directedP; split;fprops;move=> x y xsi ysi.
  move: (disjoint_union_pi1 isr xsi)(disjoint_union_pi1 isr ysi) => p1 p2.
  move: (h _ _ p1 p2) => [z [zs le1 le2]].
  move: (du_index_pr1 zs) => [p3 p4 p5].
  move: (orsum_gle_id oa le1); aw => aux; move: (im _ aux)=> Qzi.
  exists (P z); split => //; first by ue.
  move: le1 => /orsum_gleP [_ _];
    by rewrite /order_sum_r Qzi/glt pr2_pair pr1_pair; case;case.
  move: le2 => /orsum_gleP; move=> [_ _];
    by rewrite /order_sum_r Qzi/glt pr2_pair pr1_pair; case; case.
move => [] /right_directedP [_ rr] imr; apply /right_directedP; split => //; bw.
move=> x y xsr ysr.
move: (du_index_pr1 xsr) (du_index_pr1 ysr) => [Qx Px px][Qy Py py].
rewrite sr in rr; move: (rr _ _ Qx Qy) => [z [zdg Qxz Qyz]].
case: (equal_or_not (Q x) z) => eQxz.
  case: (equal_or_not (Q y) z) => eQyz.
    case: (p_or_not_p (maximal r z)) => mz.
      move: (imr _ mz).
      move /right_directedP => [oz etc].
      rewrite eQxz in Px;rewrite eQyz in Py.
      move: (etc _ _ Px Py)=> [t [ts t1 t2]].
      move: mz =>[];rewrite sr=> zs _.
      have aux:inc (J t z) (sum_of_substrates g) by apply: disjoint_union_pi1.
      exists (J t z);split => //; apply /orsum_gleP=> //;
        rewrite/order_sum_r pr1_pair pr2_pair; split=> //; right;split => //;ue.
    have [u us zu]: (exists2 u, inc u (substrate r) & glt r z u).
      ex_middle h; case: mz; split => //; first by ue.
      move=> t zt; case: (equal_or_not z t) => // nzt.
      by case: h; exists t=> //; order_tac.
    move: (orsum_pr0 alne us) => [v v1 v2]; ex_tac;
     apply /orsum_gleP=> //; rewrite /order_sum_r ?eQxz ?eQyz; aw; split;fprops.
  exists x; split => //; first by order_tac; bw.
  apply /orsum_gleP; split => //; left; rewrite eQxz; split => //.
case: (equal_or_not (Q y) z) => nQyz.
  exists y; split => //; last by order_tac; bw.
  apply /orsum_gleP; split => //;left; rewrite nQyz; split => //.
rewrite - sr in zdg.
move: (orsum_pr0 alne zdg) => [v v1 v2];ex_tac;
 apply /orsum_gleP; split => //; left; aw; order_tac.
Qed.

Lemma orsum_total1: orsum_ax2 ->
  total_order (order_sum r g) -> (total_order r /\
    forall i, inc i (domain g) -> total_order (Vg g i)).
Proof.
move=> alne; rewrite /total_order.
move: (oa) => [or sr alo]; bw;rewrite sr.
move=> [ors to]; split.
  split => // x y xdg ydg.
  move: (alne _ xdg) (alne _ ydg) => [a asx][b bsy].
  case: (to _ _ (disjoint_union_pi1 xdg asx) (disjoint_union_pi1 ydg bsy));
    move=> h; move: (orsum_gle2 h); rewrite /glt.
    move => aux;left; case: aux; move=> [res _] //; rewrite res; order_tac; ue.
  move => aux;right; case: aux; move=> [res _] //; rewrite res; order_tac; ue.
move=> i idg; move: (alo _ idg) => lo; split => //.
move=> x y xsr ysr; red.
by case: (to _ _ (disjoint_union_pi1 idg xsr) (disjoint_union_pi1 idg ysr));
 move=> h; move: (orsum_gle2 h); case; case => // _ ok; [left | right].
Qed.

Lemma orsum_total2:
  total_order r ->
  (forall i, inc i (domain g) -> total_order (Vg g i)) ->
  total_order (order_sum r g).
Proof.
move=> [_ tor] alt; rewrite /total_order.
move: (oa) => [or sr alo]; bw.
rewrite sr in tor.
split =>//; first by fprops.
move=> x y xsr ysr; move: (du_index_pr1 xsr) (du_index_pr1 ysr).
move=> [Qx Px px][Qy Py py].
case: (equal_or_not (Q x) (Q y)).
  move =>h; move: (alt _ Qx) => [lor ltor]; rewrite -h in Py.
  case: (ltor _ _ Px Py) => h1;aw ; [left | right];
    apply /orsum_gleP;split => //; right; split => //; ue.
move=> nQ; case: (tor _ _ Qx Qy) => h; [left | right];
  apply /orsum_gleP;split => //; left;split; fprops.
Qed.

Lemma orsum_g1 i x i' x':
  inc (J i x) (sum_of_substrates g) -> inc (J i' x') (sum_of_substrates g)->
  gle r x x' -> x <> x' ->
  gle (order_sum r g) (J i x) (J i' x').
Proof.
move=> js1 js2 le1 lt1.
apply /orsum_gleP; split => //; left; aw; split => //.
Qed.

Lemma orsum_lattice1: orsum_ax2 ->
  lattice (order_sum r g) -> lattice r.
Proof.
move=> alne lF.
move:(orsum_pr1 alne); set (F:= order_sum r g) => aux.
move: (oa) => [or sr alo].
have oF: (order F) by rewrite /F; fprops.
have sF: substrate F = sum_of_substrates g by rewrite /F; bw.
split => //; rewrite sr; move=> x y xsr ysr.
move: (aux _ xsr) (aux _ ysr) => [x' x'1 x'2][y' y'1 y'2].
split.
  move: (lattice_sup_pr lF y'2 x'2); rewrite -/F; move=> [le1 le2 le3].
  case: (p_or_not_p (gle r x y))=> lxy.
     exists y; apply: sup_comparable => //.
  case: (p_or_not_p (gle r y x)) => lyx.
     exists x; rewrite set2_C; apply: sup_comparable => //.
  set (z:= sup F (J y' y) (J x' x)) in *.
  move: (arg2_sr le1).
  rewrite sF => zs; move: (du_index_pr1 zs) => [Qz Pz pz]; exists (Q z).
  apply: lub_set2 => //.
      move: (orsum_gle_id oa le2); aw.
    move: (orsum_gle_id oa le1); aw.
  move=> t xt yt.
  move: (arg2_sr xt); rewrite sr; move=> tg.
  move: (aux _ tg) => [u uVg us].
  rewrite sF in x'2 y'2 us.
  have le4: (gle F (J x' x) (J u t)) by apply: orsum_g1 => //; dneg aa; ue.
  have le5: (gle F (J y' y) (J u t)).
   apply: orsum_g1 => //; move=> eyt; case: lxy; ue.
  move: (le3 _ le5 le4) => le6; move: (orsum_gle_id oa le6); aw.
move: (lattice_inf_pr lF y'2 x'2); rewrite -/F; move=> [le1 le2 le3].
case: (p_or_not_p (gle r x y))=> lxy.
  exists x; apply: inf_comparable => //.
case: (p_or_not_p (gle r y x)) => lyx.
   exists y; rewrite set2_C; apply: inf_comparable => //.
set (z:= inf F (J y' y) (J x' x)) in *.
move: (arg1_sr le1).
rewrite sF => zs; move: (du_index_pr1 zs) => [Qz Pz pz]; exists (Q z).
apply: glb_set2 => //.
      move: (orsum_gle_id oa le2); aw.
    move: (orsum_gle_id oa le1); aw.
move=> t xt yt.
move: (arg1_sr xt); rewrite sr; move=> tg.
move: (aux _ tg) => [u uVg us].
rewrite sF in x'2 y'2 us.
have le4: (gle F (J u t) (J x' x)).
  apply: orsum_g1 => //; move=> eyt; case: lxy; ue.
have le5: (gle F (J u t) (J y' y)).
  apply: orsum_g1 => //; move=> ext; case: lyx; ue.
move: (le3 _ le5 le4) => le6; move: (orsum_gle_id oa le6); aw.
Qed.

Let orsum_lattice_H1:= forall i j, inc i (domain g) -> inc j (domain g) ->
    [\/ gle r i j, gle r j i | (exists u v,
      least (Vg g (sup r i j)) u /\
      greatest (Vg g (inf r i j)) v)].

Let orsum_lattice_H2 := forall i x y t,
  inc i (domain g) -> gle (Vg g i) x t -> gle (Vg g i) y t ->
    has_supremum (Vg g i) (doubleton x y).
Let orsum_lattice_H3 := forall i x y t,
  inc i (domain g) -> gle (Vg g i) t x -> gle (Vg g i) t y ->
    has_infimum (Vg g i) (doubleton x y).
Let orsum_lattice_H4 := forall i x y,
  inc i (domain g) -> inc x (Vg (fam_of_substrates g) i)
    -> inc y (Vg (fam_of_substrates g) i) ->
  (forall t, inc t (Vg (fam_of_substrates g) i)
     -> ~ (gle (Vg g i) x t /\ gle (Vg g i) y t)) ->
  exists j, [/\ inc j (domain g),
    least (induced_order r (Zo (domain g) (fun k=> glt r i k))) j &
    exists z, least (Vg g j) z].
Let orsum_lattice_H5 := forall i x y,
  inc i (domain g) -> inc x (Vg (fam_of_substrates g) i)
    -> inc y (Vg (fam_of_substrates g) i) ->
  (forall t, inc t (Vg (fam_of_substrates g) i)
     -> ~ (gle (Vg g i) t x /\ gle (Vg g i) t y)) ->
  exists j, [/\ inc j (domain g),
    greatest (induced_order r (Zo (domain g) (fun k=> glt r k i))) j &
    exists z, greatest (Vg g j) z].

Lemma orsum_lattice2: orsum_ax2 ->
  lattice (order_sum r g) -> orsum_lattice_H1.
Proof.
move=> alne los i j idg jdg.
move: (orsum_lattice1 alne los)=> lr.
move:(orsum_pr1 alne); set (F:= order_sum r g) => aux.
have oF:order F by rewrite /F; fprops.
move: (oa) => [or sr alo].
have sF: substrate F = sum_of_substrates g by rewrite /F; bw.
case: (p_or_not_p (gle r i j)); first by in_TP4.
case: (p_or_not_p (gle r j i)); first by in_TP4.
move=> nji nij; constructor 3.
move: (aux _ idg) (aux _ jdg) => [u uVg Ju][v vVg Jv].
move: (lattice_sup_pr los Ju Jv) (lattice_inf_pr los Ju Jv).
rewrite -/F.
set (A:= inf F (J u i) (J v j)); set (a:= inf r i j).
set (B:= sup F (J u i) (J v j)); set (b:= sup r i j).
move=> [p1 p2 p3][p4 p5 p6].
rewrite - sr in idg jdg.
rewrite sF in Ju Jv.
move: (lattice_inf_pr lr idg jdg) (lattice_sup_pr lr idg jdg).
rewrite -/a -/b; move=> [q1 q2 q3][q4 q5 q6].
have Hc: Q A = a.
  have s1: (gle r (Q A) a).
    move: (orsum_gle_id oa p4); aw => s1.
    move: (orsum_gle_id oa p5); aw => s2.
    apply: (q3 _ s1 s2).
  move: (arg1_sr q1); rewrite sr => asr.
  move: (aux _ asr) => [y yVg Js].
  rewrite sF in Js.
  have s2 : (gle F (J y a) (J u i)).
    apply: orsum_g1 => //; move=> eai; rewrite -eai in nij; contradiction.
  have s3: (gle F (J y a) (J v j)).
  apply: orsum_g1 => //; move=> eai; rewrite -eai in nji; contradiction.
  move: (p6 _ s2 s3) => s4;move: (orsum_gle_id oa s4); aw => s5.
  order_tac.
have Hd: Q B = b.
  have s1: (gle r b (Q B)).
    move: (orsum_gle_id oa p1); aw => s1.
    move: (orsum_gle_id oa p2); aw => s2.
    apply: (q6 _ s1 s2).
  move: (arg2_sr q4); rewrite sr => asr.
  move: (aux _ asr) => [y yVg Js].
  rewrite sF in Js.
  have s2 : (gle F (J u i) (J y b)).
    apply: orsum_g1 => //; move=> eai; rewrite eai in nji; contradiction.
  have s3: (gle F (J v j) (J y b)).
    apply: orsum_g1 => //; move=> eai; rewrite eai in nij; contradiction.
  move: (p3 _ s2 s3) => s4;move: (orsum_gle_id oa s4); aw => s5.
  order_tac.
move: (arg2_sr p2); rewrite sF => Bs.
move: (du_index_pr1 Bs) => [QB PB pB]; rewrite Hd in PB.
move: (arg1_sr p5); rewrite sF => As.
move: (du_index_pr1 As) => [QA PA pA]; rewrite Hc in PA.
exists (P B); exists (P A).
rewrite /least /greatest; split; split => //.
  move=> x xs.
  have J1s: (inc (J x b) (sum_of_substrates g)).
    apply: disjoint_union_pi1=> //; ue.
  have s1: (gle F (J u i) (J x b)).
    apply: orsum_g1 => //;move=> ib; case: nji; ue.
  have s2: (gle F (J v j) (J x b)).
    apply: orsum_g1 => //; move=> ib; case: nij; ue.
  move: (p3 _ s1 s2) => /orsum_gleP [s3 s4].
   case; aw; [ by move => [_ ];rewrite Hd; case | by move => [->] ].
move=> x xs.
have J1s: (inc (J x a) (sum_of_substrates g)).
apply: disjoint_union_pi1=> //; ue.
have s1: (gle F (J x a) (J u i)).
  apply: orsum_g1 => //; move=> ib; case: nij; ue.
have s2: (gle F (J x a) (J v j)).
  apply: orsum_g1 => //;move=> ib; case: nji; ue.
move: (p6 _ s1 s2) => /orsum_gleP [s3 s4].
case; aw; [ by move => [_ ];rewrite Hc; case | by move => [->] ].
Qed.

Lemma orsum_lattice3:
  lattice (order_sum r g) -> orsum_lattice_H2.
Proof.
move=> lo i x y t idg le1 le2.
set (F:= order_sum r g).
have oF:order F by rewrite /F; fprops.
move: (oa) => [or sr alo].
have sF: substrate F = sum_of_substrates g by rewrite /F; bw.
move: (arg1_sr le1)(arg2_sr le1) (arg1_sr le2).
move=> xs ts ys.
move: (disjoint_union_pi1 idg xs)(disjoint_union_pi1 idg ys).
move: (disjoint_union_pi1 idg ts); rewrite - sF => Jts Jxs Jys.
move: (lattice_sup_pr lo Jxs Jys) => [ple1 ple2 ple3].
have le4: (gle F (J y i) (J t i))
   by apply /orsum_gleP;split => //; try ue; right;split => //; aw.
have le5: (gle F (J x i) (J t i))
   by apply /orsum_gleP;split => //; try ue; right;split => //; aw.
move: (ple3 _ le5 le4) => le6.
set (z:= sup (order_sum r g) (J x i) (J y i)) in *.
move: (orsum_gle_id oa ple1); aw => le7.
move: (orsum_gle_id oa le6); aw => le8.
move: (order_antisymmetry or le7 le8) => eq1.
exists (P z).
apply: lub_set2; first by apply: alo => //.
  move: ple1 =>/orsum_gleP [_ _]; case; first by move => [_]; aw;case.
    by aw; move => [->].
  move: ple2 =>/orsum_gleP [_ _]; case; first by move => [_]; aw;case.
    by aw; move => [->].
move=> u xu yu.
move: (disjoint_union_pi1 idg (arg2_sr xu)) => Jus.
rewrite - sF in Jus.
have le9: (gle F (J x i) (J u i))
   by apply /orsum_gleP;split => //; [ue|ue| right;split => //; aw].
have le10: (gle F (J y i) (J u i))
   by apply/orsum_gleP;split => //; [ue|ue| right;split => //; aw].
move: (ple3 _ le9 le10).
move /orsum_gleP => [_ _]; case;aw; first by move => [_]; case; rewrite eq1.
by move => [->].
Qed.

Lemma orsum_lattice4:
  lattice (order_sum r g) -> orsum_lattice_H3.
Proof.
move=> lo i x y t idg le1 le2.
set (F:= order_sum r g).
have oF:order F by rewrite /F; fprops.
move: (oa) => [or sr alo].
have sF: substrate F = sum_of_substrates g by rewrite /F; bw.
move: (arg2_sr le1)(arg1_sr le1) (arg2_sr le2).
move=> xs ts ys.
move: (disjoint_union_pi1 idg xs)(disjoint_union_pi1 idg ys).
move: (disjoint_union_pi1 idg ts); rewrite - sF => Jts Jxs Jys.
move: (lattice_inf_pr lo Jxs Jys) => [ple1 ple2 ple3].
have le4: (gle F (J t i) (J y i))
   by apply /orsum_gleP;split => //; try ue; right;split => //; aw.
have le5: (gle F (J t i) (J x i))
   by apply /orsum_gleP;split => //; try ue; right;split => //; aw.
move: (ple3 _ le5 le4) => le6.
set (z:= inf (order_sum r g) (J x i) (J y i)) in *.
move: (orsum_gle_id oa ple1); aw => le7.
move: (orsum_gle_id oa le6); aw => le8.
move: (order_antisymmetry or le7 le8) => eq1.
exists (P z).
apply: glb_set2; first by apply: alo.
  move: ple1 =>/orsum_gleP [_ _]; case; first by move => [_]; aw;case.
    by aw; move => [->].
  move: ple2 =>/orsum_gleP [_ _]; case; first by move => [_]; aw;case.
    by aw; move => [->].
move=> u xu yu.
move: (disjoint_union_pi1 idg (arg1_sr xu)) => Jus.
rewrite - sF in Jus.
have le9: (gle F (J u i) (J x i))
  by apply /orsum_gleP;split => //; [ue|ue| right;split => //; aw].
have le10: (gle F (J u i) (J y i))
    by apply/orsum_gleP;split => //; [ue|ue| right;split => //; aw].
move: (ple3 _ le9 le10).
move /orsum_gleP => [_ _]; case;aw; first by move => [_]; case; rewrite eq1.
by move => [->].
Qed.

Lemma orsum_lattice5:
  orsum_ax2 -> lattice (order_sum r g) -> orsum_lattice_H4.
Proof.
move=> alne los i x y idg xVs yVs alt.
move: (orsum_lattice1 alne los)=> lr.
set (F:= order_sum r g).
have aux:forall i, inc i (domain g) -> exists2 y,
    inc y (Vg (fam_of_substrates g) i) &
    inc (J y i) (substrate F) by apply: orsum_pr1.
have oF:order F by rewrite /F; fprops.
move: (oa) => [or sr alo].
have sF: substrate F = sum_of_substrates g by rewrite /F; bw.
move: xVs yVs;rewrite /fam_of_substrates; bw => xVs yVs.
move: (disjoint_union_pi1 idg xVs) (disjoint_union_pi1 idg yVs) => l1 l2.
rewrite - sF in l1 l2.
move: (lattice_sup_pr los l1 l2).
set (Z:=sup (order_sum r g) (J x i) (J y i)).
move=> [] /orsum_gleP [_ zs l3] /orsum_gleP [_ _ l4] l5.
move: (du_index_pr1 zs) => [QZ PZ pz].
have l6: (glt r i (Q Z)).
  move: l3; case; aw; move: l4; case; aw; move=> [iQ l3] [_ l4].
  move:(alt (P Z)); rewrite /fam_of_substrates; bw.
  rewrite {1} iQ;move=> h; case: (h PZ); split => //.
have sZ: (sub (Zo (domain g) (fun k => glt r i k)) (substrate r)).
  rewrite sr; apply: Zo_S.
have z1: inc (Q Z) (Zo (domain g) (fun k => glt r i k)) by apply: Zo_i.
exists (Q Z); split => //.
  red; aw;split => //; move => u /Zo_P [udg iu]; apply /iorder_gleP => //.
    by apply: Zo_i.
  move:(aux _ udg) => [v vVg Js].
  have l7: (gle F (J x i) (J v u))
    by apply /orsum_gleP;split => //; try ue; left; aw.
  have l8: (gle F (J y i) (J v u))
    by apply /orsum_gleP;split => //; try ue; left; aw.
  move: (l5 _ l7 l8) => l9; move: (orsum_gle_id oa l9); aw.
exists (P Z);split => //.
move=> u us.
move:(disjoint_union_pi1 QZ us) => Js.
have l7: (gle F (J x i) (J u (Q Z)))
  by apply /orsum_gleP;split => //; try ue; left; aw.
have l8: (gle F (J y i) (J u (Q Z)))
  by apply /orsum_gleP;split => //; try ue; left; aw.
by move: (l5 _ l7 l8) => /orsum_gleP [r1 r2];case =>[] []; aw => _; case.
Qed.

Lemma orsum_lattice6: orsum_ax2 ->
  lattice (order_sum r g) -> orsum_lattice_H5.
Proof.
move=> alne los i x y idg xVs yVs alt.
move: (orsum_lattice1 alne los)=> lr.
set (F:= order_sum r g).
have aux:forall i, inc i (domain g) -> exists2 y,
    inc y (Vg (fam_of_substrates g) i) &
    inc (J y i) (substrate F) by apply: orsum_pr1.
have oF:order F by rewrite /F; fprops.
move: (oa) => [or sr alo].
have sF: substrate F = sum_of_substrates g by rewrite /F; bw.
move: xVs yVs;rewrite /fam_of_substrates; bw => xVs yVs.
move: (disjoint_union_pi1 idg xVs) (disjoint_union_pi1 idg yVs) => l1 l2.
rewrite - sF in l1 l2.
move: (lattice_inf_pr los l1 l2).
set (Z:=inf (order_sum r g) (J x i) (J y i)).
move => []/orsum_gleP [zs _ l3 ] /orsum_gleP [_ _ l4] l5.
move: (du_index_pr1 zs) => [QZ PZ pz].
have l6: (glt r (Q Z) i).
  move: l3; case; aw; move: l4; case; aw; move=> [iQ l3] [_ l4].
  move:(alt (P Z)); rewrite /fam_of_substrates; bw.
  rewrite - iQ;move=> h; case: (h PZ); split => //.
have sZ: (sub (Zo (domain g) (fun k => glt r k i)) (substrate r)).
  rewrite sr; apply: Zo_S.
have z1: inc (Q Z) (Zo (domain g) (fun k => glt r k i)) by apply Zo_i.
exists (Q Z); split => //.
  red; aw; split => //; move => u /Zo_P [udg iu].
  apply /iorder_gleP => //; first by apply: Zo_i.
  move:(aux _ udg) => [v vVg Js].
  have l7: (gle F (J v u) (J x i))
    by apply /orsum_gleP;split => //; try ue; left; aw.
  have l8: (gle F (J v u) (J y i))
    by apply /orsum_gleP;split => //; try ue; left; aw.
  move: (l5 _ l7 l8) => l9; move: (orsum_gle_id oa l9); aw.
exists (P Z);split => //.
move=> u us.
move:(disjoint_union_pi1 QZ us) => Js.
have l7: (gle F (J u (Q Z)) (J x i))
   by apply /orsum_gleP;split => //; try ue; left; aw.
have l8: (gle F (J u (Q Z)) (J y i))
   by apply /orsum_gleP;split => //; try ue; left; aw.
by move: (l5 _ l7 l8); move /orsum_gleP => [r1 r2];case =>[] []; aw => _; case.
Qed.

Lemma orsum_lattice: orsum_ax2 ->
  (lattice (order_sum r g) <->
  ((lattice r) /\
   [/\ orsum_lattice_H1, orsum_lattice_H2, orsum_lattice_H3, orsum_lattice_H4
    & orsum_lattice_H5])).
Proof.
move=> alne.
set (F:= order_sum r g).
have oF:order F by rewrite /F; fprops.
move: (oa) => [or sr alo].
split.
  move=> h; split; last split.
  apply: (orsum_lattice1 alne h).
  apply: (orsum_lattice2 alne h).
  apply: (orsum_lattice3 h).
  apply: (orsum_lattice4 h).
  apply: (orsum_lattice5 alne h).
  apply: (orsum_lattice6 alne h).
move=> [h1 [h2 h3 h4 h5 h6]].
have sF: substrate F = sum_of_substrates g by rewrite /F; bw.
split=>//.
rewrite sF;move=> x y xs ys.
move: (du_index_pr1 xs) (du_index_pr1 ys) => [Qx Px px][Qy Py py].
rewrite - sr in Qx Qy.
split.
  move: (lattice_sup_pr h1 Qx Qy); set (a:= sup