# Theory of Sets : Exercises sections 2 and 3

Copyright INRIA (2009-2013) Apics/Marelle Team (Jose Grimm).
Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset14 ssete1 ssete2.

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

Module Exercise3.

This property has a much shorter proof than the one given here
Lemma aleph_pr13 n: ordinalp n ->
\aleph (succ_o n) <c \2c ^c (\2c ^c (\aleph n)).
Proof.
move => on.
move: (OS_succ on) => son.
move: (CS_aleph son) => cas.
move: (CS_aleph on) => con.
move:(aleph_pr5c on) => icy.
have ->: \2c ^c \omega n = \2c ^c (coarse (\omega n)).
rewrite - {1} (square_of_infinite icy).
apply: cpow_pr; fprops; rewrite /coarse cprod2_pr1; fprops.
apply: (card_lt_leT (cantor cas)).
apply: (cpow_Meqle card2_nz); rewrite - card_setP.
rewrite - (aleph_succ_pr2 on).
apply: surjective_cardinal_le.
pose f X := Yo ((worder X) /\ cardinal (substrate X) = (\omega n))
(ordinal X) (\omega n).
set T := (aleph_succ_comp n).
have zT: inc (\omega n) T.
apply /setC_P; split; last by exact: (ordinal_irreflexive (proj1 con)).
by move: (ordinal_cardinal_lt (aleph_pr10c on)) => /ord_ltP0 [].
move: (OS_aleph son) => oas.
have ta: lf_axiom f (powerset (coarse (\omega n))) (aleph_succ_comp n).
move => t te; rewrite /f; Ytac h; last by exact.
move: h => [h1 h2].
move: (OS_ordinal h1) => oot.
case: (ord_le_to_el oas oot) => // le1.
move: (ordinal_cardinal_le1 le1); rewrite (cardinal_of_ordinal h1).
rewrite h2 (card_card cas) => le2.
move: (aleph_lt_ltc (ord_succ_lt on)) => le3; co_tac.
move /ord_ltP0: le1 => [_ _ lt1].
apply /setC_P; split => // le3.
have: (ordinal t) <o (\omega n) by apply /(ord_ltP (proj1 con)).
move /(ordinal_cardinal_le2P con oot).
by rewrite (cardinal_of_ordinal h1) h2; move => [_].
exists (Lf f (powerset (coarse (\omega n))) T);split; aw.
apply: lf_surjective => //.
move => x /(aleph_succ_P1 on) [pa pb].
have ox: ordinalp x by ord_tac.
have [g [bg sg tg]]: exists g, bijection_prop g x (\omega n).
rewrite -/(x \Eq \omega n); apply /card_eqP; rewrite (card_card con).
apply: card_leA.
move: pb.
move /(ordinal_cardinal_le2P cas ox); rewrite - (succ_c_pr on) => h.
exact:(succ_c_pr4 (proj1 icy) h).
by move: (ordinal_cardinal_le1 pa);rewrite (card_card con).
move: (ordinal_o_wor ox) => wox.
have pc: substrate (ordinal_o x) = source g by rewrite ordinal_o_sr.
move: (order_transportation bg (proj1 wox) pc).
move: (bg) => [[fg _] _].
set E := image_by_fun _ _; move => isg.
have pd: function (ext_to_prod g g) by apply: ext_to_prod_f.
have pe: sub (ordinal_o x) ((source g) \times (source g)).
rewrite -pc; apply: sub_graph_coarse_substrate; fprops.
have pf: sub (ordinal_o x) (source (ext_to_prod g g)).
rewrite /ext_to_prod; aw.
have pg: cardinal x = \omega n.
apply: card_leA.
move: pb.
move /(ordinal_cardinal_le2P cas ox); rewrite - (succ_c_pr on) => h.
exact: (succ_c_pr4 (proj1 icy) h).
by move: (ordinal_cardinal_le1 pa);rewrite (card_card con).
exists E.
apply /setP_P => t /(Vf_image_P pd pf) [u uo ->].
move: (pe _ uo) => up; rewrite (ext_to_prod_V2 fg fg up).
move: up => /setX_P [_ p1 p2]; apply /setXp_P;split => //; Wtac.
rewrite /f.
have es1: ordinal_o x \Is E by exists g.
move: (worder_invariance es1 wox) => woE.
have we: worder E /\ cardinal (substrate E) = \omega n.
move: isg => [p1 p2 [p3 p4 p5] p6].
rewrite - p5.
have <-: cardinal (source g) = cardinal (target g)
by apply /card_eqP; exists g.
by rewrite p4 (ordinal_o_sr x) pg.
by Ytac0; symmetry;apply: ordinal_o_isu2 => //; apply: orderIS.
Qed.

Exercise 2.1. The maximal elements for finer_order are total orders; any ordering is the intersection of all total orderings that extent it; an ordering is isomorphic to a subset of a product of total orders

Lemma induced_sub_pr1 r X x:
(forall a b, gle r a b -> sub a b) ->
upper_bound r X x -> sub (union X) x.
Proof.
move=> h [xs ub] t /setU_P [y ty yX].
by apply: (h _ _ (ub _ yX)).
Qed.

Lemma induced_sub_pr2 r X:
order r ->
(forall a b, inc a (substrate r) -> inc b (substrate r) ->
(gle r a b <-> sub a b)) ->
sub X (substrate r) -> inc (union X) (substrate r) ->
least_upper_bound r X (union X).
Proof.
move=> or rs Xsr Usr.
apply /(lubP or Xsr); split.
split => // y yx; rewrite rs //;[ by apply: setU_s1| by apply: Xsr].
move=> z zu; move: (zu)=> [zr zu1]; rewrite rs //.
apply: (induced_sub_pr1 (r:=r)) =>// a b ab; rewrite -rs //; order_tac.
Qed.

Lemma inc_coarse a b E: inc a E -> inc b E ->
inc (J a b) (coarse E).
Proof. move=> aE bE; apply /setXp_P; split => //. Qed.

Definition orders x :=
Zo (powerset (coarse x))(fun z => order_on z x).

Lemma ordersP x z:
inc z (orders x) <-> (order_on z x).
Proof.
split; [by move /Zo_hi | move => h; apply: Zo_i => //].
apply /setP_P; move: h => [or <-].
apply: sub_graph_coarse_substrate; fprops.
Qed.

Definition finer_order x :=
sub_order (orders x).

Lemma fo_osr x: order_on (finer_order x)(orders x).
Proof. apply: sub_osr. Qed.

Lemma fo_gleP x u v:
gle (finer_order x) u v <->
[/\ order u, order v, substrate u = x, substrate v = x & sub u v].
Proof.
split.
by move /sub_gleP => [] /ordersP [pa pb] /ordersP [pd pe] pf.
move => [pa pb pc pd pe].
by apply /sub_gleP;split => //; apply/ordersP.
Qed.

Lemma fo_gle1P x u v:
gle (finer_order x) u v <->
[/\ order u, order v, substrate u = x, substrate v = x &
forall a b, inc a x -> inc b x -> gle u a b -> gle v a b].
Proof.
split.
move /fo_gleP => [ou ov su sv h]; split => //.
by move=> a b ax bx ab; apply: h.
move => [ou ov su sv h]; apply /fo_gleP;split => //.
have gu: (sgraph u) by fprops.
move=> t tu.
have pt : (pairp t) by apply: gu.
move: tu; rewrite -pt => tu.
have p1: (inc (P t) x) by rewrite - su; substr_tac.
have p2: (inc (Q t) x) by rewrite - su; substr_tac.
by apply: (h _ _ p1 p2).
Qed.

Lemma Exercise2_1a r x y
(E := substrate r)
(r':= r \cup (Zo (coarse E)(fun z=> gle r (P z) x /\ gle r y (Q z)))):
order r -> inc x (substrate r) -> inc y (substrate r) ->
~ gle r y x ->
(gle (finer_order E) r r' /\ inc (J x y) r').
Proof.
move=> or xsr ysr h; split; last first.
apply: setU2_2; apply:Zo_i; first by apply:inc_coarse.
by aw; split => //; order_tac.
apply/fo_gleP.
have gr: sgraph r by fprops.
have gr': sgraph r'.
by move=> t /setU2_P; case; [ apply: gr | move => /Zo_P [] /setX_P []].
have sr1: forall a b, inc (J a b) r' -> (inc a E /\ inc b E).
move => a b; case /setU2_P; first by move => pr; rewrite /E; split;substr_tac.
move => /Zo_P [_]; aw;move => [pa pb]; split => //; rewrite /E; order_tac.
have sr': substrate r' = E.
set_extens t.
by move /(substrate_P gr');case; move => [z si]; case: (sr1 _ _ si).
move => tE.
suff: inc (J t t) r' by move => ha;substr_tac.
by apply /setU2_P; left; order_tac.
split => //; last by apply: subsetU2l.
split => //.
by move => a; rewrite sr' => aE; apply: setU2_1; order_tac.
move => a b c pa pb.
have ae: inc a E by rewrite - sr'; substr_tac.
have be: inc b E by rewrite - sr'; substr_tac.
have ce: inc c E by rewrite - sr'; substr_tac.
have jc: inc (J b c) (coarse E) by apply : inc_coarse.
case /setU2_P : pa=> pa.
case /setU2_P: pb => pb; first by apply /setU2_P; left; order_tac.
apply /setU2_P; right;apply /Zo_P; split; aw.
move /Zo_P: pb => [pb []]; aw; rewrite /gle/related => pc pd.
split => //;order_tac.
apply /setU2_P; right;apply /Zo_P; split;aw.
move /Zo_P: pa => [pa []]; aw; rewrite /gle/related => pc pd.
case /setU2_P: pb => pb; first by split => //; order_tac.
move /Zo_P: pb => [pb []]; aw; rewrite /gle/related => pe pf.
split => //; order_tac.
move => a b pa pb.
case /setU2_P : pa=> pa.
case /setU2_P: pb => pb; first by order_tac.
move /Zo_P: pb => [pb []]; aw => pc pd; case: h.
have ab:gle r a b by done.
have ax:gle r a x by order_tac.
order_tac.
move /Zo_P: pa => [pa []]; aw => qa qb.
case /setU2_P: pb => pb; case: h.
have ab:gle r b a by done.
have ax:gle r y a by order_tac.
order_tac.
move /Zo_P: pb => [pb []]; aw => pc pd; order_tac.
Qed.

Lemma Exercise2_1bP E a:
maximal (finer_order E) a <-> (total_order a /\ substrate a = E).
Proof.
rewrite /maximal (proj2 (fo_osr _)); split.
move=> [] /ordersP [oa sa] ha; split => //; split =>//.
move=> x y xsr ysr; case: (p_or_not_p (gle a y x)) => ngge; first by right.
left;move: (Exercise2_1a oa xsr ysr ngge).
by rewrite sa;move => [p1]; rewrite (ha _ p1).
move=> [[oa ta] sa]; split => //; first by apply /ordersP;split => //.
move=> x /fo_gle1P [_ ox _ sx sv].
symmetry; apply: order_exten => //.
move => u v; split => h //.
apply: sv =>//; rewrite - sa; order_tac.
have usr: inc u E by rewrite - sx; order_tac.
have vsr: inc v E by rewrite - sx; order_tac.
rewrite sa in ta; case: (ta _ _ usr vsr) => //.
move => uv; move: (sv _ _ vsr usr uv) => h'.
move: uv; have -> //: u = v by order_tac.
Qed.

Lemma fo_inductive E: inductive (finer_order E).
Proof.
move=> X; aw => XsE tX.
move:(fo_osr E) => [or sr].
case: (emptyset_dichot X) => xE.
exists (diagonal E); split.
rewrite sr;apply /ordersP; exact: (diagonal_osr E).
by rewrite xE => y /in_set0.
have pa: forall x, inc x X -> (order_on x E).
by move=> x xX; move: (XsE _ xX); rewrite sr => /ordersP.
move: xE => [w wX]; move: (pa _ wX) => [sw ow].
exists (union X).
set (r:=finer_order E) in *.
have op: (forall a b, inc a (substrate r) -> inc b (substrate r) ->
(gle r a b <-> sub a b)).
move=> x y xsr ysr; split; first by move /fo_gleP => [_ _ _ _].
move => sa; apply /fo_gleP.
by move: xsr ysr;rewrite sr => /ordersP[ra rb] /ordersP [rc rd].
have ug: (sgraph (union X)).
move=> y => /setU_P [z yz zX];move: (pa _ zX) => [oz _].
by apply: (order_sgraph oz).
have su: (substrate (union X) = E).
set_extens t.
move /(substrate_P ug); case; move=> [y] => /setU_P [z Jz zX];
move: (pa _ zX); move=> [oe <-]; substr_tac.
move => te.
have Jx: (inc (J t t) w) by order_tac; ue.
have jy: inc (J t t) (union X) by union_tac.
substr_tac.
move: tX => [orX]; aw => tX.
suff usr: (inc (union X) (substrate r)).
by move: (induced_sub_pr2 or op XsE usr) => /(lubP or XsE) [].
rewrite /r; rewrite sr; apply /ordersP;split => //.
split => //.
move => t; rewrite su => te; apply /setU_P; exists w => //; order_tac; ue.
move => y x z /setU_P [a Ja aX] /setU_P [b Jb bX].
move: (pa _ aX) (pa _ bX) => [sa oa] [sb ob].
move: (XsE _ aX) (XsE _ bX) => asr bsr.
case: (tX _ _ aX bX); move=> ab;move:(iorder_gle1 ab); rewrite op //.
move=> sab; apply/setU_P; exists b => //;move: (sab _ Ja)=> Jb';order_tac.
move=> sba; apply/setU_P;exists a=> //; move: (sba _ Jb)=> Ja';order_tac.
move => x y /setU_P [a Ja aX] /setU_P [b Jb bX].
move: (pa _ aX) (pa _ bX) => [sa oa] [sb ob].
have ia: inc a (substrate r) by apply: XsE.
have ib: inc b (substrate r) by apply: XsE.
case: (tX _ _ aX bX); move=> ab;move:(iorder_gle1 ab); rewrite op //.
by move=> sab; move: (sab _ Ja)=> Jb'; order_tac.
move=> sba; move: (sba _ Jb)=> Ja'; order_tac.
Qed.

Lemma order_total_extension r: order r ->
exists r', [/\ total_order r', substrate r' = substrate r & sub r r'].
Proof.
move=> or.
set (E:= substrate r); set (R:= finer_order E).
move: (fo_osr E) => [or1 sr1].
have rr: (inc r (substrate R)) by rewrite /R sr1; apply /ordersP.
move: (inductive_max_greater or1 (@fo_inductive E) rr) => [m].
move/ Exercise2_1bP => [tm sm] /fo_gleP [_ _ _ _ rm].
by exists m.
Qed.

Lemma Exercise2_1c r:
order r -> r = intersection (Zo (orders (substrate r))
(fun r' => total_order r' /\ sub r r')).
Proof.
move=> or; set bs:= Zo _ _.
move: (order_total_extension or) => [r' [tor' sr' sr]].
have rb': (inc r' bs). apply: Zo_i => //; apply /ordersP; split => //.
by move: tor'=> [or'_ ].
set_extens t.
move => tr;apply: setI_i;first by ex_tac.
by move=> y => /Zo_hi [_ ]; apply.
move=> tb; move: (setI_hi tb rb') => tr'.
move: tor'=> [or' tor'].
have pt: (pairp t) by apply: (order_sgraph or').
have tp: (t = J (P t) (Q t)) by aw.
rewrite tp in tr'.
have p1: (inc (P t) (substrate r)) by rewrite - sr'; substr_tac.
have p2: (inc (Q t) (substrate r)) by rewrite - sr'; substr_tac.
case: (p_or_not_p (gle r (P t) (Q t))); first by rewrite /gle/related -tp.
move=> grqp.
move:(Exercise2_1a or p2 p1 grqp)=> /=.
set r'':= union2 _ _.
move => [] /fo_gleP [_ or'' _ sr'' rr''] Jr''.
move: (order_total_extension or'')=> [r''' [tr''' sr''' srr]].
move: (tr''') => [o3 _].
have aux: (inc r''' bs).
apply: Zo_i; last by split => //;apply: sub_trans srr.
by apply /ordersP;split => //; transitivity (substrate r'').
move:(setI_hi tb aux) (srr _ Jr''); rewrite {1} tp => p3 p4.
have pq: (P t = Q t) by order_tac.
by rewrite tp pq;order_tac.
Qed.

Lemma Exercise2_1d r: order r -> exists g h,
[/\ order_fam g,
(allf g total_order) &
order_morphism h r (order_product g)].
Proof.
move=> or.
move: (Exercise2_1c or);set bs := Zo _ _; move => rp.
set (g:= Lg bs (fun z: Set => z)).
have poa: order_fam g.
rewrite /g;hnf; bw; move=> i id; bw.
by move: id; bw => /Zo_P [_ [[oi _] _]].
set (h := Lf (cst_graph bs)
(substrate r) (prod_of_substrates g)).
exists g, h; split => //.
by rewrite /g; hnf;bw; move=> i idg; bw; move: idg => /Zo_hi [].
move: (order_total_extension or) => [x [tox sx rx]].
move: (tox)=> [ox _].
have xb: (inc x bs) by apply: Zo_i=> //; apply /ordersP.
have ta: (lf_axiom (cst_graph bs) (substrate r) (prod_of_substrates g)).
move=> y ysr; apply /setXf_P; rewrite /cst_graph /g; bw;split;fprops.
move => j jb; bw.
by move: jb =>/Zo_P [] /ordersP [_ ->].
move: (order_product_osr poa) => [o1 s1].
rewrite /h; split => //.
by split;aw => //; apply: lf_function.
red;aw;move=> u v usr vsr; aw; split.
move => h1; apply /order_product_gleP;split;fprops.
rewrite /g /cst_graph; bw; move=> i idg; bw.
by move: idg => /Zo_hi [_ ]; apply.
move/order_product_gleP => [_ _]; rewrite /g/cst_graph; bw; move=> h1.
red;red;rewrite (Exercise2_1c or) -/bs; apply:setI_i; first by ex_tac.
move=> y yb; move: (h1 _ yb); bw.
Qed.

Exercise 2.2. Applying Zorn's lemma to some specific ordering says: in any ordered set, there is at least one well-orderec subset that has no strict upper bound

Lemma Exercise2_2a r
(B:= Zo (powerset (substrate r)) (fun z=> worder (induced_order r z)))
(sso := Zo (coarse B)(fun z=> segmentp (induced_order r (Q z)) (P z))):
order r ->
(order_on sso B /\ inductive sso).
Proof.
move=> or.
have HaP: forall x y, gle sso x y <->
[/\ inc x B, inc y B & segmentp (induced_order r y) x].
move=> x y; split; first by move => /Zo_P [] /setXp_P []; aw.
move => [pa pb pc]; apply /Zo_P;split => //; [ by apply /setXp_P | aw ].
have Hb: sgraph sso by move=> t => /Zo_P [] /setX_P [].
have Hc: forall x y, gle sso x y -> sub x y.
move=> x y => /HaP [_ ] /Zo_P [] /setP_P ysr _; case; aw.
have Hf: forall x, inc x B -> sub x (substrate r).
by move=> x => /Zo_P [ ] /setP_P.
have Hd: forall x, inc x B -> gle sso x x.
move=> x xB; apply /HaP; split => //;split; first by aw; fprops.
by move=> a b ax aux; case: (iorder_gle3 aux).
have He:substrate sso = B.
set_extens t.
by move /(substrate_P Hb); case; move=> [y] =>/Zo_P [] /setXp_P [].
move=> tB; move: (Hd _ tB) ;rewrite /gle=> Js ; substr_tac.
have os: order sso.
split => //.
move => t; rewrite He; apply: Hd.
move => y x z => /HaP [xB yB [xs p1]] /HaP [_ zB [ys p2]].
apply /HaP;split => //; move: (Hf _ xB)(Hf _ yB)(Hf _ zB) => xs1 ys1 zs1.
move: xs ys; aw => xs ys.
split; first by aw ; apply: (@sub_trans y).
move=> a b ax p3; move: (iorder_gle1 p3) (iorder_gle3 p3)=> ba [bz az].
apply: (p1 _ _ ax); apply /iorder_gleP => //; last by apply: xs.
apply: (p2 _ _ (xs _ ax)); aw.
by move => // x y r1 r2; apply: extensionality; apply: Hc.
split => //.
red;rewrite He => X XE toi.
have su: (sub (union X) (substrate r)).
move=> t /setU_P [y ty yX]; exact: (Hf _ (XE _ yX)).
move: (iorder_osr or su) => [o1 sr1].
have woi: worder (induced_order r (union X)).
split => //; rewrite sr1.
move => x xu [a ax];move: (xu _ ax) => /setU_P [b ab bX].
set (Z := x \cap b).
have neZ:(nonempty Z) by exists a; apply: setI2_i.
move: (XE _ bX) => /Zo_P [] /setP_P bsr [wo1 ]; aw =>wo2.
have p1: (sub Z b) by apply: subsetI2r.
move: (wo2 _ p1 neZ) => [y]; aw; rewrite iorder_trans //.
have Z1: (sub Z (substrate r)) by apply: (sub_trans p1).
have xr: sub x (substrate r) by apply: sub_trans su.
rewrite iorder_trans //; move=> []; aw; move=> yZ yp.
have yx: (inc y x) by apply: (@setI2_1 x b).
exists y; red;aw; split => //.
move => z zx; aw.
move: (xu _ zx) => /setU_P [t zt tX].
move: toi => [toi1]; aw; last by ue.
move=> aux; move: (aux _ _ tX bX).
case => h1; move:(iorder_gle1 h1) => h2;move: (Hc _ _ h2) => h3.
have zZ: inc z Z by apply: setI2_i => //; apply: h3.
apply /iorder_gleP => //.
by move: (yp _ zZ) => h4; move: (iorder_gle1 h4).
have yb: inc y b by apply: p1.
have yt: inc y t by apply: h3.
move :(XE _ tX) => /Zo_P [xx wor].
have st: sub t (substrate r) by move: xx => /setP_P.
move: (worder_total wor) => [_ ]; aw => tor.
apply /iorder_gleP => //.
case: (tor _ _ yt zt); move=> h4; move: (iorder_gle1 h4) => //.
move: h2 => /HaP [_ _ [_ se]].
move: (se _ _ yb h4) => zb.
have zZ: inc z Z by apply: setI2_i => //; apply: h3.
by move: (yp _ zZ) => h5; move: (iorder_gle1 h5).
have uXb:inc (union X) B by apply: Zo_i => //; apply /setP_P.
exists (union X); split; first by rewrite He.
move => y yX; apply /HaP;split;fprops.
split; first by aw; apply: setU_s1 => //.
move=> u v uy uv; move: (iorder_gle1 uv) => vu.
move:(iorder_gle3 uv)=> [vU uU].
move: vU => /setU_P [w uw wX].
move:toi => [_ ]; aw; last by ue.
move=> h; move: (h _ _ yX wX).
case => h1; move: (iorder_gle1 h1) => aux; move: (Hc _ _ aux); last by apply.
move: aux => /HaP [yB wB [s1 s2]] yw.
apply: (s2 _ _ uy); apply /iorder_gleP=> //; apply: yw; fprops.
Qed.

Lemma Exercise2_2b r: order r ->
exists x, [/\ sub x (substrate r), worder (induced_order r x) &
forall z, upper_bound r x z -> inc z x].
Proof.
move=> or; move: (Exercise2_2a or).
set B:= Zo (powerset _) _.
set ss_order := Zo _ _.
move => [[sso sss] iss].
move: (Zorn_lemma sso iss)=> [a [ais am]].
move:(ais); rewrite sss => /Zo_P [] /setP_P asr woia.
exists a; split => //.
move=> z [zsr zu].
set (y:= a +s1 z).
have zy: inc z y by rewrite /y;fprops.
rewrite -(am y) //.
have ysr: (sub y (substrate r)).
move=> t /setU1_P; case ; [apply: asr| by move => ->].
apply: Zo_i.
move: (iorder_osr or ysr) => [pr1 sr1].
apply /setXp_P;split => //;first (by ue); apply: Zo_i;first by apply /setP_P.
split => //; rewrite sr1 => x xy nex.
set (t:= x \cap a).
have Ha: sub t a by apply: subsetI2r.
have Hb: sub t y.
by apply: (@sub_trans x) => //; apply: subsetI2l.
have Hc: sub t (substrate r) by apply: (@sub_trans y).
have Hd: sub x (substrate r) by apply: (@sub_trans y).
rewrite iorder_trans //.
case: (emptyset_dichot t) => te.
have xs: (forall u, inc u x -> u = z).
move=> u ux; move: (xy _ ux); case /setU1_P => //.
by move=> ua; empty_tac1 u; apply: setI2_i.
move: nex => [w wx]; move: (xs _ wx) => wz.
exists w; red; aw;split => //.
move => // v vx; apply /iorder_gle5P;split => //; rewrite (xs _ vx) - wz.
by order_tac; apply: Hd.
move: woia => [_]; aw; move=> h; move: (h _ Ha te) => [w].
rewrite iorder_trans //; move=> []; aw;move=> ws wl;exists w.
have wx: inc w x by apply: (@setI2_1 x a).
red; aw;split => //; move=> v vx; apply /iorder_gleP=> //.
move: (xy _ vx); case /setU1_P => //.
move=> va; exact: (iorder_gle1 (wl _ (setI2_i vx va))).
move => ->; exact: (zu _ (Ha _ ws)).
aw.
split; first by aw; move=> t; rewrite /y; fprops.
move=> u v xa h; move: (iorder_gle3 h)(iorder_gle1 h) => [vy uy] vu.
move: vy; case /setU2_P => // /set1_P vz.
move: (zu _ xa); rewrite -vz => uz.
by rewrite (order_antisymmetry or vu uz).
Qed.

Exercise 2.3. Any set can be partitioned into a well-ordered set and a set that has no least element; We give an example where there are many solutions

Lemma complement_p1 C A B:
A \cup B = C -> A \cap B = emptyset ->
(sub A C /\ A = C -s B).
Proof.
move => uab iab.
have sa: sub A C by move=> t tA; rewrite -uab; fprops.
have sb: sub B C by move=> t tB; rewrite -uab; fprops.
split => //; set_extens t.
move=> tA; apply /setC_P;split => //; first by apply: sa.
by move=> tB; empty_tac1 t; apply: setI2_i.
rewrite - uab; move /setC_P => [tc tb]; case /setU2_P: tc => //.
Qed.

Lemma complement_p2 C A B:
A \cup B = C -> A \cap B = emptyset ->
(sub B C /\ B = C -s A).
Proof. rewrite setI2_C setU2_C; apply: complement_p1. Qed.

Lemma complement_p3 C B (A:= C -s B):
sub B C -> (A \cup B = C /\ A \cap B = emptyset).
Proof.
move=> BC; rewrite /A;split.
set_extens t.
case /setU2_P; [ by move => /setC_P [] | apply: BC ].
move => tC; case: (inc_or_not t B) => tB; apply /setU2_P ; [right | left] =>//.
by apply /setC_P.
by apply /set0_P => y /setI2_P [] /setC_P [].
Qed.

Lemma complement_p4 C A (B:= C -s A):
sub A C -> (A \cup B = C /\ A \cap B = emptyset).
Proof. rewrite setI2_C setU2_C; apply: complement_p3. Qed.

Lemma Bnat_greatest A: sub A Bnat -> nonempty A ->
(exists x, upper_bound Bnat_order A x) ->
(exists x, greatest (induced_order Bnat_order A) x).
Proof.
move=> AB [t tA] [w wb].
move:Bnat_order_wor => [[or wo] sr].
have sA:sub A (substrate Bnat_order) by ue.
set pr:= upper_bound Bnat_order A.
have p1: (forall x, pr x -> inc x Bnat).
by move=> x; rewrite /pr /upper_bound sr; case.
case: (p_or_not_p (pr \0c)) => p2.
move: p2; rewrite /pr /upper_bound sr; move=> [zb p3].
move: (p3 _ tA) =>/ Bnat_order_leP [_ _ pt].
rewrite (card_le0 pt) in tA.
exists \0c; red; aw;split => //.
by move=> x xA; apply /iorder_gleP=> //; apply: p3.
have p3: (exists x, pr x) by exists w.
move: (least_int_prop1 p1 p2 p3) => [x [xB [sxB prs nprx]]].
have sxA: inc (succ x) A.
ex_middle sxA; case: nprx; split; first (by ue); move=> y yA.
move: (prs _ yA) => /Bnat_order_leP [yB _ ysc].
have : y <c (succ x) by split =>//; dneg ys; ue.
move /(card_lt_succ_leP xB) => h; apply /Bnat_order_leP;split => //.
exists (succ x); red; aw;split => //.
by move => z zA; apply /iorder_gleP => //; apply: prs.
Qed.

Definition ex23_prop r A B:=
[/\ A \cup B = substrate r, A \cap B = emptyset,
worder (induced_order r A) &
(forall y, ~ (least (induced_order r B) y))].

Lemma Exercise2_3a r: order r -> exists A B, ex23_prop r A B.
Proof.
move=> or.
pose no_least B := forall y, ~ least (induced_order r B) y.
set (B:= union (Zo (powerset (substrate r)) no_least)).
have Bsr: (sub B (substrate r)).
by move=> t /setU_P [y ty] /Zo_P [] /setP_P=> [h _]; apply: h.
move: (complement_p3 Bsr); set A := complement _ _.
move=> [p1 p2].
exists A, B; split => //.
have AE: (sub A (substrate r)) by apply: sub_setC.
move: (iorder_osr or AE) => [or1 sr1].
split => //; rewrite sr1.
move=> x xA nex; rewrite iorder_trans //; ex_middle h.
have xB: (sub x B).
move=> t tx; apply: (@setU_i _ x) => //; apply: Zo_i.
by apply /setP_P; apply: (@sub_trans A).
by move=> y nle; case: h; exists y.
move: nex => [y yx];move: (xB _ yx); empty_tac1 y.
move=> y; rewrite /least;aw.
move => [] /setU_P [t yt aux] h; move: (aux) => /Zo_P [] /setP_P.
move=> tr nl; case: (nl y); red; aw;split => //.
move=> x xt; apply /iorder_gleP => //.
aw; exact: (iorder_gle1 (h _ (setU_i xt aux))).
Qed.

Lemma Exercise2_3b n (r := opp_order Bnat_order)
(A := Bint n) (B:= Bnat -s A) :
inc n Bnat -> (order r /\ ex23_prop r A B).
Proof.
move=> nB.
move: Bnat_order_wor => [[o1 _] s1].
move: (opp_osr o1)=> [or]; rewrite s1 => sr.
have sAC: sub A (substrate r) by rewrite sr; apply: Bint_S1.
move: (iorder_osr or sAC) => [or1 sr1].
move: (complement_p4 sAC) => [p1 p2].
split => //; split => //.
- by rewrite /B - sr.
- by rewrite /B - sr.
- split => //; rewrite sr1.
move=> x xA nex; rewrite iorder_trans//.
rewrite sr in sAC; move: (@sub_trans _ _ _ xA sAC) => sxB.
have p3: (exists n, upper_bound Bnat_order x n).
have aux: upper_bound Bnat_order A n.
split; [ue | move=> y; rewrite /A]; move /(BintP nB).
move=> [yn _] ; apply /Bnat_order_leP;split => //.
apply: (BS_le_int yn nB).
move: (sub_upper_bound aux xA) => p3.
by exists n.
move: (Bnat_greatest sxB nex p3) => [y yg]; exists y.
have s2: sub x (substrate Bnat_order) by ue.
have s3: sub x (substrate r) by ue.
move: yg; rewrite /greatest /least; aw.
move=> [yx h]; split => //;move=> z zx; move: (h _ zx).
by move /(iorder_gleP _ zx yx) /opp_gleP => ha; apply /iorder_gleP.
- have bsr: sub B (substrate r) by rewrite sr; apply: sub_setC.
move=> y; rewrite /least; aw.
move=> [yb etc].
move: (yb) => /setC_P [yB] /(BintP nB) nyn.
move: (card_lt_succ yB) => [le2 ne1].
have ysB: inc (succ y) B.
apply /setC_P;split;fprops => /(BintP nB) le1; case: nyn;co_tac.
move: (iorder_gle1 (etc _ ysB)) => /opp_gleP /Bnat_order_leP [_ _ le3].
case: ne1; co_tac.
Qed.

Lemma Exercise2_3c
(r := diagonal (tripleton \0c \1c \2c))
(A1:= emptyset) (A2:= singleton \0c):
[/\ order r,
(ex23_prop r A1 ((substrate r) -s A1)) &
(ex23_prop r A2 ((substrate r) -s A2)) ].
Proof.
set E := (tripleton \0c \1c \2c).
move: (diagonal_osr E) => []; rewrite /E -/r.
move => or sr; rewrite sr.
have pa: forall A, sub A (substrate r) ->
(order_on (induced_order r A) A).
by move => A Ai; apply: iorder_osr.
have tws: inc \2c (substrate r) by rewrite sr; apply /set3_P; in_TP4.
have os: inc \1c (substrate r) by rewrite sr; apply /set3_P; in_TP4.
have nc: gle r \1c \2c -> False.
move /diagonal_pi_P => [_ bad]; by case: card_12.
split; first by exact.
have s1: sub A1 (substrate r) by rewrite /A1; fprops.
move: (complement_p4 s1) => [ta tb].
move: (pa _ s1) => [tc td]; rewrite - sr; split => //.
rewrite {2} /A1 in td.
rewrite (empty_substrate_zero td); exact (proj1 set0_wor).
have ->: (substrate r -s A1) = substrate r.
set_extens t; first by move => /setC_P [].
move => ts; apply /setC_P;split => //; case; case.
rewrite (iorder_substrate or); move => y [ysr yl].
case: (equal_or_not y \1c) => y1.
by move: (yl _ tws); rewrite y1.
by move: (yl _ os) => /diagonal_pi_P [_ bad].
have s1: sub A2 (substrate r).
rewrite /A2 sr;move => t /set1_P ->; apply /set3_P; in_TP4.
move: (complement_p4 s1) => [ta tb].
move: (pa _ s1) => [tc td]; rewrite - sr; split => //.
rewrite {2} /A2 in td; exact: (worder_set1 (conj tc td)).
have ->: (substrate r -s A2) = doubleton \1c \2c.
rewrite sr /A2; set_extens t.
move /setC_P => []; case /set3_P; first by move => t1 /set1_P.
move => h _; apply /set2_P; fprops.
move => h _; apply /set2_P; fprops.
case /set2_P => ->; apply /setC_P; split; try (apply /set3_P => // ;in_TP4).
move => /set1_P; apply: card1_nz.
move => /set1_P; apply: card2_nz.
have sd: sub (doubleton \1c \2c) (substrate r).
by move => t; case /set2_P => ->.
move => y []; rewrite (iorder_sr or sd) => [te tf].
case: (equal_or_not y \1c) => y1.
by move: (iorder_gle1 (tf _ (set2_2 \1c \2c)));rewrite y1.
move: (iorder_gle1 (tf _ (set2_1 \1c \2c))).
by move /diagonal_pi_P => [_ bad].
Qed.

Exercise 2.4: we say that F is partially well-ordered if every totally ordered subset is well-ordered. In any ordered set, there is a cofinal partially well-ordered set

Lemma Exercise2_4 r
(pworder := fun F => forall X,
sub X F -> total_order (induced_order r X) -> worder (induced_order r X)):
order r -> exists2 F, pworder F & cofinal r F.
Proof.
move=> or.
set (FF:= Zo (powerset (substrate r)) pworder).
pose f x y := forall a b, inc a x ->
inc b (y -s x) -> ~ gle r b a.
set (r' := graph_on (fun x y => sub x y /\ f x y) FF).
have r'P: forall x y, gle r' x y <-> [/\ inc x FF, inc y FF, sub x y & f x y].
move=> x y; split; first by move /Zo_P => [] /setXp_P[xf yf][];aw.
move => [pa pb pc pd]; apply /Zo_P;split => //; aw; last by split.
by apply /setXp_P.
have HpP: forall F, sub F (substrate r) -> (pworder F <->
(forall X, sub X F -> nonempty X -> total_order (induced_order r X)
-> exists y, least (induced_order r X) y)).
move => G Fsr;split.
move=> pwog X XG neX toX; move: (pwog _ XG toX)=> [_].
move: (sub_trans XG Fsr) => Xsr.
rewrite iorder_sr // => wor.
move: (@sub_refl X) => XX.
move: (wor _ XX neX); rewrite iorder_trans //.
move=> h X XG torX; move: (torX) =>[orX _].
move: (sub_trans XG Fsr) => Xsr.
split; fprops; aw; move=> x xX neX.
set r'':= (induced_order (induced_order r X) x).
have aux: r'' = induced_order r x by rewrite /r'' iorder_trans.
rewrite aux; apply: h => //.
by apply: sub_trans XG.
rewrite -aux;apply: total_order_sub => //; aw.
have Hf: forall x F, inc x (substrate r) -> inc F FF ->
inc (F +s1 x) FF.
move=> x F xsr =>/Zo_P [] /setP_P Fsr pwf.
have stF: (sub (F +s1 x) (substrate r)).
move=> t /setU1_P; case; [apply: Fsr | by move => ->].
apply: Zo_i; first by apply /setP_P.
apply/ (HpP _ stF) => X Xt neX toX.
move: pwf => /(HpP _ Fsr) => pwf.
case: (inc_or_not x X) => tX; last first.
apply: pwf =>// w wX; move: (Xt _ wX); case /setU1_P => // wx; case: tX; ue.
move: (sub_trans Xt stF) => Xsr.
case: (equal_or_not X (singleton x)) => eq.
exists x; split; aw; move=> t;rewrite eq => /set1_P ->.
apply /iorder_gleP;fprops;order_tac.
apply: Xsr; rewrite eq; fprops.
set (Y := X \cap F).
have sYF: (sub Y F) by apply: subsetI2r.
have sYX: (sub Y X) by apply: subsetI2l.
move: (sub_trans sYF Fsr) => Ysr.
case: (emptyset_dichot Y) => Ye.
case: eq; set_extens t; last by move /set1_P ->.
move => tx; move: (Xt _ tx); case /setU1_P; last by move => ->; fprops.
by move => tf; empty_tac1 t; apply /setI2_P.
have tos: (total_order (induced_order r Y)).
have ->: (induced_order r Y) = (induced_order (induced_order r X) Y).
by rewrite iorder_trans.
apply: total_order_sub => //; aw.
move: (pwf _ sYF Ye tos) => [y []]; aw => yY yl.
move: (total_order_lattice toX) => lX.
move: (sYX _ yY) => yX.
have xsX: inc x (substrate (induced_order r X)) by aw.
have ysX: inc y (substrate (induced_order r X)) by aw.
move: (lattice_inf_pr lX xsX ysX).
set z := (inf (induced_order r X) x y).
move=> [p1 p2 p3]; exists z;red; aw.
move: (iorder_gle3 p1)(iorder_gle1 p1) (iorder_gle1 p2) => [zX _] zx zy.
split => // w wx; apply /iorder_gleP => //.
move: (Xt _ wx); case /setU1_P => ezx; last by ue.
have wY: inc w Y by apply: setI2_i.
by move:(yl _ wY) => wy; move: (iorder_gle1 wy) => p4; order_tac.
have or' :(order r').
apply: order_from_rel;split => //.
move=> y x z [xy fxy] [yz fyz]; split => //;first by apply: sub_trans yz.
move=> a b ax /setC_P [bz nbx].
case: (inc_or_not b y) => iby; first by apply: fxy =>//; apply /setC_P.
apply: fyz =>//; [by apply: xy | apply /setC_P; split => // ].
by move=> x y [xy _] [yx _ ]; apply: extensionality.
by move=> x y _; split => //; split => // a b ax => /setC_P; case.
have sr': substrate r' = FF.
by apply: graph_on_sr=> x xp; split => //; move=> a b ax => /setC_P [].
have isr': inductive r'.
move=> X Xsr []; aw => orX' tor'.
have tor'': forall x y, inc x X -> inc y X ->
((sub x y /\ f x y) \/ (sub y x /\ f y x)).
move=> x y xX yX.
case: (tor' _ _ xX yX) =>h; move: (iorder_gle1 h) => /r'P.
move=> [_ _ xy fxy]; left; split => //.
move=> [_ _ xy fxy]; right; split => //.
have su: sub (union X) (substrate r).
move=> t /setU_P [y ty yX]; move: (Xsr _ yX); rewrite sr' => /Zo_P [].
by move=> /setP_P ysr _; apply: ysr.
have uxf: (inc (union X) FF).
apply: Zo_i => //; first by apply /setP_P => //.
move => t tu tort; move: (sub_trans tu su) => tsr.
move: (iorder_osr or tsr) => [or1 sr1].
split => //; rewrite sr1 => x xt [u ux]; rewrite iorder_trans //.
move: (tu _ (xt _ ux)) => /setU_P [i ui iX].
set (K:=x \cap i).
move: (Xsr _ iX); rewrite sr' => /Zo_P [isr pwoi].
have K1: (sub K i) by apply: subsetI2r.
move: (sub_trans xt tsr) => xsr.
have K2: (sub K t).
apply: sub_trans xt; apply: subsetI2l.
move: (sub_trans K2 tsr) => K3.
have to3:(total_order (induced_order r K)).
have ->: (induced_order r K) = (induced_order (induced_order r t) K).
by rewrite iorder_trans.
apply: total_order_sub => //; aw.
have neK: nonempty K by exists u; apply /setI2_P.
move:isr pwoi => /setP_P isr => / (HpP _ isr) pwoi.
move: (pwoi _ K1 neK to3).
move=> [y []]; aw => yK ylK.
have yx: inc y x by apply: (setI2_1 yK).
exists y; split; aw.
move=> v vx; move: (tu _ (xt _ vx)) => /setU_P [w vw wX].
apply /iorder_gleP => //.
case: (inc_or_not v i) => vi.
have wK: (inc v K) by apply: setI2_i.
move: (ylK _ wK) => ge1; apply: (iorder_gle1 ge1).
case: (tor'' _ _ wX iX); first by move=> [wi _]; case: vi; apply: wi.
move=> [i3 fiw].
have vc: inc v (w -s i) by fprops.
move: (fiw _ _ (K1 _ yK) vc) => r1.
move: (xt _ yx) (xt _ vx) => yt vt.
move: tort => [_ ]; aw => tor1.
case: (tor1 _ _ yt vt) => h; move: (iorder_gle1 h) => //.
exists (union X); split; first by ue.
move=> y yX; apply /r'P; split => //.
by rewrite - sr'; apply: Xsr.
by apply: setU_s1.
move=> a b ay => /setC_P [bu iby]; move: bu => /setU_P [z bz zX].
case: (tor'' _ _ zX yX); first by move=> [yz _]; case: iby; apply: yz.
move=> [yz fyz]; apply: fyz => //; apply /setC_P;split => //.
move: (Zorn_lemma or' isr') => [a []]; rewrite sr' => aFF h.
move: (aFF) => /Zo_P [] /setP_P asr pwoan; exists a => //.
split => // x xsr.
case: (inc_or_not x a)=> xa; first by ex_tac;order_tac.
ex_middle aux;case: xa.
suff rat: (gle r' a (a +s1 x)) by rewrite -(h _ rat); fprops.
have pa: sub a (a +s1 x) by fprops.
apply /r'P; split => //; first by apply: Hf => //.
move => t s ta /setC_P [] /setU1_P; case => //.
by move => -> _ ha; case: aux; exists t.
Qed.

Exercise 2.5: in an inductive set, there is a greatest free subset
Lemma Exercise2_5 r: order r -> inductive r ->
exists x, greatest (free_subset_order r) x.
Proof.
move=> or isr;set (A:= Zo (substrate r) (maximal r)).
have fs: (free_subset r A).
by move => x y => /Zo_hi [_ xm] _ xy; rewrite (xm _ xy).
have Af:(inc A (free_subsets r))
by apply: Zo_i => //; apply /setP_P; apply: Zo_S.
move: (fs_order_osr or) => [fso fsr].
exists A; split; first by ue.
rewrite fsr => x xs; apply /fs_order_gleP; split => //.
move=> y yx.
move:xs =>/Zo_P [] /setP_P xsr _.
move: (inductive_max_greater or isr (xsr _ yx)) => [m [mm ym]].
exists m => //; apply: Zo_i => //; order_tac.
Qed.

Exercise 2.6
We start with two auxiliary lemmas. In a well-ordered set, if a has a strict upper bound, there is a successor b; this means that x<=a and x<b are equivalent. The emptyset is an initial segment (with end-point the least element

Lemma Exercise2_6g r a (m := Zo (substrate r) (fun z => glt r a z)) :
worder r -> inc a (substrate r) ->
nonempty m -> exists2 b,
inc b (substrate r) & (segmentc r a = segment r b).
Proof.
move=> wor asr nem.
move: (worder_total wor) => tor.
have sms: (sub m (substrate r)) by apply: Zo_S.
move: wor => [or wor1]; move: (wor1 _ sms nem) => [y[]]; aw => ym yl.
move: (sms _ ym) => ysr; ex_tac.
move: (ym)=> /Zo_hi ya.
set_extens t; first by move /segmentcP => ta; apply /segmentP; order_tac.
move /segmentP => ta; apply /segmentcP.
have tsr: inc t (substrate r) by order_tac.
case: (total_order_pr2 tor asr tsr) => // lat.
have tm: inc t m by apply: Zo_i.
move: (iorder_gle1 (yl _ tm)) => h'; order_tac.
Qed.

Lemma worder_has_empty_seg r: worder r ->
nonempty (substrate r) -> exists2 x,
inc x (substrate r) & segment r x = emptyset.
Proof.
move=> [or wor] nes.
move: (wor _ (@sub_refl (substrate r)) nes) => [x].
rewrite iorder_substrate //.
move=> [xsr xle]; exists x => //; apply /set0_P.
move => y ys;move: (inc_segment ys) => lt1.
have ysr: inc y (substrate r) by order_tac.
move: (xle _ ysr) => le1; order_tac.
Qed.

We assume that f:E->E is defined on an ordered set and f(x) >=x. Let bigS be the set of all M stable by f, such that any non-empty subset N of M that has a least upper bound x is such that x belongs to M. The chain of a is the intersection of all elements of M that contain a
Section Exercise2_6.
Variables r f : Set.

Definition bigS :=
Zo (powerset (substrate r))
(fun M => (forall x, inc x M -> inc (Vf f x) M) /\
(forall N x, sub N M -> nonempty N -> least_upper_bound r N x -> inc x M)).

Definition chainx a := intersection (Zo bigS (inc a)).

Hypothesis or: order r.
Hypothesis ff: function f.
Hypothesis sf: substrate r = source f.
Hypothesis tf: substrate r = target f.
Hypothesis fxx: forall x, inc x (substrate r) -> gle r x (Vf f x).

Bourbaki says "Deduce from (a) that if E is inductive, then f has a fix-point". But this is trivial

Lemma Exercise2_6i: inductive r ->
exists2 a, inc a (source f) & Vf f a = a.
Proof.
move => ir; move: (Zorn_lemma or ir) => [a [asr am]].
rewrite - sf;exists a;fprops.
Qed.

We show: if the chain of a has a least upper bound, it is in the chain and is a fix-point of f
Lemma Exercise2_6a: inc (substrate r) bigS.
Proof.
apply: Zo_i; aw; first by apply /setP_P; fprops.
split.
move => x xsr; move: (fxx xsr) => h; order_tac.
by move=> N x Nsr [y yN] /(lubP or Nsr) [[p1 _] _].
Qed.

Lemma Exercise2_6b a:
inc a (source f) -> nonempty (Zo bigS (inc a)).
Proof.
move=> asf;exists (substrate r); apply: Zo_i;[ apply: Exercise2_6a| ue].
Qed.

Lemma Exercise2_6c a: inc a (source f) -> inc a (chainx a).
Proof.
move=> asf; apply: setI_i; first by apply: Exercise2_6b =>//.
by move=> y => /Zo_P [].
Qed.

Lemma Exercise2_6d a:
inc a (source f) -> inc (chainx a) bigS.
Proof.
move => asf.
move: (Exercise2_6b asf) =>ne; move: (ne) => [u ub].
apply: Zo_i.
apply /setP_P; move=> t td; move: (setI_hi td ub).
by move: ub => /Zo_P [] /Zo_P [] /setP_P usr _ _ tu ; apply: usr.
split.
move=> x xc; apply: setI_i => //.
move=> y yb; move: (setI_hi xc yb).
by move: yb => /Zo_P [] /Zo_P [] /setP_P _ [p _] _ tu; apply: p.
move=> N x Nca neN leN.
apply: setI_i => // y yb; move: (yb) => /Zo_P [yc ay].
move: yc => /Zo_P [_ [_ p]]; apply: (p N x) => //.
move=> t tN ; exact: (setI_hi (Nca _ tN) yb).
Qed.

Lemma Exercise2_6e a b:
inc a (source f) -> least_upper_bound r (chainx a) b ->
(inc b (chainx a) /\ Vf f b = b).
Proof.
move=> asf leb.
move: (Exercise2_6c asf) (Exercise2_6d asf) => aca.
move => /Zo_P [p1 [p2]] => aux; move: p1 => /setP_P p1.
have neca: nonempty (chainx a) by exists a.
have ba: inc b (chainx a) by apply: (aux _ _ (@sub_refl (chainx a)) neca leb).
split => //; move: leb => /(lubP or p1) [[_ ub] _ ].
move: (ub _ (p2 _ ba)) (fxx (p1 _ ba)) => le1 le2; order_tac.
Qed.

A chain is well-ordered. Proof. We consider a set M0, two subsets M1 and M2; two quantities p1, p2; we deduce M and p. For x in M; p(x) is not in x. By Zermelo_aux there exists a well-ordered set q, such that p(Sx)=x (where Sx is the segment with end point x in q) and q is not in M. As a consequence, the chain of a is a subset of q; since the ordering of q coincides with that of E, it follows that the chain is well-ordered.
Lemma Exercise2_6h a:
inc a (source f) -> worder (induced_order r (chainx a)).
Proof.
move=> asf.
set (E:= substrate r).
set(M0 := Zo (powerset E) (fun z => inc a z /\ exists b,
least_upper_bound r z b)).
have aE: inc a E by rewrite /E sf.
have p0: forall x, inc x M0 -> sub x (substrate r).
by move=> x => /Zo_P [] /setP_P.
have p1: (forall z, inc z M0 -> least_upper_bound r z (supremum r z)).
move=> z /Zo_P [zp [az [b leb]]].
by apply: supremum_pr1 => //; exists b.
have p2: forall x, inc x M0 -> (inc (supremum r x) (substrate r)
/\ inc (Vf f (supremum r x)) (substrate r)).
move => x xM0; move: (p0 _ xM0) => xE; move: (p1 _ xM0).
move => /(lubP or xE) [[sE _] _]; split => //;move: (fxx sE) => aux;order_tac.
pose sif x := glt r x (Vf f x).
set (M1 := Zo M0 (fun z => ~ (inc (supremum r z) z))).
set (M2 := Zo M0 (fun z => sif (supremum r z))).
set(M:= (M1 \cup M2) +s1 emptyset).
pose p x := Yo (x= emptyset) a
(Yo (inc x M1) (supremum r x) (Vf f (supremum r x))).
have Ha:sub (M1 \cup M2) M0 by apply: setU2_12S; apply: Zo_S.
have p3: (forall x, inc x M -> (inc (p x) E /\ ~ inc (p x) x)).
move=> x xM; rewrite /p; Ytac xe.
by split => //; move=> xie; empty_tac1 a.
Ytac xM1.
by move: xM1 => /Zo_P [xM0 ni]; split => //; case: (p2 _ xM0).
move: xM; case /setU1_P; first case /setU2_P; move => H; try contradiction.
move /Zo_P:H => [xM0 lt1]; move: (p2 _ xM0) => [p3 p4]; split => //.
move=> h; move: (p0 _ xM0) => xE;move: (p1 _ xM0); move /(lubP or xE).
rewrite /sif in lt1; move=> [ [_ ub ] _]; move: (ub _ h) => p5; order_tac.
have p4: sub M (powerset E).
move=> t th; apply /setP_P.
case /setU1_P: th => h; [ apply: (p0 _ (Ha _ h)) | rewrite h; fprops].
move: (Zermelo_aux p4 p3) => [r' []]; rewrite /Zermelo_axioms.
set (q:= substrate r'); move=> wor' qE xqs xqp nqM.
have aq: (inc a q).
case: (emptyset_dichot q) => qe; first by case: nqM; rewrite /M qe; fprops.
move: (worder_has_empty_seg wor' qe) => [x xsr' se].
by move: (xqp _ xsr'); rewrite se /p Y_true // => ->.
have compat: (forall u v, gle r' u v -> gle r u v).
move=> u v uv.
have vq: (inc v q) by rewrite /q; order_tac.
have bE: inc v E by apply: qE.
case: (equal_or_not u v) => auv; first by rewrite auv; order_tac.
have suv:(inc u (segment r' v)) by apply: segment_inc.
have nes: segment r' v <> emptyset.
move=> h; move: suv; rewrite h; case /in_set0.
move: (xqs _ vq); case /setU1_P => h; last by contradiction.
move: (p1 _ (Ha _ h)); set c := supremum r _.
have ss: sub (segment r' v) (substrate r).
apply: (@sub_trans q) => //; apply: sub_segment.
move=> /(lubP or ss) [[_ p5] _]; move: (p5 _ suv) => le1.
have csr: (inc c (substrate r)) by order_tac.
move: (xqp _ vq); rewrite /p ; Ytac0; Ytac c1; first by move => <-.
move: h; case /setU2_P; first by move => H.
move /Zo_P => [_ [le2 _]] eq1; rewrite eq1 in le2; order_tac.
move: (wor') => [or' _].
have p5: forall y, least_upper_bound r q y -> (inc y q /\ Vf f y = y).
move=> y ley.
have qM0: inc q M0 by apply: Zo_i; [ apply /setP_P | split => //; exists y].
case: (inc_or_not y q) => yq.
case: (equal_or_not y (Vf f y)) => w //.
move: nqM => /setU1_P; case; left; apply /setU2_P; right.
apply /Zo_i => //; red; rewrite - (supremum_pr2 or ley); split =>//.
by apply: fxx; apply: qE.
move: nqM => /setU1_P; case; left; apply /setU2_P; left.
by apply /Zo_i => //; rewrite - (supremum_pr2 or ley).
have stable: (forall x, inc x q -> inc (Vf f x) q).
move=> x xq; set (m:=Zo q (fun z => glt r' x z)).
case: (emptyset_dichot m) => em.
have gx: (greatest r' x).
split => // y ysr; case: (total_order_pr2 (worder_total wor') xq ysr)=>//.
move=> bad; empty_tac1 y;apply: Zo_i => //; order_tac.
have gx':(greatest (induced_order r q) x).
split;aw; move=> y yq; apply /iorder_gleP => //; apply: compat.
by move: gx => [_ p6]; apply: p6.
move: (greatest_is_sup or qE gx') => sq.
by move: (p5 _ sq) => [r1 r2]; rewrite r2.
move: (Exercise2_6g wor' xq em) => [z zsr ss].
have xs: inc x (segment r' z) by rewrite - ss; apply: inc_bound_segmentc.
case: (equal_or_not (segment r' z) emptyset) => xse; first by empty_tac1 x.
move: (xqs _ zsr) (xqp _ zsr); set s := segment r' z => p5' p6.
have ssr': sub s (substrate r') by apply: sub_segment.
have ssr: sub s (substrate r) by apply: (@sub_trans q).
have gx: (greatest (induced_order r' s) x).
split;aw=> y ysr; apply /iorder_gleP => //.
case: (total_order_pr2 (worder_total wor') xq (ssr' _ ysr))=>//.
by move: ysr; rewrite /s - ss => /segmentcP.
have gx':(greatest (induced_order r s) x).
split; aw; move=> y yq; apply /iorder_gleP => //; apply: compat.
by move: yq; rewrite /s - ss => /segmentcP.
move: (greatest_is_sup or ssr gx') => sq.
move:(supremum_pr2 or sq) => xsq.
move: p5' p6; case /setU1_P; last by exact.
rewrite /p; Ytac0; Ytac nsm1.
move: nsm1 => /Zo_P;rewrite -xsq; move=> [_ h]; contradiction.
case /setU2_P; [ done | by rewrite -xsq;move=> _ -> ].
move: (worder_total wor') => [_ tor'].
have toq: forall a b, inc a q -> inc b q -> gle r a b \/ glt r b a.
move => u v uq vq.
case:(equal_or_not u v) => uv; first by rewrite uv; left; order_tac; apply: qE.
rewrite /glt; case: (tor' _ _ uq vq) => h; move: (compat _ _ h);fprops.
have compat': forall u v, inc u q -> inc v q -> gle r u v -> gle r' u v.
move=> u v uq vq uv.
case: (tor' _ _ uq vq) => h; move: (compat _ _ h) => //.
by move=> vu; move: h; rewrite (order_antisymmetry or uv vu).
have aux: (forall N y, sub N q -> nonempty N -> least_upper_bound r N y ->
inc y q).
move => N y Nq neN infN.
move: (sub_trans Nq qE) => NE.
move: infN => /(lubP or NE) [[ys uny] luny].
set (bN:=Zo q (fun z=> gle r y z)).
case: (emptyset_dichot bN) => bne.
have le1: (least_upper_bound r q y).
apply /(lubP or qE); split.
split =>// z zq.
have [t [tN [zt _]]]: (exists t, inc t N /\ glt r z t).
ex_middle bad; empty_tac1 z; apply: Zo_i => //.
apply: luny; split; first by apply: qE.
move=> t tN; case: (toq _ _ (Nq _ tN) zq) => //.
by move => zt; case: bad; exists t.
move: (uny _ tN) => h; order_tac.
by move=> z [zr uz]; apply: luny; split => // t tn; apply: uz; apply: Nq.
by move: (p5 _ le1) => [ok _].
have bNq: (sub bN q) by apply: Zo_S.
move: wor' => [_ wor''];move: (wor'' _ bNq bne) => [z []];aw.
move=> zbN zlbn.
move: (zbN) => /Zo_P [zq yz].
case: (inc_or_not z N) => zN.
by move: (uny _ zN) => zy; rewrite (order_antisymmetry or yz zy).
have zlb1: (forall u, inc u q -> gle r y u -> gle r' z u).
move=> u uq r1; have ub: (inc u bN) by apply: Zo_i.
exact: (iorder_gle1 (zlbn _ ub)).
have Ns: (sub N (segment r' z)).
move=> t tN ; apply /segmentP; split; last by dneg tz; ue.
move: (uny _ tN) => ty; apply: compat' => //;[ by apply: Nq | order_tac].
have Nes: (nonempty (segment r' z)).
by move: neN => [w wN]; exists w; apply: Ns.
case: (equal_or_not (segment r' z) emptyset) => Nes'.
by case /nonemptyP: Nes.
move: (xqs _ zq)(xqp _ zq); case /setU1_P; last (by done).
rewrite /p;Ytac0; move=> aux; move: (p1 _ (Ha _ aux)).
have aux1: sub (segment r' z) (substrate r)
by apply: (@sub_trans q) => //; apply: sub_segment.
set s := (supremum r (segment r' z)); move /(lubP or aux1)=> [[p6 p7] p8].
have ys1: (gle r y s) by apply: luny; split => // t tn; apply: p7; apply: Ns.
have sz: (gle r s z).
apply: p8; split;fprops; move => t /segmentP [le _].
by apply: compat.
have sns: ~ (inc s (segment r' z)) .
move / segmentP => [r1 r2].
have sq: (inc s q) by rewrite / q; order_tac.
move: (zlb1 _ sq ys1) => aux2; case: r2; order_tac.
have p9: (inc (segment r' z) M1) by apply: Zo_i => //; apply: Ha.
Ytac0; move=> sz1.
suff:(gle r s y) by move=> sy; rewrite - (order_antisymmetry or sy ys1) sz1.
apply: p8; split => //; move=> t /segmentP tz.
have tq: (inc t q) by rewrite /q; order_tac.
case: (p_or_not_p (exists2 u, inc u N & glt r t u)).
move=> [u uN [tu _]]; move: (uny _ uN) => uy; order_tac.
have good: (forall u, inc u N -> gle r u t).
move=> u uN; case: (toq _ _ (Nq _ uN) tq) => // tu; case: bad; ex_tac.
have ubt: (upper_bound r N t) by split =>//; apply: qE.
move:(zlb1 _ tq (luny _ ubt)) => p10; order_tac.
have sc: (sub (chainx a) q).
move => t tc; apply: (setI_hi (y:=q) tc);apply: Zo_i => //.
apply: Zo_i; [ by apply /setP_P | split => //].
move: (sub_trans sc qE) => sE.
move: (iorder_osr or sE) => [or1 sr1].
split => //; rewrite sr1 => x xc nex; move: (sub_trans xc sc) => xcq.
move: (sub_trans xcq qE) => xE.
move: wor' => [_ wor''];move: (wor'' _ xcq nex) => [z []];aw.
move=> zx zl; exists z; rewrite iorder_trans //;split => //; aw.
move=> b bx;apply /iorder_gleP => //;apply:(compat _ _ (iorder_gle1 (zl _ bx))).
Qed.

End Exercise2_6.

Exercise 2.7. Properties of closures. If E is ordered, we consider the closures; let I(f) be the set of fixed-points of f. We have f <= g iff sub (I g) (I f). There is a least function, the identity.
Section Exercise27.
Variable r: Set.
Hypothesis or: order r.

Definition closures :=
let E:=substrate r in
Zo (functions E E) (fun z=> closure z r).

Definition closure_ordering :=
let E:=substrate r in
induced_order (order_function E E r) (closures).

Lemma Exercise2_7aP f g:
let E:=substrate r in
gle (closure_ordering) f g <->
[/\ inc f (closures), inc g (closures) &
forall i, inc i (substrate r) -> gle r (Vf f i) (Vf g i)].
Proof.
move=> E.
move: (order_function_osr E or (refl_equal E)) => [or' sr'].
have p1: (sub (closures) (substrate (order_function E E r))).
rewrite sr'; apply: Zo_S.
rewrite /closure_ordering; split => h.
move: (iorder_gle1 h)(iorder_gle3 h) => fg [fs gs]; split => //.
by move: fg => /order_functionP [_ _ ok].
move: h => [h1 h2 h3];apply/iorder_gleP => //.
by move: h1 h2 => /Zo_P [h1 h2] /Zo_P [h3' h4]; apply /order_functionP.
Qed.

Lemma Exercise2_7b:
order_on closure_ordering closures.
Proof.
rewrite /closure_ordering; set E:= (substrate r).
move: (order_function_osr E or (refl_equal E)) => [p1 p2].
apply:iorder_osr => //; rewrite p2; apply: Zo_S.
Qed.

Lemma Exercise2_7c:
least (closure_ordering) (identity (substrate r)).
Proof.
set (E:=substrate r); set (f:= identity E).
have ifsr: inc f closures.
rewrite /f; apply: Zo_i ;first by apply /fun_set_P;red;aw;split;fprops.
split => //.
- split => //; first by apply: identity_prop.
move=> x y xy; bw; rewrite /E;order_tac.
- by move=> x xsr; bw; order_tac.
- move => x xsr; bw; bw.
move: Exercise2_7b => [p1 p2].
red; rewrite p2;split => // => x xs; apply /Exercise2_7aP; split => //.
move => i isr; rewrite /f; bw.
by move: xs => /Zo_hi [_ p4 _];apply: p4.
Qed.

Lemma Exercise2_7dP f g:
inc f closures -> inc g closures ->
(gle (closure_ordering) f g <->
sub (invariants g) (invariants f)).
Proof.
move=> fs gs; move: (fs) => /Zo_P [p1 p2].
move: (gs) => /Zo_P [p3 p4].
move: p2 p4=> [q1 q2 q3] [q4 q5 q6].
move: p1 p3 => /fun_set_P [ff sf tf] /fun_set_P [fg sg tg].
split.
move /Exercise2_7aP=> [_ _ h] t => /Zo_P [tsg wg]; apply /Zo_P;split => //.
by rewrite sf - sg.
rewrite sg in tsg; move: (q2 _ tsg) => p11.
move: (h _ tsg) ; rewrite wg=> p7; order_tac.
move=> h; apply /Exercise2_7aP;split => //.
move=> i isr.
move: (q5 _ isr) => le1.
move: (q6 _ isr) => le2.
have : inc (Vf g i) (invariants f).
apply: h; apply: Zo_i=> //; rewrite sg - tg; apply: Vf_target => //; ue.
by move /Zo_P=> [_ <-]; move: q1 => [_ _ _ incf]; apply: incf.
Qed.

If f_i is a family of closures, if inf_i (f_i x) exists for all x, then this is the infimum of the family. Thus: (a) if any pair has an infimum in E, the same holds for closures; (b) if E is a complete lattice so is the set of closures

Lemma Exercise2_7e f g:
(forall x y, inc x (substrate r) -> inc y (substrate r) ->
has_infimum r (doubleton x y))
-> inc f (closures)
-> inc g (closures)
-> has_infimum (closure_ordering) (doubleton f g).
Proof.
move=> hid fc gc.
have Ht:sub (doubleton f g) (closures).
by move=> t /set2_P; case => ->.
move: (fc) (gc) => /Zo_P[p1 p2] /Zo_P [p3 p4].
set (E:= substrate r) in *.
move: p2 p4=> [q1 q2 q3] [q4 q5 q6].
have Ha: forall x, inc x E -> inc (Vf f x) E.
move=> x xE; move: (q2 _ xE) => aux; rewrite /E; order_tac.
have Hb: forall x, inc x E -> inc (Vf g x) E.
move=> x xE; move: (q5 _ xE) => aux; rewrite /E; order_tac.
set (hh:= fun z=> inf r (Vf f z) (Vf g z)).
have hp: (forall x, inc x E ->
(gle r (hh x) (Vf f x) /\ gle r (hh x) (Vf g x) /\
forall z, gle r z (Vf f x) -> gle r z (Vf g x) -> gle r z (hh x))).
move => x xE; move: (Ha _ xE) (Hb _ xE) => fE gE.
move: (inf_pr or fE gE (hid _ _ fE gE)) => [qa qb qc]; split => //.
have h1: forall x, inc x E -> gle r x (hh x).
move=> x xE; move: (hp _ xE) => [_ [_ aux]].
apply: aux; [ by apply: q2 | by apply: q5 ].
have ep: forall x y, gle r x y -> (inc x E /\ inc y E).
move=> x y xy; rewrite /E; split; order_tac.
have h2: forall x y, gle r x y -> gle r (hh x) (hh y).
move=> x y xy; move: (ep _ _ xy) => [xE yE].
move: q1 => [_ _ _ incf]; move: (incf _ _ xy) => r4.
move: q4 => [_ _ _ incg]; move: (incg _ _ xy) => r5.
move: (hp _ xE) (hp _ yE)=> [r1 [r2 _]] [_ [_ r3]].
apply: r3; order_tac.
set (h:= Lf hh E E).
have ta: lf_axiom hh E E.
by move => w xe; move: (h1 _ xe) => h3; rewrite /E;order_tac.
have fh: function h by apply: lf_function.
have ch: closure h r.
split => //.
split => //; first by rewrite /h; split; aw.
rewrite /h; move=> x y xy; move: (ep _ _ xy) => [xE yE].
aw;by apply: h2.
by move=> x xE; rewrite /h;aw; apply: h1.
move=> x xE; move: (ta _ xE) => hE; rewrite /h (lf_V ta xE) (lf_V ta hE).
move: (hp _ hE) => [r3 [r4 _]].
move: (hp _ xE) => [r5 [r6 r9]].
move: q1 => [_ _ _ incf]; move: (incf _ _ r5).
move: q4 => [_ _ _ incg]; move: (incg _ _ r6).
rewrite (q6 _ xE) (q3 _ xE) => r7 r8.
move: (r9 _ (order_transitivity or r3 r8) (order_transitivity or r4 r7)).
move: (h1 _ hE) => r10 r11; order_tac.
move: (Exercise2_7b) => [oco sco].
have hco: inc h closures
by apply: Zo_i => //; apply /fun_set_P; split => //; rewrite /h;aw.
have hsco: inc h (substrate (closure_ordering)) by rewrite sco.
have sd: sub (doubleton f g) (substrate closure_ordering) by ue.
exists h.
apply /(glbP oco sd); split.
by split => //; move=> y; aw => /set2_P; case => ->; apply /Exercise2_7aP;
split => //;move=> i isr; rewrite /h; aw; move: (hp _ isr)=>[s1 [s2 _]].
move=> z [ze zh].
move: (zh _ (set2_1 f g)) (zh _ (set2_2 f g)).
move /Exercise2_7aP => [zc _ s1] /Exercise2_7aP [_ _ s2].
apply/Exercise2_7aP;split => //.
move=> i isr; move: (s1 _ isr)(s2 _ isr)(hp _ isr)=> s3 s4 [_ [_ s5]].
by rewrite /h; aw; apply: s5.
Qed.

Lemma Exercise2_7f: complete_lattice r ->
complete_lattice (closure_ordering).
Proof.
move=> [_ cl1];move: (Exercise2_7b) => [oco sco].
apply: Exercise1_11h => //; rewrite sco => X Xc.
have xp1: forall f, inc f X -> closure f r.
by move=> f fx; move: (Xc _ fx) => /Zo_P [ _ ].
set (iv := fun x => fun_image X (fun z => Vf z x)).
have ivs: (forall x, inc x (substrate r) -> sub (iv x) (substrate r)).
move=> x xsr t => /funI_P [z zX ->].
move: (xp1 _ zX) => [_ s1 _]; move: (s1 _ xsr) => s2; order_tac.
set (hh := fun x => infimum r (iv x)).
have hp1: (forall x, inc x (substrate r) -> (lower_bound r (iv x) (hh x) /\
forall z, lower_bound r (iv x) z -> gle r z (hh x))).
move=> x xsr; move:(ivs _ xsr)=> isr; move: (cl1 _ isr ) => [_ hi].
apply: (infimum_pr or isr hi).
have ta: (lf_axiom hh (substrate r) (substrate r)).
by move=> t tsr; move: (hp1 _ tsr) => [[ok _] _].
set (h:= Lf hh (substrate r) (substrate r)).
have fh: (function h) by apply: lf_function.
have p1: (forall x f, inc x (substrate r) -> inc f X ->
gle r (Vf h x) (Vf f x)).
move=> x f xsr fX;move: (hp1 _ xsr) => [[_ xx] _]; rewrite /h; aw.
apply: xx; apply /funI_P; ex_tac.
have p2: forall x y, inc x (substrate r) -> inc y (substrate r) ->
(forall f, inc f X -> gle r y (Vf f x)) -> gle r y (Vf h x).
move=> x y xsr ysr h1; rewrite /h;aw; move: (hp1 _ xsr) => [_]; apply.
by split => //; move=> t /funI_P [z zX ->]; apply: h1.
have p3: (increasing_fun h r r).
rewrite /h;split => //; first (split; aw); move=> x y xy.
have xE: (inc x (substrate r)) by order_tac.
have yE: (inc y (substrate r)) by order_tac.
aw; move: (hp1 _ xE)(hp1 _ yE) => [[h1 h2] _] [_]; apply.
split => //; move=> z /funI_P [f fX] ->.
move: (xp1 _ fX) => [[_ _ _ incf] _ _ ].
move: (incf _ _ xy) => h3.
have h4: (inc (Vf f x) (iv x)) by apply /funI_P; ex_tac.
move: (h2 _ h4) => h5;order_tac.
have p4: (forall x, inc x (substrate r) -> gle r x (Vf h x)).
move=> x xsr; apply: (p2 _ _ xsr xsr).
by move=> f fX; move: (xp1 _ fX) => [_ h2 _]; apply: h2.
have p5:(forall x, inc x (substrate r) -> Vf h (Vf h x) = Vf h x).
move=> x xE; move: (ta _ xE) => ws.
have W1: Vf h x = hh x by rewrite /h; aw.
symmetry; apply: (order_antisymmetry or).
by move: (p4 _ ws); rewrite -W1.
move: (hp1 _ xE) => [_]; rewrite W1;apply.
split; first by rewrite /h;aw; apply: (ta _ ws).
move => y /funI_P [z zX ->].
move: (p1 _ _ ws zX) => p5.
move: (xp1 _ zX) => [[_ _ _ incf] _ aa].
move: (incf _ _ (p1 _ _ xE zX)); rewrite (aa _ xE) W1=> p6; order_tac.
have ch: (closure h r) by split => //.
have hco: inc h closures
by apply: Zo_i => //; apply /fun_set_P;split => //; rewrite /h;aw.
have hsco: inc h (substrate (closure_ordering)) by rewrite sco.
have Wsr:sub X (substrate closure_ordering) by ue.
exists h.
apply /(glbP oco Wsr); split.
split => //; move=> y; aw => yX;apply /Exercise2_7aP.
move: (Xc _ yX)=> ys;split;fprops.
move=> z [z1 z2]; apply/Exercise2_7aP; split => //; first by ue.
move=> i isr; rewrite /h; aw;move: (hp1 _ isr) => [_ ]; apply.
move: z1; rewrite sco => /Zo_P [] /fun_set_P [fx sz tz] cz.
split => //; first by rewrite -tz; Wtac.
move=> y /funI_P [t tX ->].
by move: (z2 _ tX) =>/Exercise2_7aP [_ _ ]; apply.
Qed.

Bourbaki says: Each pair of closures has a supremum if E is inductive. This assertion is false.
We consider two closures u and v, with fix-points Iu and Iv; we search a closure w, with fixed point Iw, that is the least upper bound. Let T = intersection2 Iu Iv. Let f be the composition of u and v. Its set of fixed points is T. Let Ixf(x) the set of all fixed-points of f that are >=x. If w is an upper bound, then w(x) is a fixed-point of u and v, and thus of f, so is in Ixf(x).

Definition Ixf x f := Zo (substrate r) (fun z => gle r x z /\ Vf f z = z).
Definition Jf f := (forall x, inc x (substrate r) -> exists y,
least (induced_order r (Ixf x f)) y).

Lemma Exercise2_7g u v:
inc u (closures) -> inc v (closures) ->
Jf (compose u v) ->
has_supremum (closure_ordering) (doubleton u v).
Proof.
move=> uc vc Jcuv.
have Ht:sub (doubleton u v) (closures).
by move=> t /set2_P;case => ->.
move: (uc) (vc); move => /Zo_P [p1 p2] /Zo_P [p3 p4].
set (E:= substrate r) in *.
move: p2 p4=> [q1 q2 q3] [q4 q5 q6].
have Ha: forall x, inc x E -> inc (Vf u x) E.
move=> x xE; move: (q2 _ xE) => aux; rewrite /E; order_tac.
have Hb: forall x, inc x E -> inc (Vf v x) E.
move=> x xE; move: (q5 _ xE) => aux; rewrite /E; order_tac.
move: p1 p3 =>/fun_set_P [fu su tu] /fun_set_P [fv sv tv].
have cp: u \coP v by split => //;ue.
set f := u \co v.
have ff: (function f) by rewrite /f; fct_tac.
set (gg := fun x => the_least (induced_order r (Ixf x f))).
have sI: (forall x, inc x E -> sub (Ixf x f) (substrate r)).
move=> x xE; apply: Zo_S.
have sI1: forall x, inc x E -> substrate(induced_order r (Ixf x f)) = (Ixf x f).
move=> x xE; move: (sI _ xE) => aux; aw.
have lg: forall x, inc x E -> least (induced_order r (Ixf x f)) (gg x).
move=> x xE; move: (Jcuv _ xE) => ey.
apply: the_least_pr => //; apply: (proj1 (iorder_osr or (sI _ xE))).
have gp: forall x, inc x E ->
[/\ inc (gg x) (substrate r), gle r x (gg x), Vf f (gg x) = gg x &
(forall y, inc y (Ixf x f) -> gle r (gg x) y)].
move=> x xE; move: (lg _ xE);rewrite /least; rewrite (sI1 _ xE).
move => [] /Zo_P [pa [pb pc]] p2; split => //.
move=> y yI; move: (p2 _ yI) => h;apply: (iorder_gle1 h).
have ta:(lf_axiom gg E E).
by move=> t tE; move: (gp _ tE) => [ok _].
have p0P: forall x, inc x E -> ((gg x = x) <-> (Vf f x = x)).
move=> x xE; move: (gp _ xE) => [p1 p2 p3 p4].
split => h; first by rewrite -h.
have xI: inc x (Ixf x f) by apply: Zo_i => //; split => //; order_tac.
move: (p4 _ xI) => p5; order_tac.
have p1: (forall x, inc x E -> gle r x (gg x)).
by move=> x xE; move: (gp _ xE) => [_ ].
have p2: (forall x, inc x E -> gg (gg x) = gg x).
by move=> x xE; apply /(p0P _ (ta _ xE)); move: (gp _ xE) => [_ _].
have p3: forall x y, gle r x y -> gle r (gg x) (gg y).
move=> x y xy.
have xE:(inc x E) by rewrite /E;order_tac.
have yE:(inc y E) by rewrite /E;order_tac.
move: (gp _ yE) => [s1 s2 s3 s4].
have gyI: (inc (gg y) (Ixf x f)) by apply: Zo_i => //; split => //; order_tac.
by move: (gp _ xE) => [_ _ _]; apply.
set (g:= Lf gg E E).
have fg: (function g) by apply: lf_function.
have cg: (closure g r).
split => //; rewrite /g.
split => //; first by split; aw.
move=> x y xy; aw; first (by apply: p3); rewrite /E; order_tac.
by move=> x xE;aw; apply: p1.
by move=> x xE; rewrite (lf_V ta xE) (lf_V ta (ta _ xE)); apply: p2.
move: (Exercise2_7b) => [oco sco].
have hco: inc g closures
by apply: Zo_i => //; apply /fun_set_P; split => //; rewrite /g;aw.
have hsco: inc g (substrate (closure_ordering)) by rewrite sco.
have sd: sub (doubleton u v) (substrate closure_ordering) by ue.
have sg: source g = E by rewrite /g;aw.
have sf: source f = E by rewrite /f; aw.
have ig: invariants g = invariants f.
set_extens t => /Zo_P []; rewrite ?sf ? sg => [r1 r2];
apply /Zo_P;split => //; try ue;
move : r2; rewrite /g; aw; move /(p0P _ r1) => //.
have sif: invariants f =
(invariants u) \cap (invariants v).
rewrite /invariants su sv sf; set_extens t.
move /Zo_P => [tE wf].
have tsv: inc t (source v) by ue.
have Wtsv: inc (Vf v t) (substrate r) by rewrite -/E -tv; fprops.
move: wf; rewrite /f; aw => wf.
move: (f_equal (fun z=> Vf u z) wf); rewrite q3 // wf => f1.
move: (q2 _ Wtsv) (q5 _ tE); rewrite wf => le1 le2.
apply /setI2_P; split => //; apply /Zo_P;split => //;order_tac.
move /setI2_P => [] /Zo_P [tE Wu] /Zo_P [_ Wv]; apply /Zo_P;split => //.
by rewrite /f;aw; rewrite ?sv // Wv Wu.
exists g.
apply /(lubP oco sd); split.
split => //; move=> y ys.
have aux: inc y closures by rewrite - sco; apply: sd.
by apply /(Exercise2_7dP aux hco); case /set2_P: ys => ->;
rewrite ig sif => t /setI2_P [].
move=> z [ze zh].
have zc: inc z closures by ue.
move: (zh _ (set2_1 u v)) (zh _ (set2_2 u v)).
move /(Exercise2_7dP uc zc) => h1 /(Exercise2_7dP vc zc) => h2.
apply (Exercise2_7dP hco zc);rewrite ig sif.
move => t ts; apply: setI2_i;fprops.
Qed.

If Ixf(x) has a least element g(x), then g is a closure, and has the same fixed-points as f, thus is the least upper bound. If the set is inductive, then there is a maximal element >=x which is thus in Ixf(x). If the set is well-ordered, then Ixf(x) has least element; Thus any pair of closures has a supremum

Lemma Exercise2_7h u v:
inductive r -> worder r ->
inc u (closures) -> inc v (closures) ->
has_supremum (closure_ordering) (doubleton u v).
Proof.
move=> ir [_ wor] uc vc; apply: Exercise2_7g => //.
move=> x xsr.
set y := (Ixf x (compose u v)).
have sy: sub y (substrate r) by apply: Zo_S.
move: (inductive_max_greater or ir xsr) => [m [ms mm xm]].
move: uc vc => /Zo_P [p1 p2] => /Zo_P [p3 p4].
move: p2 p4=> [q1 q2 q3] [q4 q5 q6].
move: p1 p3 => /fun_set_P [fu su tu] /fun_set_P[fv sv tv].
have cuv: composable u v by split => //; ue.
have mv: inc m (source v) by ue.
move: q1 =>[_ _ _ incf]; move: (incf _ _ (q5 _ ms)) => le1.
move: (q2 _ ms) => le2.
have ne: nonempty y.
exists m; apply: Zo_i => //; split => //; aw; apply: mm; order_tac.
apply: (wor _ sy ne).
Qed.

End Exercise27.

Let's consider a counter-example; we consider all pairs (x,0) and (x,1), where x is an integer, ordered by: (x,0) < (y,1) and (x,0)<(y,0) whenever x<y, while (x,1)<(y,1) whenever y<x. It has a greatest element, thus is inductive

Lemma Exercise2_7A1 r:
(exists u, greatest r u) -> inductive r.
Proof. move=> [u [us ug]] x xsr tor; exists u; split;fprops. Qed.

Lemma Exercise2_7A2 r r': order r -> order r' ->
(exists u, greatest r' u)
-> inductive (order_sum2 r r').
Proof.
move=> or or' [u [us ug]];apply: Exercise2_7A1.
exists (J u C1).
have p1: (inc (J u C1) (canonical_du2 (substrate r) (substrate r'))).
by apply: candu2_prb.
split; rewrite orsum2_sr => //.
move=> x h ; apply /orsum2_gleP; split => //; aw.
move/candu2P: h => [ _ ] [] [p2 ->];
[constructor 3 | constructor 2 ]; split;fprops.
Qed.

Definition NNstar :=
order_sum2 Bnat_order (opp_order Bnat_order).

Lemma Exercise2_7A3:
[/\ order_on NNstar (canonical_du2 Bnat Bnat) &
(forall x x', gle NNstar x x' <->
[/\ inc x (canonical_du2 Bnat Bnat),
inc x' (canonical_du2 Bnat Bnat) &
[\/ [/\ Q x = C0, Q x' = C0 & (P x) <=c (P x')],
[/\ Q x <> C0, Q x' <> C0 & (P x') <=c (P x)] |
(Q x = C0 /\ Q x' <> C0)]])].
Proof.
rewrite /NNstar.
move: Bnat_order_wor=> [[or _] s1].
move: (opp_osr or) => [or1]; rewrite s1 => s2.
split; first by split; fprops;rewrite orsum2_sr // s1 s2.
move=> x x'; split.
move /orsum2_gleP; rewrite s1 s2; move => [p1 p2 p3];split => //.
case: p3; first by move => [q1 q2] /Bnat_order_leP [_ _ s4]; constructor 1.
by move => [q1 q2] /opp_gleP /Bnat_order_leP [_ _ s4]; constructor 2.
by move => q1; constructor 3.
move => [p1 p2 p3]; apply /orsum2_gleP; rewrite s1 s2; split => //.
have aux: forall z, inc z (canonical_du2 Bnat Bnat) -> inc (P z) Bnat.
by move=> z /candu2P[_ ]; case; case.
case: p3.
move => [q1 q2 q3]; constructor 1;split => //;apply /Bnat_order_leP.
by split => //; apply: aux.
move => [q1 q2 q3]; constructor 2;split => //.
by apply /opp_gleP/Bnat_order_leP;split => //; apply: aux.
by move => q1; constructor 3.
Qed.

Lemma Exercise2_7A4: inductive NNstar.
Proof.
move: (Bnat_order_wor) => [[or _] bs].
apply: Exercise2_7A2 => //.
apply: (proj1 (opp_osr or)).
exists \0c; apply: least_opposite =>//.
split; first by rewrite bs; fprops.
move => x; rewrite bs => xb; apply /Bnat_order_leP; split => //; fprops.
Qed.

If f: N -> N is a function; we extent it to E by g((x,0)) = (f(x),0) and g((x,1)) = ( x,1). If f is a closure so is g

Definition extension_to_NNstar f :=
Lf (fun z=> Yo (Q z = C0) (J (Vf f (P z)) C0) z)
(substrate NNstar) (substrate NNstar).

Lemma Exercise2_7A5 f (g:= extension_to_NNstar f) (E:= substrate NNstar):
function_prop f Bnat Bnat ->
[/\ (forall x, inc x Bnat -> Vf g (J x C0) = (J (Vf f x) C0)),
(forall x, inc x E -> Q x = C0 ->
(P (Vf g x) = Vf f (P x) /\ Q (Vf g x) = C0)),
(forall x, inc x E -> Q x <> C0 -> Vf g x = x) &
function_prop g E E].
Proof.
move=> [ff sf tf].
move: Exercise2_7A3 => [[_ ss] _].
have ta:(lf_axiom (fun z=> Yo (Q z = C0) (J (Vf f (P z)) C0) z)
(canonical_du2 Bnat Bnat) (canonical_du2 Bnat Bnat)).
move: TP_ne1 => tpd.
move=> t /candu2P.
move=> [pt]; case; move=> [Pt Qt]; rewrite Qt; Ytac0.
apply: candu2_pra; Wtac.
by rewrite - pt Qt; apply: candu2_prb.
rewrite /g /extension_to_NNstar /E ss.
split => //.
move=> x xB; aw; [by Ytac0 | by apply: candu2_pra].
move=> x xE; aw; move=> ->; Ytac0; aw;split => //.
move=> x xE; aw; move=> h; Ytac0; fprops.
by red; aw; split => //; apply: lf_function.
Qed.

Lemma Exercise2_7A6: forall f, closure f Bnat_order ->
closure (extension_to_NNstar f) NNstar.
Proof.
move=> f [ [ob _ [ff sf tf] incf] c1 c2].
move: (proj2 Bnat_order_wor) => bos.
have fp: function_prop f Bnat Bnat by split => //; ue.
move: (Exercise2_7A5 fp) => /=.
set g:= (extension_to_NNstar f); set (E:=substrate NNstar).
move=> [ga0 ga gb [fg sg tg]].
move: Exercise2_7A3 => [[oNN sNN] leNNP].
rewrite /E sNN in sg tg ga gb.
split.
split;fprops; first by split; aw; ue.
move=> x y =>/leNNP [p1 p2 p3]; apply /leNNP; split; try Wtac.
case: p3.
move=> [q1 q2 q3]; constructor 1.
move: (ga _ p1 q1) (ga _ p2 q2) => [r1 r2] [r3 r4].
rewrite r1 r2 r3 r4; split => //.
have aux: gle Bnat_order (P x) (P y).
apply /Bnat_order_leP => //; split => //.
by move:p1 => /candu2P [ _ ]; case; move=> [px qx].
by move:p2 => /candu2P [ _ ]; case; move=> [px qx].
by move: (incf _ _ aux) => /Bnat_order_leP [_ _].
move=> [q1 q2 q3]; constructor 2.
by move: (gb _ p1 q1) (gb _ p2 q2) => -> ->.
move=> [q1 q2]; constructor 3.
by move: (ga _ p1 q1) (gb _ p2 q2) => [_] -> ->.
rewrite sNN; move=> x xs; apply /leNNP; split => //.
rewrite -tg; apply: Vf_target=> //; ue.
move: (xs) =>/candu2P [ _ ]; case.
move=> [pb qx]; move: (ga _ xs qx); move=> [pw qw]; constructor 1.
rewrite pw qw;split => //; rewrite bos in c1; move: (c1 _ pb).
by move /Bnat_order_leP => [_ _].
move=> [pb qx]; have qqx: (Q x <> C0) by rewrite qx; fprops.
move: (gb _ xs qqx) => ->; constructor 2; split;fprops.
move=> x; rewrite sNN => xs.
move: (xs) => /candu2P [ _ ]; case.
move=> [px qx]; move: (ga _ xs qx) ; move=> [pw qw].
have wa: inc (Vf g x) (canonical_du2 Bnat Bnat).
rewrite -tg; apply: Vf_target => //; ue.
move: (ga _ wa qw) ; move=> [pw2 qw2].
have wb: inc (Vf g (Vf g x)) (canonical_du2 Bnat Bnat) by Wtac.
move: wa => /candu2P [pw3 _ ].
move: wb =>/candu2P [pw4 _ ].
apply: pair_exten => //; [ rewrite pw2 pw c2 //; ue | rewrite qw2 //].
move=> [_ qx]; have qqx: (Q x <> C0) by rewrite qx; fprops.
by move: (gb _ xs qqx) => aux; rewrite {1} aux.
Qed.

Let u(x) be x+1 if x is even and x otherwise, and let v(x) be x+1 if x is odd and x otherwise. These are closures, and have no common fix-point, thus no least upper bound. Note that the set of integers is not inductive, so that this is not a counter-example to Bourbaki

Lemma Exercise2_7A7:
(lf_axiom (fun z => Yo (even_int z) z (succ z)) Bnat Bnat).
Proof. move=> t tb /=; Ytac h; fprops. Qed.

Lemma Exercise2_7A8:
(lf_axiom (fun z => Yo (even_int z) (succ z) z) Bnat Bnat).
Proof. move=> t tb /=; Ytac h; fprops. Qed.

Lemma Exercise2_7A9:
closure (Lf (fun z => Yo (even_int z) z (succ z)) Bnat Bnat) Bnat_order.
Proof.
move: Bnat_order_wor Exercise2_7A7 => [[ob _] sb] ta.
split => //.
split => //; first by red; aw; split => //; apply: lf_function.
move=> x y /Bnat_order_leP [xB yB xy]; aw.
apply /Bnat_order_leP;split => //; try apply:ta => //.
Ytac evx; Ytac evy => //.
move: (card_le_succ yB) => aux; co_tac.
apply /(card_le_succ_ltP _ xB); split =>// q; apply: evx; ue.
by apply /(card_le_succ_succP (CS_Bnat xB) (CS_Bnat yB)).
move=> x; rewrite sb => xB; aw; apply /(Bnat_order_leP); split => //; fprops.
Ytac evx;[ fprops | apply: (card_le_succ xB)].
move=>x ;rewrite sb => xB; rewrite (lf_V ta xB);move: (BS_succ xB) => sxB.
Ytac evx; aw; first by Ytac0.
have oi: odd_int x by split.
by move: (even_odd_succ x) => [_ h ];move: (h oi) => ok; Ytac0.
Qed.

Lemma Exercise2_7A10:
closure (Lf (fun z => Yo (even_int z) (succ z) z) Bnat Bnat) Bnat_order.
Proof.
move: Bnat_order_wor Exercise2_7A8 => [[ob _] sb] ta.
split => //.
split => //; first by red;aw; split =>//; apply: lf_function.
move=> x y /Bnat_order_leP [xB yB xy]; aw; apply /Bnat_order_leP.
split => //;fprops; Ytac evx; Ytac evy => //.
by apply /(card_le_succ_succP (CS_Bnat xB) (CS_Bnat yB)).
apply /(card_le_succ_ltP _ xB); split =>// q; apply: evy; ue.
move: (card_le_succ yB) => aux; co_tac.
move=> x;rewrite sb => xB; apply /Bnat_order_leP; aw;split => //; fprops.
Ytac evx; [apply: (card_le_succ xB) | fprops].
move=>x ;rewrite sb => xB; rewrite (lf_V ta xB); Ytac evx;aw; fprops.
by move: (even_odd_succ x) => [ h _ ]; move: (h evx) => [aa bb]; Ytac0.
by Ytac0.
Qed.

Lemma Exercise2_7A11 x w:
let u :=Lf (fun z => Yo (even_int z) (succ z) z) Bnat Bnat in
let v :=Lf (fun z => Yo (even_int z) z (succ z)) Bnat Bnat in
inc x Bnat ->
(Vf u x) <=c w ->
(Vf v x) <=c w ->
x <> w.
Proof.
move=> u v xB le1 le2 xw; rewrite /u/v.
suff: (succ x) <=c w by apply /(card_le_succ_ltP _ xB); case.
move: (Exercise2_7A7)(Exercise2_7A8) => p1 p2.
by move: le1 le2;rewrite /u/v;aw; Ytac evx; Ytac0.
Qed.

Consider the extensions of u and v to E. These are closures in an inductive set. We have to many upper bounds, for instance x -> sup(x,y), where y has the form (z,1) is an upper bound, and y=(0,1) gives the greatest upper bound.
If w is any upper bound, for any x, w(x,0) has the form (y,1) since u and v have no common fix-point. Assume w(0,0) = (k,1). Since (0,0) is the least element we have w(x) = (k,1) whenever x <=(k,1). Remembet that (k+1,1) < (k,1). Let f be the function that maps x to (k+1,1) if x<= (k+1,1) and w(x) otherwise. Then f<w and is an upper bound.
Lemma Exercise2_7A12: exists r u v,
[/\ order r, inductive r,
inc u (closures r), inc v (closures r) &
~ has_supremum (closure_ordering r) (doubleton u v)].
Proof.
move: Exercise2_7A7 Exercise2_7A8 Exercise2_7A9 Exercise2_7A10 Exercise2_7A11.
set (u :=Lf (fun z => Yo (even_int z) (succ z) z) Bnat Bnat).
set (v :=Lf (fun z => Yo (even_int z) z (succ z)) Bnat Bnat).
move=> ta1 ta2 c1 c2 ns.
move:(Exercise2_7A6 c1) (Exercise2_7A6 c2).
set (u1:= extension_to_NNstar u).
set (v1:= extension_to_NNstar v).
move=> c3 c4.
exists NNstar, u1,v1.
move: Exercise2_7A3 Exercise2_7A4 => [[oNN sNN] gNNP] iNN.
have wc:forall w, closure w NNstar -> inc w (closures NNstar).
move=> w wc; apply: Zo_i => //.
by move: wc =>[[_ _ xx _] _ _]; apply /fun_set_P.
move: (wc _ c3) (wc _ c4) => vc uc.
split => //.
move: (Exercise2_7b oNN) => [oce sce] hs.
rewrite - sce // in uc vc.
move: (sup_pr oce uc vc hs).
set w := sup _ u1 v1.
move => [/(Exercise2_7aP oNN) [_ wcl le1] /(Exercise2_7aP oNN) [_ _ le2] ale3].
have fpu: (function_prop u Bnat Bnat).
by red; rewrite /u; aw;split => //; apply: lf_function.
have fpv: (function_prop v Bnat Bnat).
by red; rewrite /v; aw;split => //; apply: lf_function.
move: (Exercise2_7A5 fpu) => /=; rewrite -/u1.
move=> [upa1 upa upb [fu1 su1 tu1]].
move: (Exercise2_7A5 fpv) => /=; rewrite -/v1.
move=> [vpa1 vpa vpb [fv1 sv1 tv1]].
move: (wcl) => /Zo_P [] /fun_set_P [fw sw tw] cw.
have wp1: forall x, inc x Bnat -> Q (Vf w (J x C0)) = C1.
move=> x xB.
have ps: (inc (J x C0) (substrate NNstar)).
by rewrite sNN; apply: candu2_pra.
have: (inc (Vf w (J x C0)) (substrate NNstar)).
rewrite -tw; Wtac.
rewrite sNN => /candu2P [p1]; case; case=> //.
move=> p2 p3.
set (y := P (Vf w (J x C0))).
have aux: (J y C0 = Vf w (J x C0)).
symmetry;rewrite /y;apply: pair_exten;fprops; aw.
have Js: (inc (J y C0) (substrate NNstar)).
by rewrite sNN; apply: candu2_pra.
move: (cw) => [_ _ p4]; move: (p4 _ ps);rewrite -aux => aux1.
move: (le1 _ Js) (le2 _ Js) => /gNNP [p5 p6 p7] /gNNP [p8 p9 p10].
move: p7; rewrite aux1 pr2_pair; case; last first.
by move => [_]; case.
by move => [_ h _]; case: h.
move: p10; rewrite aux1 pr2_pair; case; last first.
by move => [_]; case.
by move => [_ h _]; case: h.
move=> [p13 _ p14] [p11 _ p12].
have aux2: Q (J y C0) = C0 by aw.
move: (vpa _ Js aux2); aw; move=> [p15 _]; rewrite p15 in p14.
move: (upa _ Js aux2); aw; move=> [p16 _]; rewrite p16 in p12.
have yB: inc y Bnat.
by move: p9 => /candu2P [_]; case; case.
case: (ns _ _ yB p12 p14); aw.
move: (wp1 _ BS0) => p1.
set (k:= Vf w (J \0c C0)).
have Js:(inc (J \0c C0) (substrate NNstar)).
rewrite sNN; apply: candu2_pra; fprops.
have ks: (inc k (substrate NNstar)) by rewrite /k;Wtac.
have Pk: (inc (P k) Bnat).
by move: ks; rewrite sNN => /candu2P [ _ ]; case; case.
move: (wp1 _ BS0) => Qk.
move: cw => [[_ _ _ incf] wca wcb].
have Pk1: (forall x, gle NNstar x k -> Vf w x = k).
move=> x xk.
have aux : (gle NNstar (J \0c C0) x).
have xs: (inc x (substrate NNstar)) by order_tac.
apply/gNNP; rewrite - sNN; split => //; aw.
move: xs; rewrite sNN => /candu2P [ _]; case; move => [px qx].
constructor 1; split => //; apply: czero_least; fprops.
rewrite qx;constructor 3;split;fprops.
move: (incf _ _ xk)(incf _ _ aux); rewrite (wcb _ Js) -/k => r1 r2.
order_tac.
have q7: Vf w k = k by rewrite Pk1 //; order_tac.
set (k':= J (succ (P k)) C1).
have j's: (inc k' (substrate NNstar)).
rewrite /k' sNN; apply: candu2_prb; fprops.
have lt1: (glt NNstar k' k).
move: (card_lt_succ Pk) => [leP neP].
split.
apply /gNNP; rewrite - sNN /k';split => //; aw; constructor 2.
rewrite -/k Qk; split;fprops;apply: leP.
by move=> kk'; move: (f_equal P kk');rewrite /k'; aw => aux;case: neP.
set (ww := fun z=> Yo (gle NNstar z k') k' (Vf w z)).
have ta: (lf_axiom ww (substrate NNstar) (substrate NNstar)).
move=> z zs; rewrite /ww;Ytac cp => //; Wtac.
set (w' := Lf ww (substrate NNstar) (substrate NNstar)).
have fw': (function w') by apply: lf_function.
have q3: Q k' <> C0 by rewrite /k'; aw; fprops.
have q4: forall x, gle NNstar x k' -> Vf w' x = k'.
by move=> x xk; rewrite /w' /ww; aw; [ Ytac0 | order_tac].
have q5: forall x, inc x (substrate NNstar) -> ~ (gle NNstar x k')
-> Vf w' x = Vf w x.
by move=> x xs xk; rewrite /w' /ww; aw; Ytac0.
have q6: forall y, inc y (substrate NNstar) -> ~ gle NNstar y k'
-> gle NNstar k y.
move=> y ysr ng;apply /gNNP; rewrite - sNN; split => //; constructor 2.
move: (ysr); rewrite sNN =>/candu2P [py]; case.
move=> [pyb Qya]; case: ng;apply /gNNP; rewrite - sNN.
by split => //; constructor 3.
move=> [Pyb Qy]; split => //; [ rewrite Qk; fprops | rewrite Qy; fprops |].
have cy:cardinalp (P y) by fprops.
have ck:cardinalp (P k) by fprops.
case: (card_le_to_el cy ck) => //.
move=> lt2; case: ng; apply /gNNP; rewrite - sNN; split => //; constructor 2.
rewrite Qy;split => //; fprops.
by rewrite /k'; aw; apply /card_le_succ_ltP.
have w1: (forall x, inc x (substrate NNstar) ->
(gle NNstar (Vf u1 x) (Vf w' x) /\ gle NNstar (Vf v1 x) (Vf w' x))).
move=> x xs.
move: (le1 _ xs) (le2 _ xs) => le1s le2s.
case: (p_or_not_p (gle NNstar x k')) => xk; last first.
have ->:(Vf w' x = Vf w x) by rewrite /w' /ww; aw; Ytac0.
split => //; rewrite (q4 _ xk).
rewrite (q4 _ xk).
case: (equal_or_not (Q x) C0) => qx.
move: (upa _ xs qx)(vpa _ xs qx) => [_ q1] [_ q2].
by split; apply /gNNP; rewrite - sNN ?q1 ?q2;
split => //;try order_tac; constructor 3.
by move: (upb _ xs qx)(vpb _ xs qx) => -> ->.
have icw':increasing_fun w' NNstar NNstar.
rewrite /w';split => //; first (by split; aw); move=> x y xy.
have xs1: inc x (substrate NNstar) by order_tac.
have xs2: inc y (substrate NNstar) by order_tac.
case: (p_or_not_p (gle NNstar x k')) => xk; last first.
have yk: ~ gle NNstar y k' by dneg wk; order_tac.
by rewrite (q5 _ xs1 xk) (q5 _ xs2 yk); apply: incf.
case: (p_or_not_p (gle NNstar y k')) => yk.
by rewrite (q4 _ xk) (q4 _ yk); order_tac.
rewrite (q4 _ xk) (q5 _ xs2 yk).
move: (incf _ _ (q6 _ xs2 yk)); rewrite q7.
move: lt1 => [lt1 _] le3; order_tac.
have cw': (closure w' NNstar).
split => //; move=> x xs.
case: (p_or_not_p (gle NNstar x k')) => xk; first by rewrite (q4 _ xk).
by rewrite (q5 _ xs xk); apply: wca.
case: (p_or_not_p (gle NNstar x k')) => xk.
rewrite (q4 _ xk); apply: q4; order_tac; order_tac.
rewrite (q5 _ xs xk).
case: (p_or_not_p (gle NNstar (Vf w x) k')) => xk'; last first.
have ws: inc (Vf w x) (substrate NNstar) by move: (wca _ xs)=> h; order_tac.
by rewrite (q5 _ ws xk'); apply: wcb.
move: (incf _ _ (q6 _ xs xk)).
rewrite (q4 _ xk') -/k'; rewrite q7 => aux.
have aux1: gle NNstar k k' by order_tac.
order_tac.
have res0: inc w' (closures NNstar).
apply: Zo_i => //; apply /fun_set_P;split => //; rewrite /w';aw.
have res1: gle (closure_ordering NNstar) u1 w'.
apply /(Exercise2_7aP oNN);split => //.
by apply Zo_i => //; apply /fun_set_P.
by move=> i isr; case: (w1 _ isr).
have res2: gle (closure_ordering NNstar) v1 w'.
apply /(Exercise2_7aP oNN);split => //.
by apply Zo_i => //; apply /fun_set_P.
by move=> i isr; case: (w1 _ isr).
move:(ale3 _ res1 res2).
apply /(Exercise2_7aP oNN).
move=> [_ _ bad]; move: (bad _ j's); rewrite q4; last by order_tac.
move: lt1 => [lt2 lt3].
rewrite (Pk1 _ lt2) => aux; case: lt3; order_tac.
Qed.

Exercise 2.8. Ramified and completely ramified sets
Definition ramified r :=
forall x y, glt r x y -> exists z, [/\ glt r x z, ~ gle r y z & ~ gle r z y].

Definition ramifiedc r :=
ramified r /\ not (exists x, maximal r x).

Lemma Exercise2_8a r: order r -> anti_directed r -> ramified r.
Proof.
move=> or /(Exercise1_23hP or) [p1 p2].
move=> x y xy; move: (p1 _ _ xy) => [z xz p3]; exists z.
have zz: (gle r z z) by order_tac; order_tac.
have yy: (gle r y y) by order_tac; order_tac.
split => //;[ move=> yz; exact (p3 _ yz zz)| move=> zy;exact: (p3 _ yy zy)].
Qed.

The following set has a maximal element
Definition Exercise2_8a_R r a :=
Zo (powerset (substrate r))
(fun z => ramified (induced_order r z) /\
least (induced_order r z) a).

Lemma Exercise2_8b r a F: order r ->
(inc F (Exercise2_8a_R r a) <->
[/\ sub F (substrate r),
forall x y, glt r x y -> inc x F -> inc y F ->
exists z, [/\ glt r x z, ~ gle r y z, ~ gle r z y & inc z F],
inc a F &
(forall z, inc z F -> gle r a z)]).
Proof.
move=> or; split.
move => /Zo_P [] /setP_P Fd [p1 p2].
move: (p2) => []; aw => pa pb.
have pb': forall z , inc z F -> gle r a z.
by move => z zf; move /iorder_gle5P: (pb _ zf) => [_ _].
split => // x y xy xF yF.
have xy': glt (induced_order r F) x y by apply /iorder_gle6P.
move: (p1 _ _ xy'); move=> [z []] /iorder_gle6P [_ zF xz] /iorder_gle5P p4
/iorder_gle5P p5; exists z; split => // h; [ by case: p4 | by case: p5].
move=> [pF p1 p2 p3]; apply: Zo_i; first by apply /setP_P.
split; last by split; aw => x xF;apply /iorder_gleP=> //; apply: p3.
move=> x y; move/iorder_gle6P =>[xF yF xy].
move: (p1 _ _ xy xF yF) => [z [z1 z2 z3 z4]]; exists z;split.
by apply /iorder_gle6P.
by move /iorder_gle5P => [_ _].
by move /iorder_gle5P => [_ _].
Qed.

Lemma Exercise2_8c r a: order r -> inc a (substrate r) ->
exists A, maximal (sub_order (Exercise2_8a_R r a)) A.
Proof.
move=> or ar; apply: Zorn_lemma; first by fprops.
red; aw; set (F := Exercise2_8a_R r a).
move: (sub_osr F) => [oF sF].
move => X Xsr [];aw => [oX toX]; rewrite /upper_bound sF.
have asr: sub (singleton a) (substrate r) by move => t /set1_P ->.
have leX: (forall x y, inc x X -> inc y X -> sub x y \/ sub y x).
move => x y xX yX; move: (toX _ _ xX yX).
case => aux; move: (iorder_gle1 aux) => /sub_gleP [_ _ h]; in_TP4.
case: (emptyset_dichot X)=>xe.
exists (singleton a); split.
apply: Zo_i; first by apply /setP_P; apply: set1_sub.
split.
by move=> x y [cxy]; move: (iorder_gle3 cxy) => [] /set1_P -> /set1_P ->.
red; aw;split;fprops;move=> x /set1_P ->; apply /iorder_gleP;fprops.
by order_tac.
move => y yX; empty_tac1 y.
rewrite sF in Xsr.
have uX: (inc (union X) F).
rewrite /F (Exercise2_8b _ _ or); split => //.
move=> t /setU_P [y ty yX]; move: (Xsr _ yX) => /Zo_P.
by move=> [yp _]; move: yp => /setP_P; apply.
move => x y xy /setU_P [x' xx' xX'] /setU_P [y' yy' yX'].
have [z [zX xz yz]] : (exists z, [/\ inc z X, inc x z & inc y z]).
case: (leX _ _ xX' yX') => xy';[ exists y'| exists x']; split; fprops.
move: (Xsr _ zX); rewrite (Exercise2_8b _ _ or); move=> [_ h _].
move: (h _ _ xy xz yz) => [t [t1 t2 t3 t4]]; exists t; split => //.
union_tac.
move: xe => [e ex]; move: (Xsr _ ex); rewrite (Exercise2_8b _ _ or).
move=> [_ _ h _]; union_tac.
move=> z /setU_P [x zx zX]; move: (Xsr _ zX).
by rewrite (Exercise2_8b _ _ or); move=> [_ _ _ ]; apply.
exists (union X); split => //.
by move => x xF;apply/sub_gleP;split;fprops; apply: setU_s1.
Qed.

Bourbaki says "every maximal element of Exercise2_8a_R is completely ramified". Is this true ?

Lemma Exercise2_8d r a A: order r -> inc a (substrate r) ->
branched r ->
maximal (sub_order (Exercise2_8a_R r a)) A
-> ramifiedc (induced_order r A).
Proof.
move=> or asr br [As mz]; rewrite (proj2 (sub_osr _)) in As.
have aux: forall x, inc x (Exercise2_8a_R r a) -> sub A x-> x = A.
move=> x xs xA; apply: mz; apply /sub_gleP; split => //.
move: (As) => /Zo_hi [rA _].
move: As; rewrite (Exercise2_8b _ _ or); move => [p1 p2 p3 p4].
split => // [][b] []; aw => bA bm.
move: br => [_ br1].
move: (br1 _ (p1 _ bA)) => [c [d [bc bd bcd]]].
Abort.

TODO: Give an example of a branched set which is not ramified. The branched set defined in Exercise 1.24 (c) is completely ramified.
(d) Let E be a set in which each interval interval_uc c is totally ordered. Show that E has an antidirected cofinal subset

Exercise 2.9; An ordinal sum is well-ordered if and only if I and each Ei is well-ordered. We have shown one half in the main text. For the converse we must assume all Ei nonempty.

Lemma orsum_wo_P r g:
orsum_ax r g -> orsum_ax2 g ->
(worder (order_sum r g) <->
(worder r /\ (forall i, inc i (domain g) -> worder (Vg g i)))).
Proof.
move=> oa alne; move:(oa) =>[or sr alog].
split; last by move=> [p1 p2]; apply: orsum_wor => //.
move=> [or1 wor]; split.
split => //; move=> x xsr [w wx].
set (y := fun_image x (fun z => (J (rep (substrate (Vg g z))) z))).
have ys: (sub y (substrate (order_sum r g))).
rewrite orsum_sr // => t /funI_P.
move => [z zx ->]; have zdg: inc z (domain g) by rewrite - sr; apply: xsr.
by apply: disjoint_union_pi1 => //; apply: rep_i; apply: alne.
have ney: nonempty y.
by exists (J (rep (substrate (Vg g w))) w); apply /funI_P; ex_tac.
move: (wor _ ys ney) => [z []]; aw; move => zy zle.
have Qzx: (inc (Q z) x) by move: zy => /funI_P[t tx ->]; aw.
exists (Q z); red; aw; split => //; move=> t tx;apply /iorder_gleP => //.
have py: (inc (J (rep (substrate (Vg g t))) t) y)
by apply /funI_P;aw; ex_tac.
move: (zle _ py) => le1; move: (iorder_gle1 le1) => le2.
move: (orsum_gle_id oa le2); aw.
move=> i idg; split; first by apply: alog.
move=> x xsr [w wx].
set (y := fun_image x (fun z => (J z i))).
have ysr: (sub y (substrate (order_sum r g))).
move => t /funI_P [z zx ->].
by rewrite orsum_sr //;apply: disjoint_union_pi1 => //; apply: xsr.
have ney: (nonempty y) by exists (J w i); apply /funI_P; ex_tac.
move: (wor _ ysr ney) => [z []]; aw => zy zle.
move: (zy);move=> /funI_P [t tx zt].
have Px: (inc (P z) x) by rewrite zt; aw.
exists (P z); red; aw;last by apply: alog.
split => //; move=> s sx; apply /iorder_gleP => //.
have py: (inc (J s i) y) by apply /funI_P; ex_tac.
move: (iorder_gle1(zle _ py)) => /orsum_gleP [_ _ ].
by rewrite /order_sum_r zt /glt; aw; case; case.
Qed.

Exercise 2.10: proved in the main text
Exercise 2.11; A lexicographic product is well-ordered if the index is finite and each factor is well-ordered; We show here the converse. First: a striclty decreasing function between well-ordered sets has finite source

Lemma worder_decreasing_finite r r' f:
worder r -> worder r' ->
(forall i, inc i (substrate r) -> inc (f i) (substrate r')) ->
(forall i j, glt r i j -> glt r' (f j) (f i)) ->
finite_set (substrate r).
Proof.
move=> wor [or' wor'] ta finc.
have lex: (forall X, sub X (substrate r) -> nonempty X ->
exists2 a, inc a X & forall b, inc b X -> gle r b a).
move=> X Xsr [w wx]; set (Y := fun_image X f).
have Ysr: (sub Y (substrate r')).
by move => T /funI_P [z zX ->]; apply: ta; apply: Xsr.
have neY: (nonempty Y) by exists (f w); apply /funI_P; ex_tac.
move: (wor' _ Ysr neY) => [z []]; aw => zY zle.
move: zY => /funI_P [t tX zt].
ex_tac; move=> b bX.
have fbY: (inc (f b) Y) by apply /funI_P; ex_tac.
move: (zle _ fbY)=> le1; move: (iorder_gle1 le1); rewrite zt => le2.
move: (worder_total wor) => [or tor].
case: (equal_or_not t b) => tb; first by rewrite tb; order_tac; apply: Xsr.
case: (tor _ _ (Xsr _ bX) (Xsr _ tX)) => // tb1.
have ltb: (glt r t b) by split.
move:(finc _ _ ltb) => le3; order_tac.
move: Bnat_order_wor=> [wob bsr].
case: (isomorphism_worder wob wor) => [] [g [[sr isg] _]].
move: (order_morphism_fi isg) => [_ ig].
move: isg => [or _ [fg sg tg] incfg].
have sg1: source g = Bnat by rewrite sg bsr.
move: sr => [sr1 sr2].
have nerg: (nonempty (range (graph g))).
exists (Vf g \0c); Wtac; rewrite sg1; fprops.
case: (lex _ sr1 nerg) => [x p1 p2].
move: p1 => /(range_fP fg) [x1 x1g x1p].
rewrite sg1 in incfg x1g ig.
have p3: (inc (succ x1) Bnat) by apply: BS_succ.
move: (card_lt_succ x1g) => [le1 ne1]; case: ne1; apply: (ig _ _ x1g p3).
have or1: order r by move: wor => [ok _].
apply: (order_antisymmetry or1).
rewrite -incfg ? sg1 => //; apply /Bnat_order_leP; split;fprops.
rewrite -x1p; apply: p2; Wtac; rewrite sg1; fprops.
move: (order_morphism_fi isg) => ig.
move: isg => [or _ [fg sg tg] incfg].
case: (well_ordered_segment wob sr); last first.
rewrite bsr - sg; move=> [a ab rg].
have: (finite_set (range (graph g))).
by rewrite rg segment_Bnat_order //; apply :finite_Bint.
rewrite /finite_set.
by move: (equipotent_range ig) =>/card_eqP; move => ->.
rewrite bsr in tg |- * => img.
move: (@sub_refl (substrate r)) => srr.
case: (emptyset_dichot (substrate r)) => sre.
rewrite sre; apply: emptyset_finite.
move: (lex _ srr sre) => [a asr ab].
have wab: (inc (Vf g a) Bnat) by Wtac.
have : (inc (succ (Vf g a)) Bnat) by fprops.
rewrite -img => /(range_fP fg) [b bsg wba].
rewrite sg in bsg incfg; move: (ab _ bsg); rewrite incfg ? sg//.
move/Bnat_order_leP => [p1 p2]; rewrite -wba.
by move: (card_lt_succ wab) => p3 p4; co_tac.
Qed.

easy part: if the product is totally ordered, or well-ordered so is each factor. By assumption the index set is well-ordered
Section Exercise2_11.
Variables (r g: Set).
Hypothesis oa: orprod_ax r g.

Lemma orprod_total2: orsum_ax2 g ->
((total_order (order_prod r g) -> (allf g total_order))
/\
(worder (order_prod r g) -> (forall i, inc i (domain g) -> worder (Vg g i)))).
Proof.
move=> alne.
move: (oa) => [wor sr pa].
pose f i t := Lg (domain g) (fun j => Yo (j = i) t (rep (substrate (Vg g j)))).
have aux:forall i t, inc t (substrate (Vg g i)) ->
inc (f i t) (substrate (order_prod r g)).
move=> i t ts;rewrite orprod_sr //.
rewrite /f; aw;apply /prod_of_substratesP;split => //; bw;fprops.
by move => j jdg; bw; Ytac ji; [ ue | apply: rep_i; apply: alne].
have aux2: forall i t1 t2, inc i (domain g) -> inc t1 (substrate (Vg g i)) ->
inc t2 (substrate (Vg g i)) -> gle (order_prod r g) (f i t1) (f i t2)
-> gle (Vg g i) t1 t2.
move=> i t1 t2 idg t1s t2s /(orprod_gleP oa) [_ _ h].
move: (pa _ idg) => oi; case: h.
move=> eq; move: (f_equal (Vg^~ i) eq); rewrite /f; bw; Ytac0; Ytac0.
by move=> ->; order_tac.
rewrite sr; move=> [j [jsr j1 j2]]; move: j1; rewrite /f /glt; bw.
by Ytac ji; Ytac0; rewrite ? ji; case.
split.
move=> [or tor] i idg;move: (pa _ idg) => oi; split => //.
move=> x y xsr ysr.
by case: (tor _ _ (aux i _ xsr) (aux i _ ysr)) => h;
[left | right ]; apply: aux2.
move=> [or1 wor1].
move=> i idg; move: (pa _ idg) => oi; split => //.
move=> x xsr [w wx].
set (X:= fun_image x (f i)).
have Xs: (sub X (substrate (order_prod r g))).
by move=> t /funI_P [z zx ->];apply: aux; apply: xsr.
have neX: (nonempty X) by exists (f i w); apply /funI_P; ex_tac.
move: (wor1 _ Xs neX) => [y []]; aw => yX yle.
move: yX => /funI_P [z zx fz]; exists z;red; aw;split => //.
move=> t tx.
have ft: (inc (f i t) X) by apply /funI_P; ex_tac.
apply /iorder_gleP => //.
aw; move: (yle _ ft); rewrite fz => le3; move: (iorder_gle1 le3) => le4.
by apply: aux2 => //; apply: xsr.
Qed.

Assume no factor empty; then the product is totally ordered iff each factor is. Assume moreover that each factor has at least two elements. We can then construct two elements in the product such that f(i) < g(i) for any i. Let h_j the function that is f(i) or g(i) depending on how i compares to j; this is a stricty decreasing function; if the product is well-ordered it implies that the index set is empty.

Lemma orprod_total3P: orsum_ax2 g ->
( (allf g total_order) <-> total_order (order_prod r g)).
Proof.
move=> alne; split; first by apply: orprod_total => //.
by case: (orprod_total2 alne).
Qed.

Lemma orprod_total4:
total_order (order_prod r g) ->
(forall i, inc i (domain g) -> ~ (small_set (substrate (Vg g i)))) ->
exists f1 f2,
[/\ inc f1 (substrate (order_prod r g)),
inc f2 (substrate (order_prod r g)) &
forall i, inc i (domain g) -> glt (Vg g i) (Vg f1 i) (Vg f2 i)].
Proof.
move=> tor ns.
have p1: forall i, inc i (domain g) -> exists x y,
[/\ inc x (substrate (Vg g i)), inc y (substrate (Vg g i)) & x <> y].
move => i idg; move: (ns _ idg); set t:= substrate (Vg g i) => ts.
case: (emptyset_dichot t) => te; first by case: ts; move=> u v ue; empty_tac1 u.
move: te=> [x xe]; exists x; ex_middle ep.
case: ts; move=> u v ut vt; transitivity x.
by symmetry; ex_middle xu; case: ep; exists u.
by ex_middle xv;case: ep; exists v.
have alne:(forall i, inc i (domain g) -> nonempty (substrate (Vg g i))).
by move=> i idg; move: (p1 _ idg) => [x [ _ [xs _ _]]]; exists x.
move: tor; rewrite -(orprod_total3P alne) => tor.
set (f0 := fun i => choose (fun z => glt (Vg g i) (P z) (Q z))).
have f0p: (forall i, inc i (domain g) -> glt (Vg g i) (P (f0 i)) (Q (f0 i))).
move=> i idg; apply choose_pr.
move: (p1 _ idg)(tor _ idg) => [x [y [xs ys xy]]] [oi tori].
case: (tori _ _ xs ys) =>lxy.
by exists (J x y); rewrite /glt; aw.
exists (J y x); rewrite /glt; aw; split;fprops.
exists (Lg (domain g) (fun i=> (P (f0 i)))).
exists (Lg (domain g)(fun i => (Q (f0 i)))).
move: (oa) => [wor sr alo].
rewrite orprod_sr; split => //.
apply: prod_of_substrates_gi => i idg; move: (f0p _ idg) => h; order_tac.
apply: prod_of_substrates_gi => i idg; move: (f0p _ idg) => h; order_tac.
move => i idg; bw; exact: (f0p _ idg).
Qed.

Lemma ordprod_worder_bisP:
(forall i, inc i (domain g) -> ~ (small_set (substrate (Vg g i)))) ->
( ( allf g worder /\ finite_set (substrate r))
<-> worder (order_prod r g)).
Proof.
move=> ad; move: (oa) => [wor sr alo]; split.
move=> [p1 p2]; apply: orprod_wor => //.
move=> wop.
move: (orprod_total4 (worder_total wop) ad) => [f1 [f2 [f1s f2s f12]]].
split.
have p1: (forall i, inc i (domain g) -> nonempty (substrate (Vg g i))).
move=> i idg; move: (f12 _ idg); exists (Vg f1 i); order_tac.
by move: (orprod_total2 p1) => [_]; apply.
set (f := fun i => Lg (domain g)
(fun z => Yo (glt r z i) (Vg f1 z) (Vg f2 z))).
have fs: (forall i, inc i (domain g) -> inc (f i) (substrate (order_prod r g))).
move=> i idg; rewrite orprod_sr // /f; aw.
apply: prod_of_substrates_gi.
move=> j jdg; bw; move: (f12 _ jdg) (alo _ jdg) => le2 o2.
Ytac ca; order_tac.
rewrite - sr in fs; apply: (worder_decreasing_finite wor wop fs).
move=> i j ij.
have isr: (inc i (substrate r)) by order_tac.
have jsr: (inc j (substrate r)) by order_tac.
have idg: (inc i (domain g)) by ue.
have jdg: (inc j (domain g)) by ue.
have aux: ~ glt r i i by case.
have aux1: glt (Vg g i) (Vg (f j) i) (Vg (f i) i).
by rewrite /f; bw; Ytac0; Ytac0; apply: f12.
split; last first.
by move: aux1 => [_ neq1]; dneg eq1; rewrite eq1.
rewrite orprod_sr // in fs.
apply /(orprod_gleP oa) ; split => //; try (apply: fs => //).
right; exists i; split => //; move=> k ki.
have kdg: (inc k (domain g)) by rewrite - sr; order_tac.
have kj: glt r k j by move: wor => [or _];order_tac.
by rewrite /f; bw; Ytac0; Ytac0.
Qed.

End Exercise2_11.

Exercise 2.12; Study of lexciographic product.
Lemma: A subset of the union of two well-ordered sets in a totally ordered set is well-ordered

Lemma union2_wor r A B C:
total_order r -> sub A (substrate r) -> sub B (substrate r) ->
sub C (A \cup B) ->
worder (induced_order r A) ->worder (induced_order r B) ->
worder (induced_order r C).
Proof.
move => [or tor] Asr Bsr cab [or1 wo1] [or2 wo2].
have cs: sub C (substrate r).
by move => t tc;move:(cab _ tc);case /setU2_P => h; [apply: Asr| apply: Bsr].
move:(iorder_osr or Asr)(iorder_osr or Bsr)(iorder_osr or cs).
move=>[oA sA][oB sB][oC sC].
split => //; rewrite sC => X XC neX.
rewrite sA in wo1; rewrite sB in wo2.
have Xp: X = (X \cap A) \cup (X \cap B).
set_extens t; last by case /setU2_P => /setI2_P [].
move => tX; move: (cab _ (XC _ tX)).
case /setU2_P => h; apply /setU2_P; [left | right]; fprops.
rewrite (iorder_trans _ XC).
case: (emptyset_dichot (X \cap A)) => ne1.
have XB: sub X B.
rewrite Xp ne1;move => t; case /setU2_P; first by move/in_set0.
by move => /setI2_P [].
by move:(wo2 _ XB neX); rewrite (iorder_trans _ XB).
case: (emptyset_dichot (X \cap B)) => ne2.
have XA: sub X A.
rewrite Xp ne2;move => t; case /setU2_P; first by move => /setI2_P [].
by move /in_set0.
by move:(wo1 _ XA neX); rewrite (iorder_trans _ XA).
have pc: sub (X \cap A) A by apply: subsetI2r.
have pd: sub (X \cap B) B by apply: subsetI2r.
move: (wo1 _ pc ne1)(wo2 _ pd ne2).
rewrite (iorder_trans _ pc) (iorder_trans _ pd).
move: (sub_trans XC cs) => qa.
move: (sub_trans pc Asr) => qb.
move: (sub_trans pd Bsr) => qc.
move => [a ap][b bp]; move: ap bp; rewrite /least; aw.
move => [] /setI2_P [aX aA] al [] /setI2_P [bX bB] bl.
have [c [cX ca cb]]: exists c, [/\ inc c X, gle r c a & gle r c b].
case: (tor _ _ (Asr _ aA)(Bsr _ bB)) => aux.
exists a; split => //; order_tac; exact (Asr _ aA).
exists b; split => //; order_tac; exact (Bsr _ bB).
exists c;split => //; move => x xX; apply /iorder_gleP => //.
move: xX; rewrite Xp => /setU2_P; case => h.
move: (al _ h) => h1; move: (iorder_gle1 h1) => h2; order_tac.
move: (bl _ h) => h1; move: (iorder_gle1 h1) => h2; order_tac.
Qed.

Assumptions I is an index set, totally ordered by r; E(i) is a family g of ordered sets, and E is the product. If x and y are in E then olex_nsv x y is the set of indices on which x and y differ. We say x<y is this set is well-ordered and x(i)<y(i) when i is the least element.

Definition olex_nsv r x y:= Zo (substrate r) (fun i => (Vg x i <> Vg y i)).
Definition olex_io r x y:= (induced_order r (olex_nsv r x y)).

Definition olex_comp1_r r g x y :=
worder (olex_io r x y) /\
let i := the_least (olex_io r x y) in glt (Vg g i) (Vg x i) (Vg y i).
Definition olex_comp2_r r g x y :=
[/\ (inc x (prod_of_substrates g)),
(inc y (prod_of_substrates g)) &
(x = y \/ olex_comp1_r r g x y) ].

Definition olex r g := graph_on (olex_comp2_r r g) (prod_of_substrates g).
Definition olex_ax r g:=[/\ total_order r,substrate r = domain g & order_fam g].

Lemma olex_nsvS r x y: olex_nsv r x y = olex_nsv r y x.
Proof.
by set_extens t; move => /Zo_P [pa pb]; apply /Zo_P; split => //; apply:nesym.
Qed.

Lemma olex_ioS r x y: olex_io r x y = olex_io r y x.
Proof. by rewrite /olex_io olex_nsvS. Qed.

This relation is an ordering of E
Section Olex_basic.
Variables (r g: Set).
Hypothesis ax: olex_ax r g.

Lemma olex_R x:
inc x (prod_of_substrates g) -> olex_comp2_r r g x x.
Proof. by move => h; split => //; left. Qed.

Lemma olex_gleP x y: gle (olex r g) x y <-> olex_comp2_r r g x y.
Proof.
split; first by move /Zo_hi; aw.
move =>h;apply Zo_i;last by aw.
by move: h => [pa pb _]; apply : setXp_i.
Qed.

Lemma olex_nsve x y:
inc x (prod_of_substrates g) -> inc y (prod_of_substrates g) ->
((x = y) <-> (olex_nsv r x y = emptyset)).
Proof.
move=> px py;split.
by move => ->; apply /set0_P=> t /Zo_P [pa]; case.
have pd: order_fam g by move: ax=> [_ _].
have sd: substrate r = domain g by move: ax => [_].
move=> oe; move: px => /prod_of_substratesP [ra rb _].
move: py => /prod_of_substratesP [rd re _].
apply: fgraph_exten =>//; first by ue.
by rewrite rb - sd => z zd; ex_middle sv; empty_tac1 z; apply /Zo_P.
Qed.

Lemma olex_nsve1 x y:
inc x (prod_of_substrates g) -> inc y (prod_of_substrates g) ->
let r' := (olex_io r x y) in let i := the_least r' in
x <> y -> worder r' -> least r' i.
Proof.
move => px py r' i pa pb.
have or: order r by move: ax => [[ok _]_ ].
have pc: sub (olex_nsv r x y) (substrate r) by apply: Zo_S.
have sr': substrate r' = olex_nsv r x y by rewrite /r' iorder_sr.
have nse: nonempty (substrate r').
by rewrite sr'; apply /nonemptyP; move /(olex_nsve px py).
move: (worder_least pb nse) => [j jl].
move: (pb) => [qa1 _];move: (the_least_pr2 qa1 jl).
by rewrite /i; move => ->.
Qed.

Lemma olex_glt_aux x y: glt (olex r g) x y ->
let r' := (olex_io r x y) in
let i := the_least r' in
(inc i (substrate r) /\ forall j, glt r j i -> Vg x j = Vg y j).
Proof.
move => [h nxy] r' i.
move:h => /olex_gleP [pa pb]; case => pc; first by contradiction.
move: pc => [wor]; move: (olex_nsve1 pa pb nxy wor); simpl.
rewrite -/i; move => [pc pd] pe.
have or: order r by move: ax => [[ok _]_ ].
have pf: sub (olex_nsv r x y) (substrate r) by apply: Zo_S.
have sr': substrate r' = olex_nsv r x y by rewrite /r' iorder_sr.
have pg: inc i (substrate r) by apply: pf; rewrite - sr'.
split => //.
move => k ki; ex_middle aux.
have kp: inc k (substrate r') by rewrite sr' ; apply:Zo_i => //; order_tac.
move: (pd _ kp); rewrite /r' => aux1; move: (iorder_gle1 aux1) => aux2.
order_tac.
Qed.

Lemma olex_sr: substrate (olex r g) = (prod_of_substrates g).
Proof. by rewrite /olex graph_on_sr // => x; apply: olex_R. Qed.

Lemma olex_osr: order_on (olex r g) (prod_of_substrates g).
Proof.
split => //; last by apply:olex_sr.
move: (ax) => [[or tor] _ _].
have sd: substrate r = domain g by move: ax => [_].
apply: order_from_rel; split => //; last first.
by move => x y [pa pb _];split; apply: olex_R.
move=> x y => pa