Library ssete4

Theory of Sets : Exercises sections 4

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

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

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

Module Exercise4.

Exercise 4.1. is in file ssete3
Exercise 4.2. A set is finite iff every non-empty subset of the powerset has a maximal element (with respect to inclusion).

Definition meet A B := nonempty (A \cap B).

Lemma finite_is_maximal_inclusion x:
  finite_set x <->
  (forall y, sub y (powerset x) -> nonempty y -> exists2 z,
     inc z y & forall t, inc t y -> sub z t -> z = t).
Proof.
split.
  move: x; apply: finite_set_induction0.
    move=> y yp0 [t ty].
    have yp1: forall v, inc v y -> v = emptyset.
      by move=> v vy; move: (yp0 _ vy); rewrite setP_0 => /set1_P.
    by ex_tac => v vy tv; rewrite (yp1 _ ty) (yp1 _ vy).
  move=> a b hrec nba y yp yne.
  set Z:= Zo y (fun z => inc b z); case: (emptyset_dichot Z) => ze.
    have yp1: sub y (powerset a).
      move => t ty; move: (yp _ ty) => /setP_P ta; apply /setP_P => u ut.
      move: (ta _ ut); case /setU1_P => // ub;empty_tac1 t;apply: Zo_i =>//; ue.
    by apply: hrec.
    set T:= fun_image Z (intersection2 a).
    have Tp: sub T (powerset a).
      move => t /funI_P [z zZ ->]; apply /setP_P;apply: subsetI2l.
    have neT:nonempty T.
      move: ze => [z zZ]; exists (a \cap z); apply /funI_P; ex_tac.
  move: (hrec _ Tp neT)=> [z zT zm].
  move: zT => /funI_P[u uZ iau].
  move: uZ => /Zo_P [uy bu].
  ex_tac; move=> t ty ut.
  have bt: inc b t by apply: ut.
  have tz: inc t Z by apply: Zo_i => //.
  have it: inc (a \cap t) T by apply /funI_P; ex_tac.
  have it1: sub z (a \cap t).
    rewrite iau => w /setI2_P [p1 p2]; apply /setI2_P;split;fprops.
  move: (zm _ it it1) => zi.
  apply: extensionality => // v vt; move: (yp _ ty).
    move /setP_P => tt;move:(tt _ vt); case /setU1_P; last by move => ->.
  by move => va;apply: (@setI2_2 a);rewrite- iau zi; apply:setI2_i.
move=> h.
set F := (finite_subsets x).
have p1:sub F (powerset x) by apply: Zo_S.
have p2: nonempty F.
  exists emptyset; apply:Zo_i; [ apply: setP_0i| apply:emptyset_finite].
move: (h _ p1 p2) => [z /Zo_P [] /setP_P zpo zf zp].
case: (emptyset_dichot (x -s z)) => ce.
  have -> //: x = z by apply:extensionality => //; apply:empty_setC.
move: ce => [y] /setC_P [yx nyz].
set (t:= z +s1 y).
have tF: inc t F.
  by apply:Zo_i; [apply /setP_P; apply: setU1_sub | apply:setU1_finite].
have zt: sub z t by move=> u uz; rewrite /t; fprops.
move: (zp _ tF zt) => tz; case: nyz; rewrite tz /t; fprops.
Qed.


Exercise 4.3 is in file ssete3
Exercise 4.4. Assume that C is a subset of E x E that contains a pair (x , y) if and only if it does not contain (y, x). We can re-order the elements of E as (x(1), x(2), ..., x(n)) so that (x(i),x(i+1)) is in C.

Lemma Exercise4_4 n E C:
  inc n Bnat -> cardinal E = n -> sub C (coarse E) ->
  (forall x y, inc x E -> inc y E -> x <> y ->
    (exactly_one (inc (J x y) C) (inc (J y x) C))) ->
    exists2 f, bijection_prop f (Bintcc \1c n) E &
      (forall i, \1c <=c i -> i <c n ->
        inc (J (Vf f i) (Vf f (succ i))) C).
Proof.
move=> nB cn _; move: n nB E cn C.
have auxP: forall n, inc n Bnat -> forall x,
   (inc x (Bintcc \1c n) <-> (x <> \0c /\ x <=c n)).
  have ob: inc \1c Bnat by fprops.
  move=> n nB x; move:(Bint_pr5 nB) => [pa pb]; split.
     move => pc; split; first by dneg pd; rewrite -pd.
     apply /(BintcP nB); rewrite -pa; fprops.
  move => [pc] /(BintcP nB); rewrite - pa; case /setU1_P => //.
apply: cardinal_c_induction1.
move=> n nB hrec E nE C cp.
case: (emptyset_dichot E) => Ee.
  rewrite -nE Ee cardinal_set0.
  have ->: (Bintcc \1c \0c) = emptyset.
    apply /set0_P => t /(auxP _ BS0) [pa pb].
    case: (card_lt0 (conj pb pa)).
  move: (empty_function_tg_function emptyset).
  set f := empty_function_tg _; move => ww;exists f => //.
    move: ww => [pa pb pc]; split => //.
      split => //; split => //.
      by move => a b; rewrite pb => /in_set0.
      by move => ay; rewrite pc => /in_set0.
  by move => i _ i1; move: (card_lt0 i1).
move: Ee => [a aE].
set E1 := E -s1 a.
have s1:sub (singleton a) E by apply: set1_sub.
set Z1:= Zo E1 (fun z => inc (J z a) C).
set Z2:= Zo E1 (fun z => inc (J a z) C).
have Z1E1: sub Z1 E1 by apply: Zo_S.
have sE1E: sub E1 E by apply: sub_setC.
have Z1E: sub Z1 E by apply: sub_trans sE1E.
have Z2E: sub Z2 E by apply: sub_trans sE1E=>//; apply: Zo_S.
have Z2c: Z2 = E1 -s Z1.
  set_extens t.
    move /Zo_P => [ta tb]; apply /setC_P; split => //; move /Zo_P => [_ tc].
    move /setC_P: ta => [te ] /set1_P tna.
    by move: (cp _ _ te aE tna) => [_]; apply.
  move => /setC_P [te h]; apply /Zo_P;split => //.
  move /setC_P: (te) => [te1 ] /set1_P tna.
  move: (cp _ _ te1 aE tna) => [pa pb]; case: pa => // pc.
  case: h; apply :Zo_i => //.
move: (cardinal_setC s1); rewrite /card_diff cardinal_set1 -/E1.
move: (cardinal_setC Z1E1); rewrite /card_diff -Z2c nE; move => <-.
set n1:= cardinal Z1; set n2:= cardinal Z2; move => rel1.
have fe: finite_set E by red; apply /BnatP; ue.
have n1B: inc n1 Bnat by apply /BnatP; apply: (sub_finite_set Z1E fe).
have n2B: inc n2 Bnat by apply /BnatP; apply: (sub_finite_set Z2E fe).
clear fe.
have aux2: (n1 +c n2) <c n.
  have c1: cardinalp (n1 +c n2) by fprops.
  rewrite -rel1;rewrite (csumC \1c _) - card_succ_pr4 //.
  apply: card_lt_succ; fprops.
have aux3: n1 <=c (n1 +c n2) by apply: csum_M0le; fprops.
have aux4: n2 <=c (n1 +c n2) by rewrite csumC;apply: csum_M0le; fprops.
have ltn1n: n1 <c n by co_tac.
have ltn2n: n2 <c n by co_tac.
clear aux2 aux3 aux4.
have c1p: (forall x y, inc x Z1 -> inc y Z1 -> x <> y ->
  exactly_one (inc (J x y) C) (inc (J y x) C)).
   move=> x y xz1 yz1 xy; apply: (cp _ _ (Z1E _ xz1)(Z1E _ yz1) xy).
have c2p: (forall x y, inc x Z2 -> inc y Z2 -> x <> y ->
    exactly_one (inc (J x y) C) (inc (J y x) C)).
 by move=> x y xz1 yz1 xy; apply: (cp _ _ (Z2E _ xz1)(Z2E _ yz1)).
move: (hrec n2 nB n2B ltn2n Z2 (refl_equal (cardinal Z2)) C c2p).
move: (hrec n1 nB n1B ltn1n Z1 (refl_equal (cardinal Z1)) C c1p).
clear c1p c2p hrec.
move => [f1 [bf1 sf1 tf1] f1p][f2 [bf2 sf2 tf2] f2p].
pose f i := Yo (i = (succ n1)) a
 (Yo (i <=c n1) (Vf f1 i) (Vf f2 (i -c (succ n1)))).
move: (card_lt_succ n1B) => lt1.
have p1: f (succ n1) = a by rewrite /f; Ytac0.
have p2: forall i, i <=c n1 -> f i = Vf f1 i.
  move=> i lei.
  have in1:(i <> succ n1) by move=> h; rewrite -h in lt1;co_tac.
   by rewrite /f; Ytac0; Ytac0.
have p3: forall i, (succ n1) <c i -> f i = Vf f2 (i -c (succ n1)).
  move=> i [lesi nsi]; rewrite /f; Ytac0; Ytac in1 => //.
  have bad: (succ n1) <=c n1 by co_tac.
  co_tac.
have p4: forall i : Set, i <> \0c -> i <=c n1 -> inc (f i) Z1.
  move=> i inz in1; rewrite (p2 _ in1);rewrite -tf1; Wtac; try fct_tac.
  by rewrite sf1; apply /(auxP _ n1B).
move: (BS_succ n1B) => snB.
have nn12: n = ((succ n1) +c n2).
  rewrite csumC csum_via_succ // csumC card_succ_pr4; fprops.
  by rewrite csumC rel1.
have p5: forall i, (succ n1) <c i -> i <=c n ->
   inc (i -c (succ n1)) (source f2).
  move=> i [n1i ni3] n2i; rewrite sf2 ; apply /(auxP _ n2B).
  move: (cdiff_pr0 (BS_le_int n2i nB) snB n1i).
  set d := _ -c _ ; move=> [sB sv]; split.
    dneg dz; rewrite - sv dz; aw;co_tac.
  apply: (csum_le_simplifiable snB) => //; rewrite sv -nn12//.
have p6: forall i, (succ n1) <c i -> i <=c n ->
   inc (f i) Z2.
  move=> i in1 lin; rewrite (p3 _ in1) -tf2; Wtac; try fct_tac.
set sf3 :=(Bintcc \1c n).
have ta: forall i, inc i sf3 -> inc (f i) E.
  move=> i /(auxP _ nB) [inz lein].
  have ci: cardinalp i by co_tac.
  have cn: cardinalp (succ n1) by fprops.
  case: (card_le_to_el ci cn)=> aux1; last by apply: Z2E;apply: p6.
  case: (equal_or_not i (succ n1)) => is1; first by rewrite is1 p1.
  have : i <c (succ n1) by split.
   by move /(card_lt_succ_leP n1B); move => lin1; apply: Z1E; apply: p4.
set F := Lf f sf3 E.
have sF: source F = sf3 by rewrite /F; aw.
have tF: target F = E by rewrite /F; aw.
have fF: function F by apply: lf_function.
have fpF: function_prop F sf3 E by [].
have surjF: surjection F.
  apply: lf_surjective => // y yE.
  case: (equal_or_not y a).
    move=> ->; exists (succ n1) => //; apply /(auxP _ nB); split.
      apply: succ_nz.
    by apply /card_le_succ_ltP.
  move=> ya; move: (cp _ _ yE aE ya) => [p7 _]; case: p7 => pc.
    have yz1: inc y Z1 by apply: Zo_i => //; apply /setC1_P;split => //.
    move: yz1; rewrite -tf1 => yt1.
    move: bf1 => [_ srf1]; move: ((proj2 srf1) _ yt1) => [x xf1 <-].
    move: xf1; rewrite sf1; move /(auxP _ n1B)=> [xnz xn1].
    exists x; last by rewrite p2.
     apply /(auxP _ nB);split => //; move: ltn1n => [len1n _]; co_tac.
  have yz2: inc y Z2 by apply: Zo_i => //; apply/ setC1_P.
  move: yz2; rewrite -tf2 => yt2.
  move: bf2 => [_ srf2]; move: ((proj2 srf2) _ yt2) => [x xf2 <-].
  move: xf2; rewrite sf2; move /(auxP _ n2B) => [xnz xn2].
  move: (BS_le_int xn2 n2B) => xB.
  move: (cdiff_pr1 xB snB).
  set x1:= x +c (succ n1) => x1n1.
  have x1p: (succ n1) <c x1.
    have ->: (succ n1) = \0c +c (succ n1) by aw; fprops.
    rewrite /x1; apply: csum_Mlteq => //; fprops.
    by apply /strict_pos_P => //; apply:nesym.
  exists x1; last by rewrite (p3 _ x1p) x1n1.
  apply /(auxP _ nB); split.
    move=> h; rewrite h in x1p; apply: (card_lt0 x1p).
    rewrite /x1 nn12 csumC;apply: csum_Mlele => //; fprops.
exists F => //.
  split => //.
  apply: bijective_if_same_finite_c_surj => //.
    by rewrite /F lf_source lf_target /sf3 nE card_Bint1c.
    by rewrite /F lf_source /sf3 /finite_set (card_Bint1c nB); apply /BnatP.
move=> i i1 iN.
have inz: i <> \0c by move /card_ge1P: i1 => [_ /nesym].
move: (iN) => [lein _ ]; move: (BS_le_int lein nB) => iB.
have i3: inc i sf3 by apply /(auxP _ nB).
have si3: inc (succ i) sf3.
  by apply /(auxP _ nB); split; [ apply: succ_nz | apply /card_le_succ_ltP].
rewrite /F lf_V // lf_V //.
have ci: cardinalp i by co_tac.
have cn: cardinalp (succ n1) by fprops.
case: (card_le_to_el ci cn) => aux1.
  case: (equal_or_not i (succ n1)) => in1.
    have ltss: (succ n1) <c (succ (succ n1)) by apply: card_lt_succ.
    rewrite in1 p1 p3 //.
    have ->: (succ (succ n1)) -c (succ n1) = \1c.
      rewrite (card_succ_pr4 cn) csumC; apply: cdiff_pr1; fprops.
    have: inc (Vf f2 \1c ) Z2.
      Wtac ; first by fct_tac.
      rewrite sf2; apply /(auxP _ n2B);split;fprops; apply:card_ge1; fprops.
      move=> n2z; move: nn12; rewrite n2z; aw; rewrite -in1.
      by move: iN => [_ din] ein; case: din.
    by move => /Zo_hi.
  have lein1: i <=c n1 by apply /(card_lt_succ_leP n1B); split.
  case: (equal_or_not i n1) => eqin1.
    have n11: n1 <=c n1 by fprops.
    rewrite eqin1 p1 p2 //.
    have: (inc (Vf f1 n1) Z1).
      Wtac; first by fct_tac.
      rewrite sf1; apply /(auxP _ n1B); split => //;ue.
    by move /Zo_hi.
  have sin1: (succ i) <=c n1 by apply /card_le_succ_ltP.
  rewrite p2 // p2 //; apply: f1p => //.
have p7: (succ n1) <c (succ i).
  move: (card_le_succ iB) => aux3; co_tac.
rewrite p3 // p3 //.
move: (aux1) => [aux2 _].
move: (cdiff_pr0 iB snB aux2).
set k:= i -c (succ n1); move => [kB kp].
have ->: (succ i) -c (succ n1) = succ k.
  rewrite - csucc_diff // cdiff_pr6//.
apply: f2p.
  apply: card_ge1; fprops.
  by move=> kz; move:kp aux1; rewrite kz; aw; move=> ->; by case.
by apply: (csum_lt_simplifiable snB) => //;rewrite kp -nn12.
Qed.


Exercise 4.5. Let E be an ordered set, k the maximal number of elements in a free subset. Then E can be partitioned into k totally ordered subsets.
Definitions: Hw(k) says that any free subset has at most k elements, H(k) says moreover that there is a free subset with k elements. Cw(k) says that there exists at most k totally ordered, mutually disjoint sets whose union is E, C(k) says that this number is exactly k, and the sets are non-empty. The claim is H(k) implies C(k). We can restate it as Hw(k) implies Cw(k). Note that if we have a free subset with k elements, each element of the partition contains at most one element of the free subset, so that if Cw(k) holds, there are k sets, none of them is empty.
Lemma: a finite non-empty set has a minimal element.
Assume T is a subset of a set partitioned by Y, both sets have the same finite number of elements; assume that the intersection of T and each Yi is empty or a singleton. Then it is never empty.

Lemma finite_set_minimal r:
  order r ->finite_set (substrate r) -> nonempty (substrate r) ->
  exists x, minimal r x.
Proof.
move => or.
move: (opp_osr or) => [or' sr'].
rewrite - sr' => fsr nes.
move: (finite_set_maximal or' fsr nes) => [x xf]; exists x.
by apply /maximal_opp.
Qed.

Definition Exercise4_5_hyp r k :=
  (exists2 x, inc x (free_subsets r) & cardinal x = k) /\
  (forall x, inc x (free_subsets r) -> (cardinal x) <=c k).
Definition Exercise4_5_conc r k :=
  exists X, [/\ partition_s X (substrate r), cardinal X = k &
    forall x, inc x X -> total_order (induced_order r x)].

Lemma Exercise4_5a Y T k:
  cardinal Y = k -> cardinal T = k -> inc k Bnat ->
  sub T (union Y) ->
  (forall a b : Set, inc a Y -> inc b Y -> a = b \/ disjoint a b) ->
  (forall Z, inc Z Y -> small_set (T \cap Z)) ->
  (forall Z, inc Z Y -> singletonp (T \cap Z)).
Proof.
move => cY cT kB Tu ald als.
set V1 := Zo Y (fun z => (T \cap z) <> emptyset).
set V2 := Lg V1 (fun z => (T \cap z)).
move=> Z ZY; case: (small_set_pr (als _ ZY)) => //.
move=> itz.
have s1: sub V1 Y by apply: Zo_S.
have fsy: finite_set Y by apply /BnatP; rewrite cY.
have xy: V1 <> Y.
    move=> TZ; move: ZY;rewrite -TZ; move /Zo_P => [_ bad]; contradiction.
move: (strict_sub_smaller (conj s1 xy) fsy) => [_ bad] {itz s1 xy fsy ZY}.
case: bad.
have v1p: forall x, inc x V1 -> cardinal (Vg V2 x) = \1c.
  move=> x xV1; rewrite /V2; bw.
  move: xV1 => /Zo_P [zY ine].
  case: (small_set_pr (als _ zY));first by move=> aux; contradiction.
  by move=> [y] ->; rewrite cardinal_set1.
move: (csum_of_ones V1); rewrite /card_sum.
rewrite /disjointU.
set duf:= disjointU_fam _ ;set D:= unionb _.
move: (cardinal_pr D); move=> pa pb.
rewrite cY - cT; apply /card_eqP.
eqtrans D; first by move: pb; move /card_eqP; eqsym.
clear pa pb.
have pa: fgraph duf by rewrite /duf/disjointU_fam; fprops.
have pb:fgraph V2 by rewrite /V2; fprops.
have pc: domain duf = domain V2 .
  rewrite /duf/disjointU_fam/V2/cst_graph; bw.
have pd: (forall i, inc i (domain duf) -> equipotent (Vg duf i) (Vg V2 i)).
  rewrite /duf/disjointU_fam/V2/cst_graph; bw.
  move=> i iV1; bw; eqtrans \1c; first by eqsym; fprops.
  apply /card_eqP; rewrite -(v1p _ iV1) double_cardinal /V2; bw.
have pe: mutually_disjoint duf.
  apply: disjointU_disjoint; rewrite /cst_graph; fprops.
have pf: mutually_disjoint V2.
  rewrite /V2; apply: mutually_disjoint_prop2.
  move=> i j y => /Zo_S iY /Zo_S jY /setI2_P [_ yi] /setI2_P [_ yj].
  case: (ald _ _ iY jY) => // di; empty_tac1 y.
move: (equipotent_disjointU (conj pc pd) pe pf).
have ->: unionb V2 = T => //.
rewrite /V2;set_extens t.
  by move /setUb_P; bw; move => [y yv1]; bw; move /setI2_P => [].
move=> tT; move: (Tu _ tT) => /setU_P [y ty yY].
have tv: inc t (T \cap y) by apply: setI2_i.
have nei: nonempty (T \cap y) by exists t.
have yv1: inc y V1 by apply: Zo_i => //; apply /nonemptyP.
apply/setUb_P;exists y; bw.
Qed.

Proof by induction on the cardinal of E, when it is finite.

Lemma Exercise4_5b r k: finite_set (substrate r) ->
  order r -> inc k Bnat -> Exercise4_5_hyp r k -> Exercise4_5_conc r k.
Proof.
move /BnatP; set n := cardinal (substrate r).
move: (refl_equal n); rewrite {2} /n.
move: n; move=> n nc nB; move: n nB r k nc; apply: cardinal_c_induction1.
move=> n nB hrec r k csr or kB [[X Xf cX] h2].
The case where E is empty is trivial
case: (emptyset_dichot (substrate r)) => sre.
  move: Xf => /Zo_P []; rewrite /Exercise4_5_conc sre; move /setP_P => Xse _.
  exists emptyset => //;split.
      split;last by move=> a /in_set0.
      by split => //; try split => //; [rewrite setU_0 |move=> a b /in_set0].
    by move/sub_set0: Xse => <-.
  by move=> x /in_set0.
Assumption: we have a free set X with k elements, all other free subsets have at most k elements. We have chosen an element a, the complementary is E'. The results holds, for any k, on sets with less than n elements. In particular, if no free subset of E' has k elements, we can partition E' in k-1 subsets, and add (singleton a) as last set.
have fse: finite_set (substrate r) by red;rewrite - csr; apply /BnatP; fprops.
move: (finite_set_minimal or fse sre) => [a [asr amin]].
move: (card_succ_pr1 (substrate r) a).
rewrite (setC1_K asr) - csr; set E':= _ -s1 _ => eq1.
set r' := induced_order r E'.
have sE': sub E' (substrate r) by apply: sub_setC.
move: (iorder_osr or sE')=> [or' sr'].
set p1:= (cardinal E').
have p1c: p1 = (cardinal (substrate r')) by ue.
move: eq1; rewrite -/p1 => le1.
have cp: cardinalp p1 by rewrite /p1;fprops.
have p1B: inc p1 Bnat by apply/BnatP /(finite_succP cp)/BnatP; rewrite - le1.
 move: (card_lt_succ p1B); rewrite -le1 => p1n {le1 cp}.
have fsE: forall T, inc T (free_subsets r') -> inc T (free_subsets r).
  move=> T /Zo_P [] /setP_P p3 p2; apply /Zo_P;split.
    apply /setP_P; apply: (sub_trans _ sE'); ue.
  move => x y xt yt lexy;apply: p2=> //.
  by apply /iorder_gleP => //;rewrite - sr'; apply: p3.
have h21: forall x, inc x (free_subsets r') -> (cardinal x) <=c k.
  by move=> x xsr; apply: h2; apply: fsE.
rewrite - sr' in sE'.
case: (p_or_not_p (exists2 X',
   inc X' (free_subsets r') & cardinal X' = k)); last first.
  move=> ne.
  set X1 := X -s1 a.
  have X1f: inc X1 (free_subsets r').
    move: Xf => /Zo_P [] /setP_P p3 p2; apply /Zo_P; split.
      apply /setP_P; rewrite sr' => t; move /setC1_P=> [tX ta].
      by apply /setC1_P;split => //; apply: p3.
    move=> u v => /setC1_P [uX _] /setC1_P [vX _] uv.
    by move: (iorder_gle1 uv);apply: p2.
  case: (inc_or_not a X) => aX; last first.
    by case: ne; exists X => //; rewrite - (setC1_eq aX).
  move: (card_succ_pr1 X a); rewrite setC1_K // -/X1 cX.
  set k1:= (cardinal X1) => ks.
  have kB': inc k1 Bnat by apply: BS_nsucc; rewrite /k1; fprops; ue.
  have krec: Exercise4_5_hyp r' k1.
    split; first by exists X1.
    move=> x xsr'; move: (h21 _ xsr') => le1.
    have: (cardinal x) <c k.
      split => //; move=> xk; case: ne; ex_tac.
    by rewrite ks; move /(card_lt_succ_leP kB').
  move: (hrec p1 nB p1B p1n _ _ p1c or' kB' krec)
      => [Y [[[uY adi] ane] cY altY]].
  have nauy: ~(inc a (union Y)).
     by rewrite uY sr' /E'; move /setC1_P => [_].
  have nsY: ~ inc (singleton a) Y.
    move=> say; case: nauy; apply: (@setU_i _ (singleton a)); fprops.
  move: (card_succ_pr nsY); rewrite cY -ks => p3.
  set Y' := (Y +s1 (singleton a)).
  have pr1: union Y' = substrate r.
    set_extens t.
      move=> /setU_P [y ty];case /setU1_P => tY.
        apply: sE'; rewrite -uY; union_tac.
      by move: ty; rewrite tY; move /set1_P => ->.
    move=> tsr; case: (equal_or_not t a) => ta.
      rewrite /Y' - ta;apply /setU_P; exists (singleton t);fprops.
    have: inc t (substrate r') by rewrite sr'; apply /setC1_P; fprops.
    rewrite /Y' -uY => /setU_P [y ty uyY]; union_tac.
  have pr2: forall u v, inc u Y' -> inc v Y' -> u = v \/ disjoint u v.
    move => u v; case /setU1_P => us; case /setU1_P => vs.
        by apply: adi.
      right; rewrite vs; apply: disjoint_pr => t tu /set1_P ta.
      case: nauy; rewrite -ta; union_tac.
    right; rewrite us; apply: disjoint_pr => t /set1_P ta tu.
    case: nauy; rewrite -ta; union_tac.
    by left;rewrite us vs.
  have pr3: alls Y' nonempty.
   move=> u; case /setU1_P; [ by apply: ane| move=> ->; apply: set1_ne].
  exists (Y +s1 (singleton a)); split => //.
  move => x ;case /setU1_P => xy.
    have sx: sub x (substrate r') by rewrite -uY; apply: setU_s1.
    have sx1: sub x (substrate r).
      by apply: (@sub_trans (substrate r')) => //; rewrite sr' //.
    move: (altY _ xy) => []; aw => orx torx.
    move: (iorder_osr or sx1) => [pa pb].
   split => //; rewrite pb=> y z yx zx; case: (torx _ _ yx zx) => le1.
      by left; apply /iorder_gleP => //;move: (iorder_gle1(iorder_gle1 le1)).
      by right; apply /iorder_gleP => //;move: (iorder_gle1(iorder_gle1 le1)).
   have xsr: sub x (substrate r) by rewrite xy; apply: set1_sub.
   move: (iorder_osr or xsr) => [pa pb].
   split => //; rewrite pb xy;move=> y z.
   by move =>/set1_P -> /set1_P ->; left; apply /iorder_gleP; fprops; order_tac.
We assume now that there is a free subset with k elements in E' and partition E' into k parts. Let f T be the set of elements of T that are >= a. Assume that there is Z in the partition such that any free subset that contains no element of f Z has less than k elements. By induction we partition the complement of f Z into k-1 sets, and add f Z as last set.
move=> h22.
have krec: Exercise4_5_hyp r' k by [].
move: (hrec p1 nB p1B p1n _ _ p1c or' kB krec)=> [Y [[[uY adi] ane] cY altY]].
pose f T := Zo T (fun z => gle r a z).
case: (p_or_not_p (exists2 Z, inc Z Y &
   forall T, inc T (free_subsets (induced_order r (E' -s (f Z))))
     -> (cardinal T) <c k)).
  move => [Z ZY hZ].
  set E'':= (E' -s (f Z)).
  set r'':= induced_order r E''.
  have sEs: sub E'' (substrate r).
    apply: (@sub_trans E') => //; apply: sub_setC.
  move: (iorder_osr or sEs) => [or'' sr''].
  set X1:= X \cap (E' -s (f Z)).
  have X1f: inc X1 (free_subsets r'').
    apply: Zo_i; first by apply /setP_P; rewrite sr''; by apply: subsetI2r.
    move=> x y /setI2_P [xX _] /setI2_P [yX _] le1.
    move: Xf => /Zo_P [p3 p2].
     move: (iorder_gle1 le1) => le2; by apply: p2.
  move: (hZ _ X1f) => le1.
  have knz: k <> \0c.
    move=> kz; rewrite kz in le1; case: (card_lt0 le1).
  move: (cpred_pr kB knz); set k1 := cpred k; move => [k1B k1s].
  have krec1: Exercise4_5_hyp r'' k1.
    split; last first.
       by move=> x xr; move: (hZ _ xr);rewrite k1s; move/(card_lt_succ_leP k1B).
    move: Xf => /Zo_P [] /setP_P aa bb.
    have cXp: forall x, inc x (X -s X1) ->
      (inc x X /\ (x = a \/ (inc x Z /\ gle r a x))).
      move=> x /setC_P [xX] /setI2_P => x1.
      split => //; case: (equal_or_not x a) => xa;first by left.
      right; ex_middle aux; case: x1; split => //; apply /setC_P;split => //.
             by apply /setC1_P;split => //; apply: aa.
       by apply /Zo_P.
    have sc: small_set (X -s X1).
      move=> x y xc yc; move: (cXp _ xc) (cXp _ yc) => [xX ex] [yX ey].
      case: ex => xp; case: ey => yp.
            rewrite xp yp //.
          by move: yp; rewrite -xp; move => [_ xy]; apply: bb.
        by symmetry;move: xp; rewrite -yp; move => [_ xy]; apply: bb.
      move: xp yp => [xz _] [yz _].
      have Zs: sub Z (substrate r') by rewrite -uY; apply: setU_s1.
      move: (altY _ ZY) => [orz]; aw => aux.
      case: (aux _ _ xz yz) => le2; move: (iorder_gle1 (iorder_gle1 le2)) => le3.
         by apply: bb.
      by symmetry; apply: bb.
    have X1c: sub X1 X by apply: subsetI2l.
    move: (cardinal_setC X1c); rewrite cX k1s.
    have cX1: cardinalp (cardinal X1) by fprops.
    case: (small_set_pr sc) => cp1.
      rewrite /card_diff cp1 cardinal_set0 csum0r //.
      by move=> le2; move: le1; rewrite le2 -k1s; move => [_ bad]; case: bad.
    rewrite /card_diff; move: cp1; move=> [x] ->.
    rewrite cardinal_set1 - card_succ_pr4 // => ssc.
    have ck: cardinalp k1 by fprops.
    by exists X1 => //; apply: succ_injective1.
  set p2 := cardinal (E' -s (f Z)).
  have p2c: p2 = cardinal (substrate r'') by ue.
  have ee'': sub E'' E' by apply: sub_setC.
  move: (sub_smaller ee''); rewrite -/p1 -/p2 => p12.
  have p2n: p2 <c n by co_tac.
  have p2B: inc p2 Bnat by apply: (BS_le_int p12 p1B).
  move: (hrec p2 nB p2B p2n _ _ p2c or'' k1B krec1)
    => [Y' [[[uY' adi'] ane'] cY' altY']].
  set U1 := (f Z) +s1 a.
  have nauy: ~(inc a (union Y')).
     by rewrite uY' sr''; move /setC_P => [] /setC1_P [_].
  have nsY: ~ inc U1 Y'.
    move=> say; case: nauy; apply: (@setU_i _ U1); rewrite /U1;fprops.
  move: (card_succ_pr nsY); rewrite cY' -k1s => p3.
  have Zr': sub Z (substrate r') by rewrite -uY; apply: setU_s1.
  have Zr: sub Z (substrate r) by apply: (@sub_trans (substrate r')).
  have U1r: sub U1 (substrate r).
    move=> t;case /setU1_P ; last by move => ->.
    by move /Zo_P => [tz _]; apply: Zr.
  set Y'' := Y' +s1 U1.
  have pr1:union Y'' = substrate r.
    set_extens t.
      move=> /setU_P [y ty /setU1_P[]]=> tY.
        apply: sEs; rewrite - sr'' -uY'; union_tac.
         move: ty; rewrite tY;apply: U1r.
      move=> tsr; apply /setU_P;case: (equal_or_not t a) => ta.
      rewrite ta/Y'';exists U1 => //; rewrite /U1;fprops.
    have tE': inc t E' by apply /setC1_P; split.
    case: (inc_or_not t (f Z)) => tf.
      exists U1 => //; rewrite /Y''/U1;fprops.
    have : inc t E'' by apply /setC_P; split.
    rewrite - sr'' -uY'/Y'';move=> /setU_P [y ty yy]; exists y; fprops.
  have aux: forall u,inc u Y' -> disjoint u U1.
      move => u uy; rewrite /U1;apply: disjoint_pr => t tu /setU1_P ta.
      have : inc t (union Y') by union_tac.
      case: ta; last by move => ->;by apply: nauy.
      by rewrite uY' sr'' => tf; move /setC_P => [_]; case.
  have pr2:forall u v, inc u Y'' -> inc v Y'' -> u = v \/ disjoint u v.
    move => u v;case /setU1_P => us; case /setU1_P => vs.
        by apply: adi'.
      by right; rewrite vs; apply: aux.
    by right; apply /disjoint_S;rewrite us; apply: aux.
    by left;rewrite us vs.
  have pr3: alls Y'' nonempty.
    move=> u; case /setU1_P; [ by apply: ane'| move=> ->; exists a].
    rewrite /U1;fprops.
  exists (Y''); split => //.
  move => x;case /setU1_P => xy.
    have sx: sub x (substrate r'') by rewrite -uY'; apply: setU_s1.
    have sx1: sub x (substrate r).
      by apply: (@sub_trans (substrate r'')) => //; rewrite sr'';apply: sEs.
    move: (altY' _ xy) => []; aw => orx torx.
    move: (iorder_osr or sx1) => [pa pb].
    split => //; rewrite pb=> y z yx zx; case: (torx _ _ yx zx) => le2.
      by left; apply /iorder_gleP => //; move: (iorder_gle1 (iorder_gle1 le2)).
    by right;apply /iorder_gleP => //; move: (iorder_gle1(iorder_gle1 le2)).
  move: (iorder_osr or U1r) => [pa pb].
  rewrite xy; split => //; rewrite pb; move=> x1 y1 x1u y1u.
  suff: ocomparable r x1 y1.
    case => cp; [left | right]; apply /iorder_gleP => //.
  red;move: (altY _ ZY) => [_]; aw; move=> torz.
  move: x1u y1u; case /setU1_P=> x1p; case /setU1_P => y1p.
        move: x1p y1p => /Zo_S a1 /Zo_S a2.
        case:(torz _ _ a1 a2) => ax; move: (iorder_gle1(iorder_gle1 ax));fprops.
      by rewrite y1p; move: x1p => /Zo_hi; right.
    by rewrite x1p; move: y1p => /Zo_hi; left.
  by rewrite x1p y1p; left; order_tac.
For each Z in the partition Y, there is g Z a free subset with k elements in the complement of f Z
pose io Z := (induced_order r (E' -s (f Z))).
move=> bad.
have Zp1: forall Z, sub (E' -s (f Z)) (substrate r).
  move=> Z ;by apply: (@sub_trans E'); [ apply: sub_setC | ue].
have Zp2: forall Z, substrate (io Z) = E' -s (f Z).
   by move => Z;rewrite /io; aw.
have sfr: forall Z T, inc Z Y ->
  inc T (free_subsets (io Z)) -> inc T (free_subsets r).
  move=> Z T ZY /Zo_P [] /setP_P pa pb; apply /Zo_P.
  move: (Zp1 Z)(Zp2 Z) => pc pd; rewrite pd in pa.
  split; first by apply /setP_P;apply: (@sub_trans (E' -s (f Z))).
  by move=> x y xT yT xy; apply: pb => //; apply /iorder_gleP => //; apply: pa.
have good: forall Z, inc Z Y -> exists2 T,
     inc T (free_subsets (io Z)) & cardinal T = k.
  move => Z ZY; ex_middle bad2.
  case: bad; exists Z => // => T Tf.
  move: (sfr _ _ ZY Tf) => f1.
  split; first by apply: (h2 _ f1).
  case: (equal_or_not (cardinal T) k) => // Tk; case: bad2; ex_tac.
pose g Z := choose(fun T => inc T (free_subsets(io Z)) /\ cardinal T = k).
have gp1: forall Z, inc Z Y ->
  (inc (g Z) (free_subsets (io Z)) /\ cardinal (g Z) = k).
  by move=> Z /good [t ta tb]; apply choose_pr; exists t.
clear bad good.
Let W the set of all free subsets of E' that have k elements. Then g Z is in W. An element of W intersects Z at most once. By the previous lemma, the intersection of g Z and T is a singleton say sij Z T, whenever Z and T are in the partition. The relations (sij Z T) <= a are false; as well as a <= (sij Z Z).

pose krec1 T:= [/\ inc T (free_subsets r), sub T E' & cardinal T = k].
have gp2: forall Z, inc Z Y -> krec1 (g Z).
  move=> Z ZY; move: (gp1 _ ZY) => [pa pb]; split => //.
    apply: (sfr _ _ ZY pa).
  move: pa =>/Zo_P [] /setP_P pa _.
  apply: (@sub_trans (substrate (io Z))) => //.
  rewrite /io; aw; apply: sub_setC.
have gp3: forall T Z, krec1 T -> inc Z Y -> small_set (T \cap Z).
  move=> T Z [pa pb pc] ZY x y /setI2_P [xT xZ] /setI2_P [yT yZ].
  have Zr': sub Z (substrate r') by rewrite -uY; apply: setU_s1.
  have Zr: sub Z (substrate r) by apply: (@sub_trans (substrate r')).
  move: pa => /Zo_P [_ aux2].
  move: (altY _ ZY) => [_]; aw;move=> tor; case: (tor _ _ xZ yZ)=> aux.
    by move: (iorder_gle1 (iorder_gle1 aux)); apply: aux2.
    by symmetry; move: (iorder_gle1 (iorder_gle1 aux)); apply: aux2.
have gp4: forall T Z, krec1 T -> inc Z Y ->
    singletonp (T \cap Z).
  move => T Z kr; move: (kr) => [kt1 kt2 kt3].
  have stu: sub T (union Y) by rewrite uY sr'.
  apply: (Exercise4_5a cY kt3 kB stu adi).
  move=> z zy;apply: (gp3 _ _ kr zy).
pose sij z1 z2 := union ((g z1) \cap z2).
have sijp: forall z1 z2, inc z1 Y -> inc z2 Y ->
   (g z1) \cap z2 = singleton (sij z1 z2).
  move=> z1 z2 z1Y z2Y; rewrite /sij; move: (gp4 _ _ (gp2 _ z1Y) z2Y) => [s] ->.
  by rewrite setU_1.
have sij1: forall i j, inc i Y -> inc j Y -> inc (sij i j) (g i).
   move => i j iY jY; apply: (@setI2_1 _ j).
   rewrite (sijp _ _ iY jY); fprops.
have sij2: forall i j, inc i Y -> inc j Y -> inc (sij i j) j.
   move => i j iY jY; apply: (@setI2_2 (g i)).
   rewrite (sijp _ _ iY jY); fprops.
have sija1: forall i j, inc i Y -> inc j Y -> gle r (sij i j) a-> False.
  move=> i j iY jY; move: (sij1 _ _ iY jY) => aux2.
  move: (gp1 _ iY) => [] /Zo_P [] /setP_P; rewrite /io; aw=> s1 _.
  move: (s1 _ aux2) => /setC_P [] /Zo_P [pa] /set1_P pb pc _.
  by move => aux1; move: (amin _ aux1).
have sija2: forall i, inc i Y-> gle r a (sij i i) -> False.
  move=> i iY; move: (sij1 _ _ iY iY) => pa pc.
  move: (gp1 _ iY) => [] /Zo_P [] /setP_P; rewrite /io; aw=> s1 _.
  move: (s1 _ pa) => /setC_P [] /Zo_P [pb] /set1_P pe pd _.
  by case: pd; apply: Zo_i=> //; apply: sij2.

Fix T; consider the least of the sij Z T. This exists, since we consider a non-empty finite subset of a totally ordered set. This gives some sj T. These elements are all distinct. Together with a, we get a free subset with k+1 elements, absurd.
pose V1 j:= fun_image Y (fun i => sij i j).
pose sj j := the_least (induced_order r (V1 j)).
have v1p: forall j, inc j Y ->
   let r1 := (induced_order r (V1 j)) in
     [/\ order r1, substrate r1 = V1 j & least r1 (sj j)].
  move=> j jY r1.
  have s1: sub (V1 j) j.
    move => t /funI_P [z zY ->]; apply: (sij2 _ _ zY jY).
  have s0: sub j (substrate r').
    move=> t tj;rewrite -uY; union_tac.
  move: (sub_trans s1 s0) => s2.
  move: (sub_trans s2 sE') => s3.
  move: (sub_trans s0 sE') => s4.
  move: (iorder_osr or s3) => [or1 pb].
  have ne1: nonempty (V1 j) by exists (sij j j); apply /funI_P; ex_tac.
  have fs1: finite_set (V1 j) by apply: ( sub_finite_set s3 fse).
  rewrite /r1;split => //; aw; apply: the_least_pr => //.
  have s5: sub (V1 j) (substrate (induced_order r j)) by aw.
  move: (altY _ jY) => to1.
  rewrite - (iorder_trans r s1).
  apply: finite_subset_torder_least => //.
  rewrite - (iorder_trans r s0) sr'//.
have v2p: forall i j, inc i Y -> inc j Y ->
   gle r (sj i) (sj j) -> i = j.
  move=> i j iY jY leij.
  move: (v1p _ iY) (v1p _ jY) => [o1 sr1 le1][o2 sr2 le2].
  move: le1 => []; rewrite sr1; move /funI_P => [z zY sa] _.
  have sb: inc (sij z j) (substrate (induced_order r (V1 j))).
    rewrite sr2; apply /funI_P; ex_tac.
  move:le2 => [le3 le4]; move: (le4 _ sb) => le5.
  move: (order_transitivity or leij (iorder_gle1 le5)); rewrite sa => le6.
  move: (sijp _ _ zY iY)(sijp _ _ zY jY) => s1 s2.
  move: (gp2 _ zY) => [fk _]; move: fk => /Zo_P [_ fk2].
  move: (fk2 _ _ (sij1 _ _ zY iY) (sij1 _ _ zY jY) le6).
  move: (sij2 _ _ zY iY) (sij2 _ _ zY jY) => i1 i2 sv.
  case: (adi _ _ iY jY) => //; rewrite /disjoint => di.
  empty_tac1 (sij z i); apply: setI2_i => //; ue.
set V2 := fun_image Y sj.
have sii: forall j, inc j Y-> exists2 i, inc i Y & sj j = sij i j.
  move=> j jY; move: (v1p _ jY) => [pa pb [pc pd]].
    move:pc; rewrite pb => /funI_P [z zY ->]; ex_tac.
have v3p: forall j, inc j Y -> inc (sj j) (substrate r).
  move=> l lY;move: (sii _ lY) => [j jY ->].
  apply: sE'; rewrite -uY; move: (sij2 _ _ jY lY) => su; union_tac.
have c2: cardinal V2 = k.
   symmetry; rewrite - cY; apply /card_eqP.
   exists (Lf sj Y V2); hnf; rewrite lf_source lf_target; split => //.
   apply: lf_bijective.
      move=> t TY; apply /funI_P; ex_tac.
    move=> u v uY1 vY ss; apply: (v2p _ _ uY1 vY); rewrite - ss; order_tac.
    by apply: v3p.
  by move => y /funI_P.
set v3:= V2 +s1 a.
have an2: ~ (inc a V2).
  move=> /funI_P [z zY]; move: (sii _ zY) => [j jY] -> ta.
  by case: (sija1 _ _ jY zY); rewrite - ta; order_tac.
move: (card_succ_pr an2); rewrite c2;set (V3:= V2 +s1 a) => bad1.
have V3t: inc V3 (free_subsets r).
  apply: Zo_i.
    apply /setP_P => t; case /setU1_P; last by move => ->.
    by move=> /funI_P [z zY ->];apply: v3p.
  move=> x y ; case /setU1_P => pa; case /setU1_P => pb.
  move: pa pb => /funI_P [z zY ->] /funI_P [z' zY' ->].
        by move=> aux; rewrite (v2p _ _ zY zY' aux).
      rewrite pb; move: pa => /funI_P [z zY ->].
      move: (sii _ zY) => [j jY ->] le1.
      case: (sija1 _ _ jY zY le1).
    rewrite pa; move: pb => /funI_P [z zY ->].
    move: (v1p _ zY) => [qa qb [qc qd]] asj; rewrite qb in qd.
    have sb: inc (sij z z) (V1 z) by apply /funI_P; ex_tac.
    move: (order_transitivity or asj (iorder_gle1 (qd _ sb))) => le2.
    case: (sija2 _ zY le2).
  by rewrite pa pb.
move: (h2 _ V3t); rewrite bad1; move: (card_lt_succ kB) => pa pb; co_tac.
Qed.

Corollary: Assume E finite. Then Hw(k) implies Cw(k).

Lemma Exercise4_5c r k:
  finite_set (substrate r) -> order r -> inc k Bnat ->
  (forall x, inc x (free_subsets r) -> (cardinal x) <=c k) ->
  exists X, [/\ (cardinal X) <=c k,
    union X = (substrate r),
    (forall a b, inc a X -> inc b X -> disjointVeq a b) &
    (forall x, inc x X -> total_order (induced_order r x))].
Proof.
move=> fsr or kB h1.
set T := fun_image (free_subsets r) cardinal.
have neT: nonempty T.
  exists \0c; apply /funI_P; exists emptyset; rewrite ? cardinal_set0 //.
   apply: Zo_i; first by apply /setP_P;fprops.
   by move=> x y /in_set0.
have zb: inc \0c Bnat by fprops.
have sT: sub T (Bintcc \0c k).
  by move=> x /funI_P [z zf ->];apply /BintcP => //; apply: h1.
move: (Binto_wor \0c k) => [hh sio].
move: (worder_total hh) => iot.
move: (iot) => [ior _].
rewrite - sio in sT.
have fss: finite_set (substrate (Bint_cco \0c k)).
  rewrite sio; apply : finite_Bintcc.
move: (sub_finite_set sT fss) => fst.
move: (finite_subset_torder_greatest iot fst sT neT) => [x [xs xg]].
move: xs;aw => /funI_P pa.
have hyp: Exercise4_5_hyp r x.
  split; first by move:pa => [z p1 p2]; ex_tac.
  move => y yf.
  have ct: inc (cardinal y) T by apply /funI_P; ex_tac.
  move: xg; aw; move=> h; move: (h _ ct) => h2; move: (iorder_gle1 h2).
   by move /Binto_gleP => [_ _].
have lxk:x <=c k by move: (proj1 hyp)=> [z zs cs]; ue.
have xB: inc x Bnat by apply: (BS_le_int lxk kB).
move: (Exercise4_5b fsr or xB hyp) => [X [[[p1 p2] p3] p4 p5]].
by exists X;split => //; rewrite p4.
Qed.

Proof by induction on k in the general case; k=0 is trivial

Lemma Exercise4_5d r k:
  order r -> inc k Bnat -> Exercise4_5_hyp r k -> Exercise4_5_conc r k.
Proof.
move=> or kB; move: k kB r or.
apply:cardinal_c_induction.
  move=> r or [hyp1 hyp2]; exists emptyset.
  case: (emptyset_dichot (substrate r)).
     move => ->; rewrite cardinal_set0; split => //.
     split; last by move=> a /in_set0.
     split; first by apply: setU_0.
     by move=> a b /in_set0.
    by move=> x /in_set0.
  move=> [x sxr].
  have px: inc (singleton x) (free_subsets r).
    apply: Zo_i; first by apply /setP_P; apply: set1_sub.
    by move=> u v /set1_P -> /set1_P ->.
  move:(hyp2 _ px); rewrite cardinal_set1 => h.
  by move: (card_le0 h) => h1; case: card1_nz.
move=> k kB hrec r or [[X0 X0f cX0] gensiz].
We assume the result true for k, and X0 is free with k+1 elements. Assume that there is a totally ordered set C, such that any free subset in the complementary has at most k elements. Then there is a free subset with k elements, we can partition the complement into k subsets. With C, this gives k+1 sets.
pose comp C := ((substrate r) -s C).
pose indC C := induced_order r ((substrate r) -s C).
suff: exists C, [/\ sub C (substrate r), (total_order (induced_order r C))&
    (forall T, sub T (comp C) -> (free_subset r T) ->
     (cardinal T) <=c k)].
  move=> [C [Cs torC h1]].
  set E1 := comp C.
  have s1: sub E1 (substrate r) by apply: sub_setC.
  set r1:= indC C.
  move: (iorder_osr or s1) => [or1 sr1].
  have p1: forall x, inc x (free_subsets r1) ->
    (cardinal x) <=c k.
    move => x => /Zo_P [] /setP_P p1 p2.
    have p3: free_subset r x.
     move=> u v ux vx uv; apply:p2 =>//;rewrite /r1 /indC -/(comp C) -/E1 - sr1.
     by apply /iorder_gleP => //; apply: p1.
    rewrite sr1 in p1;exact: (h1 _ p1 p3).
  have i1: inc (X0 \cap E1) (free_subsets r1).
    apply: Zo_i; first by apply /setP_P;rewrite sr1; apply: subsetI2r.
    move=> x y /setI2_P [xX0 xE1] /setI2_P [yX0 yE1] xy.
    move: X0f => /Zo_P [_ X0f1]; apply: X0f1 => //.
    exact (iorder_gle1 xy).
  have X0sr: sub X0 (substrate r).
    by move: X0f =>/Zo_P [] /setP_P X0s X0f.
  case: (emptyset_dichot C) => neC.
    move: (p1 _ i1).
    have ->: X0 \cap E1 = X0.
      rewrite /E1/comp neC;set_extens t; first by move /setI2_P => [].
      move=> tx; apply /setI2_P;split => //; apply /setC_P.
      split => //; [by apply: X0sr | case;case ].
    rewrite cX0; move: (card_lt_succ kB) => pa pb; co_tac.
  have hrec1: Exercise4_5_hyp r1 k.
    split => //; exists (X0 \cap E1) => //.
    move: (p1 _ i1) => rel1; ex_middle q.
    have : (cardinal (X0 \cap E1)) <c k by split.
    have c1: sub (X0 \cap E1) X0 by apply: subsetI2l.
    move:(cardinal_setC c1); rewrite cX0 /card_diff.
    set a := cardinal _; set b := cardinal _.
    have skB: inc (succ k) Bnat by fprops.
    have ca: cardinalp a by rewrite /a; fprops.
    have cb: cardinalp b by rewrite /b; fprops.
    have csa: cardinalp (succ a) by apply: CS_succ.
    move => p2; rewrite -p2 in skB.
    move: (Bnat_in_sum cb skB) (Bnat_in_sum2 ca skB) => bB aB.
    move/ (card_le_succ_ltP _ aB) /(card_le_succ_succP csa (CS_Bnat kB)).
    rewrite -p2 (card_succ_pr4 csa) (card_succ_pr4 ca) - csumA.
    rewrite card_two_pr => p3.
    move: (csum_le_simplifiable aB BS2 bB p3) => b2.
    move: b2 => /card_le2P [x1 [x2 [x1b x2b x12]]].
    move: X0f =>/Zo_P [] /setP_P X0s X0f.
    move: x1b x2b => /setC_P [x10] /setI2_P e1 /setC_P [x20] /setI2_P e2.
    move: (X0s _ x10) (X0s _ x20) => x1s x2s.
    case: (inc_or_not x1 C) => x1C; last by case: e1; split => //; apply /setC_P.
    case: (inc_or_not x2 C) => x2C; last by case: e2; split => //; apply /setC_P.
    move: torC => [_ ]; aw; move => tc.
    case: (tc _ _ x1C x2C) => h; move: (iorder_gle1 h) => aux.
      by case: x12; move: (X0f _ _ x10 x20 aux).
      by case: x12; move: (X0f _ _ x20 x10 aux).
  move: (hrec _ or1 hrec1) => [Y [[[uY adi] ane] cY altY]].
  set X:= Y +s1 C.
  have nCY : ~ (inc C Y).
    move=> CY; move: (ane _ CY) => [x xC].
    have : inc x (union Y) by union_tac.
    rewrite uY sr1 => /setC_P [_ nxc]; contradiction.
  move: (card_succ_pr nCY); rewrite cY -/X => p3.
  have pr1: union X = substrate r.
    rewrite /X;set_extens t.
      move=> /setU_P [y ty /setU1_P]; case => yy; last by apply: Cs; ue.
      apply: s1; rewrite - sr1 -uY; union_tac.
     move=> tsr; apply /setU_P;case: (inc_or_not t C) => tC.
        by exists C;fprops.
     have : inc t (union Y) by rewrite uY sr1; apply /setC_P.
     move /setU_P=> [y ty yY]; exists y; fprops.
  have pr2: forall a b, inc a X -> inc b X -> disjointVeq a b.
    move=> a b; case /setU1_P => aY; case /setU1_P => bY.
          by apply: adi.
        right; rewrite bY; apply: disjoint_pr => u uA.
        have:inc u (union Y) by union_tac.
        by rewrite uY sr1 => /setC_P [_ nxc].
      right; rewrite aY; apply: disjoint_pr => u uA uB.
      have:inc u (union Y) by union_tac.
      by rewrite uY sr1 => /setC_P [_ nxc].
    by left; rewrite aY bY.
  have pr3: alls X nonempty.
    by move=> a; case /setU1_P => ay; [ apply: ane | ue ].
  exists X; rewrite /partition_s; split => //.
  move=> x;case /setU1_P => aY; last by ue.
  move: (altY _ aY); rewrite /r1 /indC iorder_trans //.
  by rewrite -/(comp C) -/E1 - sr1 -uY; apply: setU_s1.
Let sra F X stand for: X is a weak partition of F of totally ordered set with at most k+1 elements. Let sr C mean: for any finite set F, there is X such that sra F X and C \cap F is a subset of one element of X. The previous lemma says that sr holds for the empty set.
pose sra F X := [/\ (cardinal X) <=c (succ k), union X = F,
     (forall a b : Set, inc a X -> inc b X -> disjointVeq a b) &
    (forall Y, inc Y X -> (total_order (induced_order r Y)))].
pose sr C := sub C (substrate r) /\ forall F, finite_set F ->
    sub F (substrate r) -> exists2 X, sra F X &
     exists2 Y, inc Y X & sub (C \cap F) Y.
set ssr:= Zo (powerset (substrate r)) sr.
set sso:= sub_order ssr.
move: (sub_osr ssr) => [osso sssr].
have sre: (sr emptyset).
  split; first by fprops.
  move=> F Fsf Fsr.
  set r1:= induced_order r F.
  move: (iorder_osr or Fsr) => [pa pb].
  have fsr1: finite_set (substrate r1) by ue.
  have fk: forall x, inc x (free_subsets r1)
     -> (cardinal x) <=c (succ k).
    move=> x /Zo_P [] /setP_P xr1 fs1; rewrite pb in xr1.
    apply: gensiz; apply: Zo_i.
       by apply /setP_P; apply: (@sub_trans F) => //.
   by move=> u v ux vx uv; apply: fs1 => //; apply/iorder_gleP => //;apply: xr1.
  have skB: inc (succ k) Bnat by fprops.
  case: (emptyset_dichot F) => eF.
    have pr1:sra F (singleton emptyset).
       rewrite /sra cardinal_set1 eF setU_1; split => //.
          rewrite - succ_zero; apply /(card_le_succ_succP CS0 (CS_Bnat kB)).
          apply: czero_least; fprops.
        by move=> a b /set1_P -> /set1_P ->; left.
      have s1: sub emptyset (substrate r) by fprops.
      move: (iorder_osr or s1) => [pax pbx].
      by move=> a /set1_P ->; split; fprops; aw; move=> x y /in_set0.
    exists (singleton emptyset) => //.
    by exists emptyset; fprops; move => t /setI2_P; case.
  move: (Exercise4_5c fsr1 pa skB fk).
  rewrite /sra;move=> [X [cX uX mdX toX]]; exists X; first split => //.
      ue.
    move=> Y YX; move: (toX _ YX); rewrite /r1 iorder_trans //.
    by rewrite - pb -uX; apply: setU_s1.
  move: eF => [u]; rewrite - pb -uX => /setU_P [y uy yX].
  by ex_tac; move=> t/setI2_P [] /in_set0.
The set of subsets satisfying sr is inductive. Assume we have sets Ci, totally ordered by sub, and let C be the union. Let F be a finite set, Vf = C \cap F. For x in W, there is an index i such that x is in Ci. Since W is finite, there is a greatest such Ci. We deduce C \cap F = Ci \cap F. Then sr C follows trivially.
have isso: inductive sso.
  move=> X sX tio;rewrite sssr in sX.
  set uX:= union X.
  have uXr: sub uX (substrate r).
    apply: setU_s2 => y yX t ty.
    move: (sX _ yX) => /Zo_P [] /setP_P ysr _; apply: (ysr _ ty).
  suff uxs: inc (union X) ssr.
    exists (union X); red; rewrite sssr; split => //.
     by move=> y yX; apply /sub_gleP;split;fprops;apply: setU_s1.
  apply: Zo_i; [ by apply /setP_P | split => //].
  move => F fsF Fsr; set w := ((union X) \cap F).
  case: (emptyset_dichot w) => wne.
    move: sre; move=> [_ h]; move: (h _ fsF Fsr).
    have -> // : emptyset \cap F = w.
    by rewrite wne; apply /set0_P; move=> y /setI2_P [/in_set0].
  pose f x:= choose (fun y => inc x y /\ inc y X).
  have fp: forall x, inc x w -> (inc x (f x) /\ inc (f x) X).
    move=> x /setI2_P [] /setU_P [y p1 p2] _.
    by apply choose_pr; exists y.
  set w1:= fun_image w f.
  move: (sub_finite_set (@subsetI2r (union X) F) fsF) => fsw.
  move: (finite_fun_image f fsw); rewrite -/w -/w1 => fsw1.
  have sw1: sub w1 X.
    by move => t /funI_P [z zw ->]; case: (fp _ zw).
  have w1ne : nonempty w1.
    move: wne => [x xw]; exists (f x); apply /funI_P; ex_tac.
  have sis: substrate (induced_order sso X) = X by aw; ue.
  move: (sw1); rewrite - sis => sw2.
  move: sX; rewrite - sssr => sw3.
  move: (sub_trans sw1 sw3) => sw4.
  move: (finite_subset_torder_greatest tio fsw1 sw2 w1ne) => [x].
  rewrite iorder_trans //; move=> []; aw => xw1 xle.
  move: (sw1 _ xw1) => xX.
  have ->: w = x \cap F.
    set_extens t.
      move=> tw; apply /setI2_P.
      have ft: inc (f t) w1 by apply /funI_P; ex_tac.
      move: (xle _ ft) => /(iorder_gleP _ ft xw1)
          /sub_gleP [fts xsr ftx].
      move: (fp _ tw) => [pa pb]; split; first by apply: (ftx _ pa).
      by apply: (@setI2_2 (union X)).
   move=> /setI2_P[pa pb]; apply /setI2_P;split => //; union_tac.
  move: (sw3 _ xX); rewrite sssr;move => /Zo_P [_ [_ ok]].
  apply: (ok F fsF Fsr).
By Zorn, there is a maximal C satisfying sr; Taking for F a doubleton shows that C is totally ordered
move: (Zorn_lemma osso isso) => [C [Cs Cm]].
move: Cs; rewrite sssr => Cs1; move: (Cs1) => /Zo_P [_ [cp1 cp2]].
have toc: total_order (induced_order r C).
  move: (iorder_osr or cp1) => [pax pbx].
  split => //; rewrite pbx => x y xC yC; red.
  suff: gle r x y \/ gle r y x.
     by case => h; [left| right]; apply /iorder_gleP.
  set F:= doubleton x y.
  have fsF: finite_set F by apply: set2_finite.
  have FC:sub F C by apply: sub_set2.
  have Fsr: sub F (substrate r) by apply: sub_trans cp1.
  move: (cp2 _ fsF Fsr) => [X [pa pb pc pd]] [Y YX si].
  have ysr: sub Y (substrate r).
    by apply: sub_trans Fsr => //; rewrite -pb; apply: setU_s1.
  move: (pd _ YX) => [ory]; aw.
  have xY: inc x Y by apply: si; apply /setI2_P;rewrite /F;split;fprops.
  have yY: inc y Y by apply: si; apply /setI2_P;rewrite /F;split;fprops.
  move=> aux; case: (aux _ _ xY yY) => aux2; move: (iorder_gle1 aux2); fprops.
All we need to do is show that free subsets in the complementary of C have at most k elements. By contradiction, assume there is T with k+1 elements. Let Ci x be the union of C and an element x of T. By maximality, there exists a finite set Ciq x, denoted here F such that for any X such that sra X holds, for any Y in X, (Ci x) \cap F is not a subset of Y. Let G be the union of these sets, together with T.
case: (p_or_not_p (forall T,
      sub T (comp C) -> free_subset r T -> (cardinal T) <=c k)) => hh.
  by exists C.
case: hh => T TC fsT.
have Tc: sub T (substrate r).
  apply: (@sub_trans (comp C)) => //; apply: sub_setC.
have Tf: inc T (free_subsets r) by apply: Zo_i => //; apply /setP_P.
move: (gensiz _ Tf); case: (equal_or_not (cardinal T) (succ k)); last first.
  move=> pa pb; apply /card_lt_succ_leP => //; split => //.
move => cTk _.
pose Ci i := C +s1 i.
pose Cip i F := finite_set F /\ sub F (substrate r)
    /\ forall X, sra F X -> forall Y, inc Y X ->
     ~ ( sub ((Ci i) \cap F) Y).
have Cip1: forall i, inc i T -> exists F, Cip i F.
  move=> i iT; case: (p_or_not_p (gle sso C (Ci i))) => h.
    move: (TC _ iT) => /setC_P [_]; rewrite - (Cm _ h); case; apply: setU1_1.
  ex_middle ef; case: h.
  have cc: sub C (Ci i) by apply : sub_setU1.
  have cc2: sub (Ci i) (substrate r) by apply: setU1_sub => //; apply: Tc.
  apply /sub_gleP;split=> //;apply/ Zo_P; split;first by apply /setP_P.
  split => // F Fsf Fsr; ex_middle exp.
  case: ef; exists F;rewrite /Cip;split => //; split => // X p1 Y YX.
  case: (p_or_not_p (sub ((Ci i) \cap F) Y)) => //.
  move => bad2; case: exp; exists X => //; ex_tac.
pose Ciq i := choose (fun F => Cip i F).
have Cip2: forall i, inc i T -> Cip i (Ciq i).
  by move => i iT; apply: choose_pr; apply: Cip1.
set G:= T \cup (unionb (Lg T Ciq)).
have fG: finite_set G.
  apply: finite_union2; first by rewrite /finite_set cTk ; apply /BnatP; fprops.
   apply: finite_union_finite; fprops; red;bw.
     by move=> i iT; bw; move: (Cip2 _ iT) => [Ok _].
   red; rewrite cTk; apply /BnatP; fprops.
have Gs: sub G (substrate r).
  rewrite /G=> t; case /setU2_P; first by apply: Tc.
  move /setUb_P; bw; move=> [y yd]; bw => tC.
  by move: (Cip2 _ yd) => [_ [Ok _]]; apply: Ok.
By construction there is a partition X of G, and Y such that C \cap G is a subset of Y. We have sra ( Ciq i) (mp i), where mp i is the set of intersections of Ciq i with the elements of X.

move: (cp2 _ fG Gs) => [X [cX uX mdX toX] [Y YX si]].
pose mp i := fun_image X (fun k => (Ciq i) \cap k).
have Cip3: forall i, inc i T -> sra (Ciq i) (mp i).
  move=> i iT.
  have pr1:cardinal (mp i) <=c succ k.
    set fa:= Lf (fun k => (Ciq i) \cap k) X (mp i).
    have ff: function fa.
      apply: lf_function; move=> t tX; apply /funI_P; ex_tac.
    move: (image_smaller_cardinal ff).
    rewrite /fa; aw; set y := image_of_fun _.
    have ->: y = (mp i).
      rewrite /y /mp/image_of_fun lf_source.
      set Ta := [eta intersection2 (Ciq i)].
      have aa: sub X (source (Lf Ta X (fun_image X Ta))) by aw.
      have bb: lf_axiom Ta X (fun_image X Ta)
           by move=> t tx; apply /funI_P; ex_tac.
      set_extens t.
        move /(Vf_image_P ff aa) => [z pa pb]; apply /funI_P; ex_tac.
        rewrite pb /fa; aw.
      move /funI_P => [z pa pb] ;apply /(Vf_image_P ff aa); ex_tac.
      rewrite pb /fa; aw.
    move=> le1; co_tac.
  have pr2: union (mp i) = Ciq i.
    set_extens t.
      move=> /setU_P [y ty] /funI_P [z zX izy].
      by apply:(@setI2_1 _ z); rewrite - izy.
    move=> ti; apply /setU_P.
    have : inc t G by apply /setU2_P; right; apply /setUb_P; bw; exists i;bw.
    rewrite -uX => /setU_P [y ty yX].
    exists ((Ciq i) \cap y) => //; first by apply /setI2_P.
    apply /funI_P; ex_tac.
  have pr3:forall a b, inc a (mp i) -> inc b (mp i) -> disjointVeq a b.
    move=> a b /funI_P [za zaX ->] /funI_P [zb zbX ->].
    case: (mdX _ _ zaX zbX); first by move=> ->; left.
    rewrite {1}/disjoint; right; apply: disjoint_pr => u.
    by move=> /setI2_P [_ ua] /setI2_P [_ ub]; empty_tac1 u; apply: setI2_i.
  split => //.
  move=> Y1 => /funI_P [z zX ->]; move: (toX _ zX) => to1.
    have aux2: sub z (substrate r).
      by apply: sub_trans Gs => //; rewrite -uX; apply: setU_s1.
  have aux1: sub ((Ciq i) \cap z) z by apply: subsetI2r.
  have aux: sub ((Ciq i) \cap z) (substrate (induced_order r z)) by aw.
  move: (total_order_sub to1 aux); rewrite iorder_trans //.
The sets T and Y are disjoint. But T intersects each element of X at most once, thus exactly once, absurd.

have TYe: T \cap Y = emptyset.
  apply /set0_P => y /setI2_P [yT yY].
   move: (Cip2 _ yT) => [pa [pb pc]]; move: (pc _ (Cip3 _ yT)) => aux.
   have YMP: inc ((Ciq y) \cap Y) (mp y) by apply /funI_P; ex_tac.
  case: (aux _ YMP) => t /setI2_P [ta tb]; apply /setI2_P;split => //.
  move: ta; case /setU1_P; last move=> ->; fprops.
  move=> tC;apply: si; apply /setI2_P;split => //; apply /setU2_P;right.
  apply /setUb_P; bw; ex_tac; bw.
have stu: sub T (union X) by rewrite uX /G; apply: subsetU2l.
set k1:= cardinal X.
have ksb: inc (succ k) Bnat by fprops.
have k1B: inc k1 Bnat by apply: (BS_le_int cX ksb).
move:cX; rewrite - cTk -eq_subset_cardP1; move=> [T1 T1S].
move/card_eqP; rewrite -/k1 => pa; symmetry in pa.
have sm:(forall Z : Set, inc Z X -> small_set (T1 \cap Z)).
  move=> Z ZY x y /setI2_P [xT xZ] /setI2_P [yT yZ].
  move: (T1S _ xT) (T1S _ yT) => xt1 yt1.
  have Zr': sub Z G by rewrite -uX; apply: setU_s1.
  have Zr: sub Z (substrate r) by apply: sub_trans Gs.
  move: (toX _ ZY) => [orZ]; aw; move=> tor; case: (tor _ _ xZ yZ)=> aux.
    by move: (iorder_gle1 aux); apply: fsT.
    by symmetry; move: (iorder_gle1 aux); apply: fsT.
move: ((@Exercise4_5a X T1 k1 (refl_equal (cardinal X)) pa k1B
   (sub_trans T1S stu) mdX sm) _ YX).
move=> [x]; aw => sx; move: (set1_1 x); rewrite - sx.
move=> /setI2_P [ha hb]; empty_tac1 x; aw; split => //.
Qed.


Exercise 4.6. We start with some follow-ups to the previous exercise. The notations H, Hw, C and Cw are as above. We first show that a non-empty bounded set of integers has a greatest element. It follows that if Hw(n) holds, then H(k) holds for some k. If Hw(n+h) holds and there is a free subset with n elements, then H(n+k) holds for some k.

Lemma finite_bounded_greatest_B n T:
  inc n Bnat -> (forall m, inc m T -> m <=c n) ->
  nonempty T ->
  exists2 m, inc m T & forall k, inc k T -> k <=c m.
Proof.
move=> nB Tp neT.
have zb: inc \0c Bnat by fprops.
have Ti: sub T (Bintcc \0c n).
  by move=> i iT; bw; move: (Tp _ iT) => lein; apply /BintcP.
have aux: Bnat_le \0c n by split;fprops; apply /BintcP.
move: (sub_finite_set Ti (finite_Bintcc \0c n)) => fst.
move: (Binto_wor \0c n) => [/worder_total iot sio].
rewrite - sio in Ti.
move: (finite_subset_torder_greatest iot fst Ti neT) => [x []].
move: iot=> [ot _];aw => xT aux2; ex_tac.
move=> k kT; move: (iorder_gle1 (aux2 _ kT)).
by move /Binto_gleP => [_ _].
Qed.

Lemma Exercise4_5A1 r n:
  inc n Bnat ->
  (forall x, inc x (free_subsets r) ->
     (cardinal x) <=c n) ->
  exists2 k, inc k Bnat & Exercise4_5_hyp r k.
Proof.
move=> nB hyp.
set T := Zo Bnat (fun k => exists2 x, inc x (free_subsets r) &
   cardinal x = k).
have pa: (forall m, inc m T -> m <=c n).
  by move=> m /Zo_P [mB [x xfr <-]]; apply: hyp.
have neT: nonempty T.
  exists \0c; apply: Zo_i;fprops; exists emptyset.
     by apply: Zo_i; [ apply /setP_P;fprops | move=> x y /in_set0].
    apply: cardinal_set0.
move:(finite_bounded_greatest_B nB pa neT) => [m mT mg].
move: mT => /Zo_P [mb mp]; ex_tac; split => //.
move => x xs.
move: (hyp _ xs) => le1; move: (BS_le_int le1 nB) => cxB.
by apply: mg;apply: Zo_i => //; ex_tac.
Qed.

Lemma Exercise4_5A2 r n h:
  inc n Bnat -> inc h Bnat ->
  (forall x, inc x (free_subsets r) ->
     (cardinal x) <=c (n +c h)) ->
  (exists2 x, inc x (free_subsets r) & (cardinal x = n)) ->
  exists k, [/\ inc k Bnat, k <=c h & Exercise4_5_hyp r (n +c k)].
Proof.
move=> nB hB hyp1 [x xf cx].
move: (Exercise4_5A1 (BS_sum nB hB) hyp1) => [k kB [pa pb]].
move: (pb _ xf); rewrite cx => lexk.
move: (cdiff_pr0 kB nB lexk);set m := _ -c _.
move => [mB aux]; ex_tac; last by rewrite aux.
move: pa => [y ys yx]; move: (hyp1 _ ys); rewrite yx -aux.
move=> aux3; apply: (csum_le_simplifiable nB) => //.
Qed.

Assumptions: we have two non-empty families X and Y with m and n elements. Let E46_hprop h be the property that, whenever we take r+h elements of X, the union of these sets meets at least r elements of Y. Let E46_h h be the property that h is the least integer satisfying this property. Then there is a set with at most n+h elements that meets every element of X and Y.
For simplicity, we assume the domains of X and Y disjoint, and we define an ordering on the union of the domains such that i<j if X(i) meets Y(j).

Section Exercise46.
Variables A X Y m n :Set.
Hypothesis (nB: inc n Bnat) (mB: inc m Bnat).
Hypothesis Xpr:
  [/\ fgraph X, cardinal (domain X) = m, sub (range X) (powerset A) &
   forall i, inc i (domain X) -> nonempty (Vg X i)].
Hypothesis Ypr:
  [/\ fgraph Y, cardinal (domain Y) = n, sub (range Y) (powerset A) &
   forall i, inc i (domain Y) -> nonempty (Vg Y i)].
Hypothesis disdom: disjoint (domain X) (domain Y).

Definition E46_hprop h := forall r Z, r <=c (m -c h) ->
   sub Z (domain X) -> cardinal Z = r +c h ->
   exists T, [/\ sub T (domain Y), cardinal T = r &
   forall j, inc j T -> meet (Vg Y j) (unionb (restr X Z))].

Definition E46_hp h := [/\ inc h Bnat, h <=c m, E46_hprop h &
   forall l, inc l Bnat -> l <=c m -> E46_hprop l -> h <=c l].

Definition E46_conc h := exists B, [/\ (cardinal B) <=c (n +c h),
  finite_set B, (forall i, inc i (domain X) -> meet (Vg X i) B),
  sub B A & (forall j, inc j (domain Y) -> meet (Vg Y j) B)].

Definition E46_u := (domain X) \cup (domain Y).
Definition E46_order_rel x y :=
  x = y \/ [/\ inc x (domain X), inc y (domain Y) & meet (Vg X x) (Vg Y y)].
Definition E46_order_r := graph_on E46_order_rel E46_u.

Lemma Exercise4_6a:
  order_on E46_order_r E46_u /\
  (forall x y, gle E46_order_r x y <->
    [/\ inc x E46_u, inc y E46_u & E46_order_rel x y]).
Proof.
have pa: (forall a : Set, inc a E46_u -> E46_order_rel a a).
  by move => a _; left.
move: (graph_on_sr pa); rewrite -/E46_order_r => sr.
have or: order E46_order_r.
  apply: order_from_rel;split => //.
      move=> y x z; case => xy; first (by rewrite xy); case => yz => //.
        by rewrite -yz; right.
      move: xy yz => [_ yY _][yX _ _];empty_tac1 y.
    move => x y; case => // xy; case => // yx.
    move: xy yx => [_ yY _][yX _ _]; empty_tac1 y.
  by move => x y _; split; left.
split => //; move=> x y; apply /graph_on_P1.
Qed.

We show that there is h such that E46_hp h holds

Lemma Exercise4_6b h: h <=c m ->
  E46_hprop h -> m <=c (n +c h).
Proof.
move => hm hp; move: (BS_le_int hm mB) => hB.
move: (cdiff_pr0 mB hB hm); set r := (m -c h); move=> [rB phm].
have pa: r <=c (m -c h) by rewrite -/r; fprops.
have pb: sub (domain X) (domain X) by fprops.
have pc: cardinal (domain X) = r +c h.
   by rewrite csumC phm; move: Xpr => [_ ok _ _].
move: (hp _ _ pa pb pc) => [T [Td cT _]].
move: (sub_smaller Td); move: Ypr => [_ cdY _ _]; rewrite cT cdY.
have lehh: h <=c h by fprops.
by move=> pd; move: (csum_Mlele pd lehh); rewrite csumC phm.
Qed.

Lemma Exercise4_6c: exists h, E46_hp h.
Proof.
set F:= Zo Bnat (fun h => h <=c m /\ E46_hprop h).
move: Bnat_order_wor => [[pa pb] pc].
have sFb: sub F (substrate Bnat_order) by rewrite pc; apply: Zo_S.
have neF: nonempty F.
  exists m; apply: Zo_i; first (rewrite /E46_hprop;fprops); split; fprops.
  move=> r Z le1 Zd cT.
  exists emptyset;split;fprops;last by move=> j /in_set0.
  rewrite (cdiff_n_n m) in le1.
  rewrite (card_le0 le1) cardinal_set0 //.
move: (pb _ sFb neF) => [h []]; aw => /Zo_P [hB [lhm hp]] hm.
exists h;split => //.
move=> l lB lm lp; have lF: inc l F by apply: Zo_i.
by move: (iorder_gle1 (hm _ lF)); move /Bnat_order_leP => [_ _].
Qed.

We restate E46_hprop h as a property of the ordering

Lemma Exercise4_6d h: E46_hprop h <->
  forall r Z, r <=c (m -c h) ->
   sub Z (domain X) -> cardinal Z = r +c h ->
   exists T, [/\ sub T (domain Y), cardinal T = r &
   forall j, inc j T -> exists2 i, inc i Z & gle E46_order_r i j].
Proof.
move: Exercise4_6a Xpr => [[oR sR] rR] [fgX _].
split; move=> aux r Z pa pb pc;
   move: (aux _ _ pa pb pc) => [T [tdY cT aux1]]; exists T;split => // j jT.
  move: (aux1 _ jT) => [k] /setI2_P [kVg] /setUb_P [y].
  rewrite restr_d // => yd; rewrite restr_ev//.
  have yX: inc y (domain X) by apply: pb.
  have jY: inc j (domain Y) by apply: tdY.
  move=> kV1; ex_tac; apply/rR;rewrite /E46_u; split;fprops.
  by right; split => //;exists k; apply: setI2_i.
move: (aux1 _ jT) => [i iZ]; move / rR => [_ _ ].
case => h0.
  empty_tac1 j;rewrite -h0; fprops.
move: h0 => [_ _ [k]] /setI2_P [k1 k2]; exists k; apply /setI2_P;split => //.
apply /setUb_P; exists i; rewrite ?restr_d //; rewrite restr_ev//.
Qed.

Proprety E46_hprop h says that free subsets are not too big

Lemma Exercise4_6e h K:
  inc h Bnat -> E46_hprop h -> inc K (free_subsets E46_order_r) ->
  (cardinal K) <=c (n +c h).
Proof.
move=> hB; rewrite Exercise4_6d => aux free.
set Z := K \cap (domain X).
set Z1 := K \cap (domain Y).
have ZX: sub Z (domain X) by apply: subsetI2r.
have Z1Y: sub Z1 (domain Y) by apply: subsetI2r.
move: Exercise4_6a => [[oR sR] rR].
move: free => /Zo_P [] /setP_P;rewrite sR /E46_u; move=> pa pb.
have uZ: K = Z \cup Z1.
  rewrite - (set_IU2r K (domain X) (domain Y)).
  by symmetry; apply /setI2id_Pl.
have dj: disjoint Z Z1.
   apply: disjoint_pr => u ux uy; empty_tac1 u; aw;split => //.
move: (csum2_pr5 dj); rewrite -uZ - csum2_pr2b - csum2_pr2a => cs.
have ca: cardinalp (cardinal Z) by fprops.
have cn: cardinalp h by fprops.
move: Ypr => [_ cY _ _]; move: Xpr => [_ cX _ _].
case: (card_le_to_ee ca cn).
  move: (sub_smaller Z1Y) => aux1 aux2; move: (csum_Mlele aux2 aux1).
  by rewrite - cs csumC cY.
move => le1.
have cZB: inc (cardinal Z) Bnat.
  have fsdX: finite_set (domain X) by red; rewrite cX; apply /BnatP.
  by move: (sub_finite_set ZX fsdX) => /BnatP.
move: (cdiff_pr0 cZB hB le1); set r := (_ -c h); move=> [rB phm].
move: (sub_smaller ZX); rewrite cX => Zm.
have c2:cardinal Z = r +c h by symmetry; rewrite csumC.
rewrite cs c2 csumC csumA.
apply: csum_Mlele; last by fprops.
have c1: r <=c (m -c h).
   rewrite -phm in Zm; apply: (csum_le_simplifiable hB) => //; fprops.
   rewrite cdiff_pr //.
   have le2: h <=c (h +c r) by apply: csum_M0le; fprops.
   co_tac.
move: (aux _ _ c1 ZX c2) => [T [TdY cT etc]].
have di: disjoint Z1 T.
  apply: disjoint_pr => j jZ1 jT; move: (etc _ jT) => [i iZ le].
  have iK: inc i K by rewrite uZ; apply /setU2_P; left.
  have jK: inc j K by rewrite uZ; apply /setU2_P; right.
  move: (pb i j iK jK le) => ij.
  by empty_tac1 i; rewrite ij.
move:(csum2_pr5 di); rewrite - cY - cT csum2_pr2b csum2_pr2a => <-.
apply: sub_smaller; move=> t; case /setU2_P => ta; fprops.
Qed.

Property E46_hp h says H(n+k) for some k

Lemma Exercise4_6f h: inc h Bnat -> E46_hprop h ->
  exists k, [/\ inc k Bnat, k <=c h & Exercise4_5_hyp E46_order_r (n +c k)].
Proof.
move=> hB hp; apply: Exercise4_5A2 => //.
   move=> x xs;apply: Exercise4_6e => //.
move: Exercise4_6a => [[oR sR] rR].
exists (domain Y).
apply: Zo_i; first by apply /setP_P;rewrite sR /E46_u; apply: subsetU2r.
move=> x y; rewrite rR; move=> xY yY [_ _ ]; case => //; move=> [xX _].
  empty_tac1 x.
by move: Ypr => [_ pa _].
Qed.

Lemma Exercise4_6g h: E46_hp h ->
  exists k, [/\ inc k Bnat, k <=c h & Exercise4_5_conc E46_order_r (n +c k)].
Proof.
move=> [hB _ hprop _]; move: (Exercise4_6f hB hprop).
move=> [k [kB pa pb]]; ex_tac.
move: Exercise4_6a => [[oR sR] rR].
by move: (Exercise4_5d oR (BS_sum nB kB) pb).
Qed.

We apply the previous exercise. It gives a partition of E into totally ordered sets. Note that an ordered set U is either singleton A, where A is in X or Y, or a doubleton (A,B) where A is in X and B in Y, and these sets meet; let xU be an element of A in the first case, an element of A \cap B in the second case. The set of these xU is a solution.

Lemma Exercise4_6h h: E46_hp h -> E46_conc h.
Proof.
move=> hp; move: (Exercise4_6g hp) => [k [kB kh [C [pC cc altc]]]].
move: pC => [[pca pcc] pcb].
move: Exercise4_6a => [[oR sR] rR].
red in disdom.
have tcp: forall x a b, inc x C -> inc a x -> inc b x ->
   [\/ a = b, glt E46_order_r a b | glt E46_order_r b a].
  move=> x a b xC ax bx; case: (equal_or_not a b) => nab; first by in_TP4.
  have nba: b <> a by apply:nesym.
  have sxs: sub x (substrate E46_order_r) by rewrite -pca; apply: setU_s1.
  move: (altc _ xC) => [or]; aw; move => aux; move: (aux _ _ ax bx).
  by case => aux2; [constructor 2 | constructor 3]=> //;move:(iorder_gle1 aux2).
have tcp1: forall i j, glt E46_order_r i j ->
  [/\ inc i (domain X), inc j (domain Y) & meet (Vg X i) (Vg Y j)].
  move=> i j [leij nij]; move: leij;rewrite rR; move => [isR jsR].
  case => h0 //.
have tcp2: forall x, inc x C ->
  [\/ (exists2 i, inc i (domain X) & x = singleton i),
      (exists2 j, inc j (domain Y) & x = singleton j) |
      (exists i j, glt E46_order_r i j /\ x = doubleton i j)].
  move=> x xC; move: (pcb _ xC) => xne.
  move: (xne) => [y yx].
  case: (equal_or_not x (singleton y)) => xs.
    have: inc y (union C) by union_tac.
    rewrite pca sR /E46_u.
    case /setU2_P => yc; [constructor 1 | constructor 2 ]; ex_tac.
  have [z zx yz]: exists2 z, inc z x & y <> z.
    ex_middle bad; case: xs; apply set1_pr => // z zx.
    ex_middle ty; case: bad; exists z;fprops.
  have [i [j [ix jx ltij]]]: exists i j, [/\ inc i x, inc j x &
    glt E46_order_r i j].
    case: (tcp _ _ _ xC yx zx); first (by contradiction); case => h0.
       by exists y, z.
     by exists z, y.
  move: (tcp1 _ _ ltij) => [iX jY _].
  constructor 3; exists i, j; split => //.
  set_extens t; last by case /set2_P => ->.
  move => tx; case: (tcp _ _ _ xC tx ix); first by move => ->; fprops.
    by move => ti; move: (tcp1 _ _ ti) => [_ iY _]; empty_tac1 i; aw.
  case: (tcp _ _ _ xC jx tx); first by move => ->; fprops.
    by move => tj; move: (tcp1 _ _ tj) => [jX _]; empty_tac1 j; aw.
  move => ti tj; move: (tcp1 _ _ ti) (tcp1 _ _ tj) => [tX _ _] [_ tY _].
  empty_tac1 t.
 pose xup x y:= forall i,
    ( (inc i (x \cap (domain X)) -> inc y (Vg X i) ) /\
      (inc i (x \cap (domain Y)) -> inc y (Vg Y i))).
pose f x := choose (fun y => xup x y).
have fp1: forall x, inc x C -> xup x (f x).
  move=> x xc; apply: choose_pr; case: (tcp2 _ xc).
      move => [i idX ->]; exists (rep (Vg X i)); red.
      move=> j;split; move => /setI2_P [] /set1_P -> uu.
        by apply: rep_i;move: Xpr => [_ _ _ hh]; apply: hh.
      empty_tac1 i; apply /setI2_P;split => //.
    move => [i idX ->]; exists (rep (Vg Y i)); red.
    move=> j; split; move => /setI2_P [] /set1_P -> uu.
      empty_tac1 i; aw.
    by apply: rep_i;move: Ypr => [_ _ _ hh]; apply: hh.
  move=> [i [j [ltij]]] ->; move: (tcp1 _ _ ltij) => [idx jdy mt].
  exists (rep ((Vg X i) \cap (Vg Y j))).
  move: (rep_i mt) => /setI2_P; set r:= rep _; move=> [ra rb].
  move => z;aw;split; move => /setI2_P [];case /set2_P => -> bad //.
    empty_tac1 j; aw.
  empty_tac1 i; aw.
set B:= fun_image C f.
have pa: (cardinal B) <=c (n +c h).
  have sjb: (surjection (Lf f C (fun_image C f))).
    apply: lf_surjective; first by move=> t ta; apply /funI_P; exists t.
    move=> y /funI_P //.
  move: (image_smaller_cardinal (proj1 sjb)); rewrite (surjective_pr0 sjb).
  aw; rewrite -/B => le1.
  have le2: ((cardinal C) <=c (n +c h)).
    rewrite cc; apply: csum_Mlele => //; fprops.
  co_tac.
have pb: finite_set B.
  move: hp => [hB _ _ _].
  red; apply /BnatP; apply: (@BS_le_int _ (n +c h)); fprops.
have sBA: sub B A.
  move=> t /funI_P [z zC ->]; move: (fp1 _ zC) => fz.
  move: Xpr Ypr => [fgX _ rpX _][fgY _ rpY _].
  have auxx: forall i y, inc i (domain X) -> inc y (Vg X i) -> inc y A.
    move=> i y id yv.
    have : sub (Vg X i) A.
       apply /setP_P; apply: rpX; apply /(range_gP fgX); ex_tac.
    by apply.
  have auxy: forall i y, inc i (domain Y) -> inc y (Vg Y i) -> inc y A.
    move=> i y id yv.
    have : sub (Vg Y i) A.
       apply /setP_P; apply: rpY; apply /(range_gP fgY); ex_tac.
    by apply.
  case: (tcp2 _ zC).
      move=> [i idx zi].
      have ii2: inc i (z \cap (domain X)) by rewrite zi; fprops.
      move: (fz i) => [fa _]; move: (fa ii2) => fv; apply: (auxx _ _ idx fv).
    move=> [i idx zi].
    have ii2: inc i (z \cap (domain Y)) by rewrite zi; fprops.
    move: (fz i) => [_ fa]; move: (fa ii2) => fv; apply: (auxy _ _ idx fv).
  move=> [i [j [ltij zi]]]; move: (tcp1 _ _ ltij) => [idx jdy mt].
  have ii2: inc j (z \cap (domain Y)) by rewrite zi; fprops.
  move: (fz j) => [_ fa]; move: (fa ii2) => fv; apply: (auxy _ _ jdy fv).
exists B; split => // i idx.
  have : inc i (union C) by rewrite pca sR /E46_u; fprops.
  move=> /setU_P [y iy yC]; move: (fp1 _ yC i) => [fa _].
  move: (fa (setI2_i iy idx)) => pc.
  exists (f y); apply /setI2_P;split => //; apply /funI_P; ex_tac.
have : inc i (union C) by rewrite pca sR /E46_u; fprops.
move=> /setU_P [y iy yC]; move: (fp1 _ yC i) => [_ fa].
move: (fa (setI2_i iy idx)) => pc.
exists (f y); apply /setI2_P;split => //; apply /funI_P; ex_tac.
Qed.
End Exercise46.

Assume A(x) is a subset of F for any x in E. We want to know when E46b_hyp holds, namely that there exists an injection f such that f(x) is in A(x), or when E46c_hyp G holds (this is E46b_hyp , where moreover G is a subset of the image of f.
Let E46b_conc be the assertion: for any set H, the union of all A(x), for x in H has at least as many elements as H, and let E46c_conc G be: for any subset L of G, the number of elements x such that A(x) meets L is at least the cardinal of L.
We have: E46b_hyp implies E46b_conc, and E46c_hyp G implies E46b_conc and E46c_conc G.

Definition E46b_hyp E F A :=
  exists2 f, injection_prop f E F &
  (forall x, inc x E -> inc (Vf f x) (A x)).

Definition E46c_hyp E F A G :=
  exists f, [/\ injection_prop f E F,
  sub G (image_of_fun f) & (forall x, inc x E -> inc (Vf f x) (A x))].

Definition E46b_conc E A :=
  forall H, sub H E ->
  (cardinal H) <=c (cardinal (union (fun_image H A))).

Definition E46c_conc E A G :=
  forall L, sub L G ->
    (cardinal L) <=c (cardinal (Zo E (fun z => meet (A z) L))).

Lemma Exercise4_6i E F A: E46b_hyp E F A -> E46b_conc E A.
Proof.
move=> [f [injf sf tf] fp] H HE.
set fH:= image_by_fun f H.
have ff: function f by fct_tac.
have shs:sub H (source f) by ue.
have pa:sub fH (union (fun_image H A)).
  move=> t /(Vf_image_P ff shs) [u uH ->].
  move: (fp _ (HE _ uH)) => aux; apply /setU_P;exists (A u) => //.
  apply /funI_P; ex_tac.
move: (sub_smaller pa) => pb.
move: (equipotent_restriction1 shs injf); rewrite -/fH.
by move /card_eqP => ->.
Qed.

Lemma Exercise4_6j E F A G: E46c_hyp E F A G ->
  (E46b_conc E A /\ E46c_conc E A G).
Proof.
move => [f [[injf pa pb] pc pd]].
split; first by apply: (@Exercise4_6i _ F) ; exists f => //.
move => L LG; set K := inv_image_by_fun f L.
have ff: function f by fct_tac.
have Ksf: sub K (source f).
  move=> t /iim_graph_P [u uL Jg]; Wtac.
have aux: L = image_by_fun f K.
   set_extens t.
    move => tL; apply /(Vf_image_P ff Ksf).
    move: (pc _ (LG _ tL)) => /(Vf_image_P1 ff) [x xsf Jg].
    exists x => //; apply /iim_graph_P; exists t => //; rewrite Jg; Wtac.
  move /(Vf_image_P ff Ksf) => [u ui ->]; move:ui => /iim_graph_P [v vL Jg].
  by rewrite - (Vf_pr ff Jg).
move: (equipotent_restriction1 Ksf injf).
rewrite -aux; move /card_eqP=> <-; apply: sub_smaller.
move => t /iim_graph_P [u uL jg]; move: (p1graph_source ff jg) => tf.
rewrite pa in tf;apply: Zo_i => //; move: (pd _ tf); rewrite - (Vf_pr ff jg).
by move=> ua; exists u; apply /setI2_P.
Qed.

Converse: E46b_conc and E46c_conc G imply E46b_conc if E and F are finite

Lemma Exercise4_6k E F A G:
  finite_set F -> sub G F ->
  (forall x, inc x E -> sub (A x) F) ->
   E46b_conc E A -> E46c_conc E A G -> E46b_hyp E F A.
Proof.
move=> fsF GF Ap h1 h2.
we consider some ordering on the disjoint union of E, F and G
set za:= \0c; set zb:= \1c; set zc:= \2c.
set Gi:= G *s1 za.
set Fi:= F *s1 zb.
set Ei:= E *s1 zc.
set Et := Gi \cup (Fi \cup Ei).
have Gp1: forall x, inc x G -> inc (J x za) Et.
   by move=> x xG; apply /setU2_P;left; apply:indexed_pi.
have Fp1: forall x, inc x F -> inc (J x zb) Et.
  by move=> x xG; apply /setU2_P;right; apply /setU2_P;left; apply:indexed_pi.
have Ep1: forall x, inc x E -> inc (J x zc) Et.
  by move=> x xG;apply /setU2_P;right; apply /setU2_P;right; apply:indexed_pi.
pose rc x y := [\/ x = y, [/\ Q x = za, Q y = zb & P x = P y] |
    [/\ (Q x = za \/ Q x = zb), Q y = zc & inc (P x) (A (P y))]].
set r := graph_on rc Et.
have sr: substrate r = Et by apply: graph_on_sr; move=> a _; in_TP4.
have rvP: forall x y, gle r x y <-> [/\ inc x Et, inc y Et & rc x y].
  by move=> x y; apply /graph_on_P1.
have nab: za <> zb by rewrite /za /zb; fprops.
have nac: zc <> za by rewrite /za /zc; apply: card2_nz.
have nbc: zb <> zc by rewrite /zb /zc; apply: card_12.
have trr: transitive_r rc.
  move => x y z xy; case: (xy); first by move=> ->.
    move=> aux; case; first by move=> <-.
      by move: aux => [_ pa _] [pb _ _]; case: nab; rewrite - pa - pb.
    move => [a2 pa pb]; case: a2.
      by move => a2; case: nab; rewrite -a2; move : aux => [_ -> _].
    by move: aux => [pc pd pe] h; constructor 3; rewrite pe; split => //; left.
  move=> [pa pb pc]; case; first by move => <-.
    by move => [pd _ _]; case: nac; rewrite -pb -pd.
  rewrite pb;move => [pd _ _];case: pd => pd; [ by case: nac | by case: nbc].
have arr: antisymmetric_r rc.
  move => x y xy; case: xy; first by move=> ->.
    move=> aux; case; first by move=> <-.
      by move: aux => [_ pa _] [pb _ _]; case: nab; rewrite - pa - pb.
    by move: aux => [pa _ _] [_ pb _]; case: nac; rewrite - pa - pb.
  move=> [_ pb _]; case; first by move => <-.
    by move => [pd _ _]; case: nac; rewrite -pb -pd.
  rewrite pb;move => [pd _ _];case: pd => pd; [ by case: nac | by case: nbc].
have or: order r.
  apply: order_from_rel;split => //.
  by move=> x y _; split; constructor 1.
We consider the size of the biggest free subset
set m := cardinal F.
have pa: (exists2 x, inc x (free_subsets r) & cardinal x = m).
  exists Fi; last by apply /card_eqP; eqsym; rewrite /m /Fi; fprops.
  apply: Zo_i; first by apply /setP_P; rewrite sr /Et => t; fprops.
  move=> x y xFi yFi; move: xFi yFi=> /indexed_P [_ _ qx] /indexed_P [_ _ qy].
  move /rvP => [_ _]; case => //.
    by move=> [qxa _]; case: nab; rewrite -qx -qxa.
  by move=> [_ qya _]; case: nbc; rewrite -qy -qya.
have pb: forall x, inc x Et -> pairp x.
  by move => x;case /setU2_P; [ | case /setU2_P]; move/indexed_P => [].
have pc: Exercise4_5_hyp r m.
  split => // x0 => /Zo_P [] /setP_P; rewrite sr; move=> xET x0f.
  pose f x := Yo (Q x = za) (J (P x) zb) x.
  set x1 := fun_image x0 f.
  have x1E: sub x1 Et.
    rewrite /x1; move=> t /funI_P [z zx0 ->].
    move: (xET _ zx0) => zEt; rewrite /f; Ytac zza => //;apply: Fp1.
    move: (zEt); case /setU2_P.
      by move /indexed_P => [_ hh _]; apply: GF.
    by case /setU2_P;move/indexed_P => [_ h3 h4]//;case: nac;rewrite -h4 - zza.
  have x1f: free_subset r x1.
    move=> x y /funI_P [u ux0 ->] /funI_P [v vx0 ->] h.
    case: (equal_or_not u v) => nuv; first by rewrite nuv.
    move: (xET _ ux0)(xET _ vx0) => uEt vEt.
    move: h;rewrite /f; Ytac uza; Ytac vza.
          by move /rvP=> [_ _]; case => //;aw;
             move => [xx yy]; [case: nab | case: nbc].
        move /rvP => [_ _]; case => //; aw; first by move => [p1]; case: nab.
        move => [_ aa bb].
        case: nuv;apply: (x0f u v ux0 vx0); apply /rvP; split => //.
        by constructor 3; split => //; left.
     move /rvP => [ _ _]; case => //; aw; move => [aa bb] //.
    move=> uv;case: nuv; apply: (x0f u v) => //.
  have -> : cardinal x0 = cardinal x1.
    apply /card_eqP; exists (Lf f x0 x1); split; aw; apply: lf_bijective.
        move=> t tx0; apply /funI_P; ex_tac.
      move=> u v ux0 vx0; rewrite /f; Ytac uza; Ytac vza.
            move: (pb _ (xET _ ux0)) (pb _ (xET _ vx0)) => xp yp sJ.
            apply: pair_exten => //; [apply: (pr1_def sJ) | ue ].
          move=> sj; move: (f_equal P sj) (f_equal Q sj); aw => qa qb.
          by apply: (x0f u v) => //; apply /rvP;split;fprops; constructor 2.
        move=> sj; move: (f_equal P sj) (f_equal Q sj); aw => qa qb.
        by symmetry;apply:(x0f v u)=>//; apply /rvP;split;fprops; constructor 2.
      trivial.
    by move=> y/funI_P.
  set H1 := Zo E (fun z => inc (J z zc) x1).
  set H2 := Zo F (fun z => inc (J z zb) x1).
  have ->: cardinal x1 = (cardinal H1) +c (cardinal H2).
    have ->: x1 = (x1 \cap Ei) \cup (x1 \cap Fi).
    rewrite - (set_IU2r x1 Ei Fi); symmetry; apply /setI2id_Pl.
    move => t; case /funI_P => [z zx0 ->].
       move: (xET _ zx0); case /setU2_P.
         move /indexed_P => [pz Pz Qz]; apply /setU2_P; right.
         by rewrite /f; Ytac0; apply: indexed_pi; apply: GF.
       case /setU2_P; move /indexed_P => [pz Pz Qz]; rewrite /f.
         rewrite Qz; Ytac0; apply /setU2_P; right; by apply /indexed_P.
         rewrite Qz; Ytac0; apply /setU2_P; left; by apply /indexed_P.
    transitivity (H1 +c H2); last by apply: csum2_pr4; fprops.
    have di: disjoint (x1 \cap Ei) (x1 \cap Fi).
      by apply: disjoint_pr; move => u /setI2_P [_] /indexed_P [_ _ qc]
       /setI2_P [_] /indexed_P[_ _ qb]; case: nbc; rewrite - qc -qb.
    rewrite (csum2_pr5 di); apply: csum2_pr4.
       exists (Lf P (x1 \cap Ei) H1).
        split; aw => //; apply: lf_bijective.
            move=> t /setI2_P [tx1] /indexed_P [pt PE Qt].
            by apply: Zo_i => //; rewrite -Qt pt.
         move=> u v /setI2_P [_] /indexed_P [pt _ Qt]
           /setI2_P [_] /indexed_P [pv _ Qv].
           by move=> aux; apply: pair_exten => //; ue.
        move=> y /Zo_P [yE px1].
        by exists (J y zc)=> //;aw;apply /setI2_P;split => //;apply: indexed_pi.
      exists (Lf P (x1 \cap Fi) H2).
        split; aw => //; apply: lf_bijective.
            move=> t /setI2_P [tx1] /indexed_P [pt PE Qt].
            by apply: Zo_i => //; rewrite -Qt pt.
          move=> u v /setI2_P [_] /indexed_P [pt _ Qt]
            /setI2_P[_] /indexed_P [pv _ Qv] aux.
           apply: pair_exten => //; ue.
        by move=> y =>/Zo_P [yE px1]; exists (J y zb); aw;
        apply /setI2_P; split => //; apply: indexed_pi.
  have hE: sub H1 E by apply: Zo_S.
  move: (h1 _ hE); set K:= (union _).
  have KM: sub K F.
    move=> t /setU_P [y ty] /funI_P [z zH1 zh2].
    move: zH1 => /Zo_P [zE _].
    by move: (Ap _ zE); rewrite - zh2; apply.
  move: (cardinal_setC KM); rewrite -/m.
  suff: (sub H2 (F -s K)).
    move=> s1; move: (sub_smaller s1) => qa qb qc.
    by rewrite -qb; apply: csum_Mlele.
  move=> t =>/Zo_P [tF px1]; apply /setC_P;split => //.
  move=> /setU_P [y ty] /funI_P [z zH1 Az].
  move: zH1 => /Zo_P [zE J2x1].
  have le1: (gle r (J t zb) (J z zc)).
    apply /rvP;split;fprops; constructor 3; aw.
    split => //; [ by right | by rewrite - Az].
  move: (pr2_def (x1f _ _ px1 J2x1 le1)); exact nbc.
To each element x of F we associate the set of the partition that contains x; this is a bijection f; we get similarly an injection g on E.
have mB: inc m Bnat by move: fsF => /BnatP.
move: (Exercise4_5d or mB pc) => [X [[[uX deX] neX] cX toeX]].
pose f x := choose (fun z => inc (J x zb) z /\ inc z X).
have fp1: forall x, inc x F -> (inc (J x zb) (f x) /\ inc (f x) X).
  move=> x xF; apply choose_pr;move:(Fp1 _ xF); rewrite - sr -uX;move /setU_P.
  by move => [t t1 t2]; exists t.
have taf: lf_axiom f F X by move => t tF; move: (fp1 _ tF) => [p1 p2].
have bijF: bijection (Lf f F X).
   apply:bijective_if_same_finite_c_inj;first by rewrite lf_source lf_target cX.
     aw.
  apply: lf_injective => //.
  move => u v uF vF; move: (fp1 _ uF) (fp1 _ vF) => [p1 p2] [p3 p4] sf.
  have sfu: sub (f u) (substrate r) by rewrite -uX; apply: setU_s1.
  rewrite - sf in p3; move: (toeX _ p2) => [orf]; aw.
  move=> aux; move: (aux _ _ p1 p3); case => leuv; move: (iorder_gle1 leuv)
     => /rvP [qa qb]; case => aux1.
            apply: (pr1_def aux1).
         by move: aux1; aw; move=> [r1 _ _]; case: nab.
       by move: aux1; aw; move=> [_ r1 _]; case: nbc.
     by rewrite (pr1_def aux1).
     by move: aux1 => [_ _ ]; aw.
   by move: aux1; aw; move=> [_ r1 _]; case: nbc.
pose g x := choose (fun z => inc (J x zc) z /\ inc z X).
have gp1: forall x, inc x E -> (inc (J x zc) (g x) /\ inc (g x) X).
  move=> x xE;apply choose_pr;move: (Ep1 _ xE); rewrite - sr -uX; move/setU_P.
  by move => [t t1 t2]; exists t.
have tag: lf_axiom g E X by move => t tE; move: (gp1 _ tE) => [p1 p2].
have bijG: injection (Lf g E X).
  apply: lf_injective => //.
  move => u v uF vF; move: (gp1 _ uF) (gp1 _ vF) => [p1 p2] [p3 p4] sf.
  have sfu: sub (g u) (substrate r) by rewrite -uX; apply: setU_s1.
  rewrite - sf in p3; move: (toeX _ p2) => [orf]; aw.
  move=> aux; move: (aux _ _ p1 p3); case => leuv; move: (iorder_gle1 leuv)
     => /rvP [qa qb]; case; aw => aux1.
            apply: (pr1_def aux1).
         by move: aux1 => [_ _].
       by move: aux1 => [aux2 _ _];case: aux2=> h; [case: nac | case: nbc].
     by rewrite (pr1_def aux1).
   by move: aux1 => [_ _ ->].
  by move: aux1 => [aux2 _ _];case: aux2=> h; [case: nac | case: nbc].
By composition, we have an injection E->F, a solution to the problem
set h := compose (inverse_fun (Lf f F X)) (Lf g E X).
have sh: source h = E by rewrite /h; aw.
have th: target h = F by rewrite /h; aw.
move: (inverse_bij_fb bijF) => bif.
have cifg: composable (inverse_fun (Lf f F X)) (Lf g E X).
  split => //; try fct_tac; aw.
have ih: injection h by apply: compose_fi => //; move: bif => [ok _].
have ph: forall x, inc x E -> inc (Vf h x) (A x).
  move=> x xE; rewrite /h; aw.
  set y := Vf (inverse_fun (Lf f F X)) (g x).
  have yF: inc y F.
     have ->: F = target (inverse_fun (Lf f F X)) by aw.
     by apply: Vf_target; try fct_tac; aw; apply: tag.
  move: (fp1 _ yF) (gp1 _ xE) => [p1 p2] [p3 p4].
  have aux: inc (g x) (target (Lf f F X)) by aw; apply: tag.
  move: (inverse_V bijF aux); rewrite -/y; aw.
  move=> eq0; rewrite - eq0 in p3.
  have sfy:sub (f y) (substrate r) by rewrite -uX; apply: setU_s1.
  move: (toeX _ p2) => [orX]; aw.
  move=> aux1; move: (aux1 _ _ p1 p3); case => leuv; move: (iorder_gle1 leuv);
    move /rvP=> [qa qb]; case => aux2;
     try (case: nbc;move: (pr2_def aux2); fprops); move: aux2;aw.
        by move=> [zbc _]; case: nab.
      by move=> [_ _].
    by move=> [zba _]; case: nab.
  by move=> [_ zbc _]; case: nbc.
have gp: forall t, inc t G -> inc (J t za) (f t).
  move=> t tG; move: (Gp1 _ tG); rewrite - sr -uX => /setU_P [y Jy yX].
  move: (fp1 _ (GF _ tG)) => [Jf1 fX].
  set z := Vf (inverse_fun (Lf f F X)) y.
  have zF: inc z F.
    have ->: F = target (inverse_fun (Lf f F X)) by aw.
     apply: Vf_target => //; [fct_tac | aw ].
  have: y = Vf (Lf f F X) z by rewrite inverse_V => //; aw.
  aw; move: (fp1 _ zF) => [p5 p6].
  move => yf; rewrite yf in Jy.
  have aux3: sub (f z) (substrate r) by rewrite -uX; apply: setU_s1.
  case: (equal_or_not z t) => zt; first by move: Jy; rewrite zt.
  move: (toeX _ p6) => [orX]; aw.
  move=> aux1; move: (aux1 _ _ Jy p5);case => leuv;move: (iorder_gle1 leuv);
    move /rvP => [qc qd]; case => aux2.
            by case: zt; move: (pr2_def aux2).
          by case: zt; move: aux2 => [_ _]; aw.
        case: nbc;move: aux2=> [_ e1 _]; move: e1;aw.
      by case: zt; move: (pr1_def aux2).
     by case: zt; move: aux2 => [_ _]; aw.
  by case: nac;move: aux2=> [_ e1 _]; move: e1;aw.
by exists h.
Qed.

We deduce that E46b_conc implies E46b_conc

Lemma Exercise4_6l E F A:
  finite_set F -> (forall x, inc x E -> sub (A x) F) ->
   E46b_conc E A -> E46b_hyp E F A.
Proof.
move=> pa pb pc.
apply: (Exercise4_6k (G := emptyset)) => //; first fprops.
move=> L LE.
have ->: L =emptyset.
   apply /set0_P; move=> y yL; case: (LE _ yL); case.
rewrite cardinal_set0.
apply: czero_least; fprops.
Qed.

TODO: show that E46c_hyp G holds. But we do not know what to do with assumption E46c_conc G

Exercise 4.7. In a lattice E, an element is said to be irreducible if it is never a strict supremum.
Let J be the set of irreducible elements; P the set J minus the least element (if it exists); S(x) be the set of irreducible elements that are <= x. We start with some auxiliary results. In particular, in a distributive lattice, if a is ireducible and a <= sup(x,y) then a<=x or a<=y.

Lemma char_fun_sub A A' B: sub A B -> sub A' B ->
  ((sub A A') <-> (forall x, inc x B ->
     (Vf (char_fun A B) x) <=c (Vf (char_fun A' B) x))).
Proof.
move=> AB A'B; split.
  move => AA' x xB; case: (inc_or_not x A) => xA.
    rewrite char_fun_V_a // char_fun_V_a //;[ fprops | by apply: AA'].
  rewrite char_fun_V_b //; last by apply /setC_P.
  by apply: czero_least; apply: char_fun_V_cardinal.
move=> h t tA; ex_middle ta'; move: (AB _ tA) => tB.
move: (h _ tB); rewrite char_fun_V_a // char_fun_V_b //; last by apply /setC_P.
move: card_lt_01 => h1 h2; co_tac.
Qed.

Definition sup_irred r x:=
  forall a b, inc a (substrate r) -> inc b (substrate r) ->
   x = sup r a b -> (x = a \/ x = b).

Definition irreds r := Zo (substrate r)(sup_irred r).

Definition E47S r x := Zo (substrate r)
   (fun z => (sup_irred r z) /\ (gle r z x)).

Section Irred_lattice.

Variable r:Set.
Hypothesis lr:lattice r.

Lemma Exercise4_7a x: inc x (substrate r) ->
 sup_irred r x \/ (exists a b, [/\ glt r a x, glt r b x & x = sup r a b]).
Proof.
case: (p_or_not_p (sup_irred r x)); first by left.
move=> p1; right; ex_middle h; case: p1 => a b asr bsr xs.
case: (equal_or_not x a)=> xa; first by left.
case: (equal_or_not x b)=> xb; first by right.
move: (lattice_sup_pr lr asr bsr); rewrite -xs; move => [p2 p3 _].
by case: h; exists a, b; rewrite /glt;split => //;split => //; apply: nesym.
Qed.

Lemma Exercise4_8a a: distributive_lattice3 r ->
  sup_irred r a ->
  forall x y, inc x (substrate r) -> inc y (substrate r) ->
   gle r a (sup r x y) -> (gle r a x \/ gle r a y).
Proof.
move => dl1 sia x y xsr ysr sa.
have or: order r by move: lr => [or _].
have asr: inc a (substrate r) by order_tac.
 move:(Exercise1_16b lr) => [_ _ p1]; move: ((p1 dl1) _ _ _ asr xsr ysr).
rewrite (inf_comparable1 or sa) => ia.
move: (lattice_inf_pr lr asr xsr)(lattice_inf_pr lr asr ysr).
move=> [_ px _] [_ py _].
have r1: inc (inf r a x) (substrate r) by order_tac.
have r2: inc (inf r a y) (substrate r) by order_tac.
by case: (sia _ _ r1 r2 ia); move=> ->; [left | right].
Qed.

If E is finite, any non-empty set has a minimal and a maximal element. In particular, E has a least element, which is irreducible. Any finite set has a supremum and an infimum. The supremum of S(x) is x. We restate this: any x is the supremum of a finite number of irreducible elements.

Hypothesis fs: finite_set (substrate r).
Hypothesis nes: nonempty (substrate r).

Definition E48P := (irreds r) -s1 (the_least r).

Lemma Exercise4_7b: order r.
Proof. by move: lr => [or _]. Qed.

Lemma finite_set_maximal1 U: sub U (substrate r) -> nonempty U ->
  exists2 x, inc x U & (forall y, inc y U -> gle r x y -> x = y).
Proof.
move: Exercise4_7b=> or Usr neU.
set r':= induced_order r U.
move: (iorder_osr or Usr) => [or' sr'].
move:(sub_finite_set Usr fs); rewrite - sr' => fsE.
rewrite - sr' in neU.
move: (finite_set_maximal or' fsE neU) => [x [xs xm]].
ex_tac; move=> y yser' xy; symmetry; apply: xm; apply /iorder_gleP => //; ue.
Qed.

Lemma finite_set_minimal1 U: sub U (substrate r) -> nonempty U ->
  exists2 x, inc x U & (forall y, inc y U -> gle r y x -> y = x).
Proof.
move: Exercise4_7b => or Usr neU.
set r':= opp_order (induced_order r U).
move: (iorder_osr or Usr) => [or1 sr1].
move: (opp_osr or1) => [or']; rewrite sr1 => sr'.
move:(sub_finite_set Usr fs); rewrite - sr' => fsE.
rewrite - sr' in neU.
move: (finite_set_maximal or' fsE neU) => [x [xs xm]].
ex_tac; move=> y yser' xy; apply: xm; apply /opp_gleP.
apply /iorder_gleP => //; ue.
Qed.

Lemma Exercise4_7c: exists a, least r a.
Proof.
move: (finite_set_minimal1 (@sub_refl (substrate r)) nes).
move=> [x xsr xp]; exists x;split => //.
move=> u usr; move: (lattice_inf_pr lr xsr usr); move=> [p1 p2 p3].
move: lr => [or _].
have isr:inc (inf r x u) (substrate r) by order_tac.
by move: (xp _ isr p1) => aux; rewrite aux in p2.
Qed.

Lemma Exercise4_7d: inc (the_least r) (irreds r).
Proof.
move: Exercise4_7b Exercise4_7c => or el.
move: (the_least_pr or el) => [p1 p2].
apply: Zo_i => //; case: (Exercise4_7a p1) => // aux.
move: aux => [a [_ [al _ _]]].
have asr: inc a (substrate r) by order_tac.
move: (p2 _ asr) => p3; order_tac.
Qed.

Lemma Exercise4_7e: sub E48P (substrate r).
Proof.
apply: (@sub_trans (irreds r));[ apply: sub_setC | apply: Zo_S].
Qed.

Lemma Exercise4_7f:
  irreds r = E48P +s1 (the_least r).
Proof. rewrite setC1_K //; apply: Exercise4_7d. Qed.

Lemma Exercise4_7g a: inc a (substrate r) ->
  inc (the_least r) (E47S r a).
Proof.
move: Exercise4_7b=> or asr.
move: (the_least_pr or (Exercise4_7c)) => [p1 p2].
apply: Zo_i => //;split;fprops.
by move: Exercise4_7d => /Zo_P [].
Qed.

Lemma Exercise4_7h a: inc a (substrate r) -> nonempty (E47S r a).
Proof. by exists (the_least r); apply: Exercise4_7g. Qed.

Lemma Exercise4_7i x: sub x (substrate r) ->
  has_supremum r x.
Proof.
move: Exercise4_7b => or xr; case: (emptyset_dichot x) => nex.
  move: (the_least_pr or Exercise4_7c) => tlp.
  rewrite nex; exists (the_least r).
  rewrite lub_set0 //.
by apply: (lattice_finite_sup2 lr (sub_finite_set xr fs) xr).
Qed.

Lemma Exercise4_7j a: inc a (substrate r) ->
  gle r (supremum r (E47S r a)) a.
Proof.
move => asr; move: (Exercise4_7h asr) => ne.
have sE: sub (E47S r a) (substrate r) by apply: Zo_S.
apply /(lattice_finite_sup3P lr _ (sub_finite_set sE fs) ne sE).
by move=> z /Zo_hi [].
Qed.

Lemma Exercise4_7k a b:
  gle r a b -> sub (E47S r a) (E47S r b).
Proof.
move: Exercise4_7b=> or ab t.
move /Zo_P => [p1 [p2 p3]]; apply /Zo_P; split => //; split => //;order_tac.
Qed.

Lemma Exercise4_7l u: inc u (substrate r) ->
  (supremum r (E47S r u)) = u.
Proof.
move: Exercise4_7b => or usr.
apply: (order_antisymmetry or); first by apply: Exercise4_7j.
ex_middle bad.
set U := Zo (substrate r) (fun z => ~ gle r z (supremum r (E47S r z))).
have neU:nonempty U by exists u; apply: Zo_i.
have su: sub U (substrate r) by apply: Zo_S.
move: (finite_set_minimal1 su neU) => [t tu tv].
move: (tu) => /Zo_P [tsr bad1]; case: bad1.
have sV: sub (E47S r t) (substrate r) by apply: Zo_S.
move: (Exercise4_7i sV) => hst.
move: (supremum_pr or sV hst) => [[ub1 ub2] _].
case: (Exercise4_7a (su _ tu)) => aux.
   have h: inc t (E47S r t) by apply: Zo_i => //;split => //; order_tac.
   by apply: ub2.
move: aux => [a [b [[leat neat] [lebt nebt ts]]]].
case: (p_or_not_p (gle r a (supremum r (E47S r a)))); last first.
  move=> p1;case: neat; apply: tv => //; apply: Zo_i => //; order_tac.
case: (p_or_not_p (gle r b (supremum r (E47S r b)))); last first.
  move=> p1;case: nebt; apply: tv => //; apply: Zo_i => //; order_tac.
move=> bs1 bs2.
have asr: inc a (substrate r) by order_tac.
have bsr: inc b (substrate r) by order_tac.
move: (Exercise4_7k leat) => s1.
move: (Exercise4_7k lebt) => s2.
move: (Exercise4_7i (sub_trans s1 sV)) => hs1.
move: (Exercise4_7i (sub_trans s2 sV)) => hs2.
move: (sup_increasing or (sub_trans s1 sV) sV s1 hs1 hst).
move: (sup_increasing or (sub_trans s2 sV) sV s2 hs2 hst).
move=> le1 le2.
move: (lattice_sup_pr lr asr bsr); rewrite -ts; move=> [h1 h2 h3].
apply: h3; order_tac.
Qed.

The function S is an order isomorphism E -> X for some subset X of the powerset of E order by inclusion. S of inf is intersection of S

Lemma Exercise4_7m a b:
  inc a (substrate r) -> inc b (substrate r) ->
  sub (E47S r a) (E47S r b) -> gle r a b.
Proof.
move => asr bsr sab.
set E := (E47S r a).
have sE: sub E (substrate r) by apply: Zo_S.
move: (sub_finite_set sE fs) => fsE.
rewrite - (Exercise4_7l asr).
apply /(lattice_finite_sup3P lr _ fsE (Exercise4_7h asr) sE).
by move=> z zE; move: (sab _ zE) =>/Zo_hi [_].
Qed.

Lemma Exercise4_7n a: inc a (substrate r) ->
  exists S, [/\ finite_set S, nonempty S, sub S (substrate r),
  (forall x, inc x S -> sup_irred r x) &
  supremum r S = a].
Proof.
move=> asr.
have sE: sub (E47S r a) (substrate r) by apply: Zo_S.
move: (sub_finite_set sE fs) => fsE.
move: (Exercise4_7h asr) (Exercise4_7l asr) => ne ass.
exists (E47S r a);split => //.
by move=> x /Zo_hi [].
Qed.

Lemma Exercise4_7o a b: inc a (substrate r) -> inc b (substrate r) ->
  (E47S r (inf r a b)) = (E47S r a) \cap (E47S r b).
Proof.
move=> asr bsr.
move: (lattice_inf_pr lr asr bsr)=> [p1 p2 p3].
have isr: inc (inf r a b) (substrate r) by order_tac.
move: (Exercise4_7k p1) (Exercise4_7k p2) => p4 p5.
set_extens t; first by move=> t1; apply /setI2_P; split; fprops.
move => /setI2_P [] /Zo_P [tsr [si ta]] /Zo_hi [_ tb]; apply /Zo_P;split;fprops.
Qed.

Lemma Exercise4_7p:
  let tg := (irreds r) in
   order_morphism (Lf (E47S r) (substrate r) (powerset tg))
   r (subp_order tg).
Proof.
move: lr => [or _] tg.
have ta: forall x, inc x (substrate r) -> inc (E47S r x) (powerset tg).
  by move=> x xsr; apply /setP_P => t /Zo_P [p1 [p2 p3]]; apply /Zo_P.
move: (subp_osr tg) => [pa pb].
split; fprops; rewrite ? pb;first by split; aw; apply: lf_function.
hnf; aw;move=> x y xsr ysr; red;aw; split.
   move => pa1; apply /sub_gleP;split;fprops.
   by apply: Exercise4_7k.
by move /sub_gleP => [pa1 [pb1 pc]]; apply:Exercise4_7m.
Qed.

Lemma Exercise4_7q a: inc a (substrate r)
 -> sub (E47S r a) (irreds r).
Proof. by move=> asr b => /Zo_P [pa [pb pc]]; apply /Zo_P. Qed.


Exercise 4.8. We assume that E is a distributive lattice.
We have: S of sup is union of S. If t is irreducible, U a non-empty set of irreducibles, t<= sup U simplies that t <= x for at least one element of U. Let p(U) be the property that U is a non-empty set of irreducibles, such that x <=y, x irreducible and y in U implies x in U. Then U = S(sup U). Moreover p (S(x)) holds for any x.

Hypothesis dl3: distributive_lattice3 r.

Lemma Exercise4_8b a b: inc a (substrate r) -> inc b (substrate r) ->
  (E47S r (sup r a b)) = (E47S r a) \cup (E47S r b).
Proof.
move=> asr bsr.
move: (lattice_sup_pr lr asr bsr)=> [p1 p2 p3].
have isr: inc (sup r a b) (substrate r) by order_tac.
have or: order r by move: lr => [ok _].
move: (Exercise4_7k p1) (Exercise4_7k p2) => p4 p5.
set_extens t; last first.
  case /setU2_P => /Zo_P [tsr [si ta]];
       apply /Zo_P;split => //; split => //; order_tac.
move /Zo_P=> [tsr [si ts]].
by case: (Exercise4_8a dl3 si asr bsr ts)=> le;
 apply /setU2_P;[left | right]; apply: Zo_i.
Qed.

Lemma Exercise4_8c1 t U: inc t (substrate r) ->
  sup_irred r t -> sub U (irreds r) -> gle r t (supremum r U) ->
  nonempty U -> exists2 x, inc x U & gle r t x.
Proof.
move: Exercise4_7b => or tsr sit Usi tsU neU.
pose pA U := sub U (irreds r) /\ gle r t (supremum r U).
pose pB U := exists2 x, inc x U & gle r t x.
have sis: sub (irreds r) (substrate r) by apply: Zo_S.
have Usr: sub U (substrate r) by apply: (@sub_trans (irreds r)).
move: (sub_finite_set Usr fs) => fsU.
apply: (@finite_set_induction2 pA pB U) => //.
  move => a; rewrite /pA /pB; move=> [p1 p2].
  have :inc a (irreds r) by apply: p1; fprops.
   move /Zo_P=> [asr ai]; move: p2.
   rewrite supremum_singleton // => ta; exists a;fprops.
move => a b aux nea; rewrite /pA /pB; move=> [p1 p2].
have air: sub a (irreds r).
  apply: (@sub_trans (a +s1 b)) => //; fprops.
have bir: inc b (irreds r) by apply: p1; fprops.
have asr: sub a (substrate r) by apply: (@sub_trans (irreds r)).
have bsr: inc b (substrate r) by apply: sis.
move: (sub_finite_set asr fs) => fsa.
have hsa: has_supremum r a by apply: lattice_finite_sup2 => //.
move: p2; rewrite supremum_setU1 // => aux2.
move: (supremum_pr1 or hsa) => /(lubP or asr) [[p2 p3] p4].
case: (Exercise4_8a dl3 sit p2 bsr aux2)=> aux3; last by exists b; fprops.
have aux4: pA a by split.
move: (aux aux4 nea); move=> [x xa tx]; exists x;fprops.
Qed.

Lemma Exercise4_8c U: sub U (irreds r) ->
   (forall x y, inc y U -> sup_irred r x -> gle r x y -> inc x U) ->
   nonempty U ->
  U = (E47S r (supremum r U)).
Proof.
move: Exercise4_7b => or Usi hU neU.
have sis: sub (irreds r) (substrate r) by apply: Zo_S.
have Usr: sub U (substrate r) by apply: (@sub_trans (irreds r)).
move: (sub_finite_set Usr fs) => fsU.
move: (lattice_finite_sup2 lr fsU Usr neU) => hs.
move: (supremum_pr or Usr hs) => [[ub1 ub2] ub3].
set_extens t => ts.
  move: (ub2 _ ts) (Usi _ ts) => aux /Zo_P [p1 p2].
  apply /Zo_P;split => //; by apply: Usr.
move: ts => /Zo_P [tsr [srt ltsr]].
move: (Exercise4_8c1 tsr srt Usi ltsr neU).
   move=> [x sU tx]; apply: (hU _ _ sU srt tx).
Qed.

Lemma Exercise4_8d:
  let p:= fun U => [/\ sub U (irreds r), nonempty U &
    (forall x y, inc y U -> sup_irred r x -> gle r x y -> inc x U)] in
  (forall x, inc x (substrate r) -> p (E47S r x)) /\
  (forall U, p U -> exists2 x, (inc x (substrate r)) & U = (E47S r x)).
Proof.
move: Exercise4_7b=> or p; split.
  move=> x xsr; split => //.
      move=> t /Zo_P [pa [pb pc]]; apply /Zo_P; split => //.
    by apply: Exercise4_7h.
  move=> u v /Zo_P [vsr [su vx]] iu uv.
  apply /Zo_P; split => //; try split => //;order_tac.
move=> U [p1 p2 p3]; rewrite (Exercise4_8c p1 p3 p2).
exists (supremum r U) => //.
have sU: sub U (substrate r).
  by move=> t tu; move: (p1 _ tu) => /Zo_P [].
by move: (supremum_pr1 or (Exercise4_7i sU)) => /(lubP or sU) [[ok _] _].
Qed.

Let Sb(x) be S(x) without the least element of E. These two sets have the same supremum. The previous result can be rewriten as Let q(U) be the property that U is a subset of P such that x <=y, x irreducible and y in U implies x in U. Then Sb(x) satisfies q and any set satisfying q has the form Sb(x).

Lemma Exercise4_8e:
  let comp:= fun X => X -s1 (the_least r) in
  let p:= fun U => (sub U E48P /\
    (forall x y, inc y U -> inc x E48P -> gle r x y -> inc x U)) in
  (forall x, inc x (substrate r) -> p (comp (E47S r x))) /\
  (forall U, p U -> exists2 x, (inc x (substrate r)) & U = comp (E47S r x)).
Proof.
move: Exercise4_7b Exercise4_8d => or [pa pb] comp p; split.
  move=> x xsr; move: (pa _ xsr) => [p1 p2 p3]; split.
    move => t /setC1_P [p4 p5]; apply /setC1_P;split;fprops.
  move=> z y => /setC1_P [yE yne] /setC1_P [zi znl] zy;apply/setC1_P;split=> //.
  move: zi => /Zo_P [_ zi]; apply: (p3 _ _ yE zi zy).
move=> U [p1 p2].
set U' := U +s1 (the_least r).
have [x xsr aux]:exists2 x, inc x (substrate r) & U' = E47S r x.
  apply: (pb U'); split => //.
      move=> t; case /setU1_P; last by move => ->; apply: Exercise4_7d.
      by move=> tu; move: (p1 _ tu) => /setC1_P [].
    by exists (the_least r); rewrite /U';fprops.
  move=> x y yU' ir xy; apply /setU1_P.
  have xsr: inc x (substrate r) by order_tac.
  case: (equal_or_not x (the_least r)); first by right.
  move => nxle; left.
  have xp: inc x E48P by apply /setC1_P;split => //; apply: Zo_i => //.
  move: yU' => /setU1_P; case.
    by move=> yU; move: (p2 _ _ yU xp xy).
    move: (the_least_pr or Exercise4_7c) => [_ tle].
  move=> h; rewrite h in xy; case: nxle; move: (tle _ xsr) => aux; order_tac.
ex_tac.
rewrite -aux; set_extens t.
   move => tu; apply /setC1_P; split => //; first by apply /setU1_P; left.
   by move: (p1 _ tu) => /setC1_P [].
move /setC1_P => [] /setU1_P; case => //.
Qed.

Let's consider the sets FJ and FP of increasing functions J->d and P->d, respectively, where the first set is J or P, ordered by the opposite ordering, and the second set is the doubleton (0,1) ordered by 0<1. These are ordered sets. To each x we associate the characteristic function of S(x) and Sb(x). This give an order isomorphism from E onto a subset of FJ and FP, because the conditions p and q considered above just say that the characteristic function is increasing.
Bourbaki says that the first mapping is bijective. This is wrong, because the constant function zero is never the characteristice function of S(x). We get a bijection be excluding this function. On the other hand the second mapping is bijective.

Definition E48I := doubleton \0