proposition: Lemma Exercise1_18d E X Y (r := coarser E): gle r Y X -> exists X', [/\ inc X' (substrate r), inf r X X' = Y & sup r X X' = greatest_partition E].
proof: Proof. move=> lYX; move: (lYX). move /coarser_gleP => [py px cyx]. move: (px)(py) => [[px1 px3] px2] [[py1 py3] py2]. set (X1 := Zo (\Po E) (fun z=> exists2 a, z = singleton a & ~(exists2 u, inc u X & a = rep u))). set X2 := fun_image Y (fun v => Zo E (fun z => exists u, [/\ inc u X, sub u v & z = rep u])). set (Z:=X1 \cup X2). have Hb: forall x a, inc x a-> inc a X -> x <> (rep a) -> inc (singleton x) Z. move=>x a xa aX nrep; apply /setU2_1. apply: Zo_i; first by apply /setP_P => w /set1_P ->; rewrite -px1;union_tac. exists x => //; move=> [w wx tr]. have xw: (inc x w) by rewrite tr; apply: rep_i; apply: px2. case: (px3 _ _ aX wx) => aw; first by case: nrep; ue. by red in aw; empty_tac1 x. have pz: (partition_s Z E). split; last first. move=> a; case/setU2_P. move /Zo_P => [_ [u ua _]];rewrite ua; exists u; fprops. move /funI_P => [v vy ->]; move: (py2 _ vy) => [x xv]. have : inc x E by rewrite -py1; union_tac. rewrite -px1; move=> /setU_P [u xu uX]. move: (rep_i (px2 _ uX)) (cyx _ uX) => ru [w wY uW]. case: (py3 _ _ vy wY) => vw; last by empty_tac1 x. exists (rep u); apply: Zo_i; [ union_tac | exists u;split => //; ue]. split; first set_extens x. move=> /setU_P [u xu]; case/setU2_P. by move /Zo_P => [] /setP_P uE _; apply: uE. by move=> /funI_P [v vy vw];move: xu; rewrite vw => /Zo_P [te _]. move=> xE;move: (xE); rewrite -px1=> /setU_P [a xa aX]; apply /setU_P. case: (equal_or_not x (rep a)) => xrep; last first. exists (singleton x); fprops; apply: (Hb _ _ xa aX xrep). move: (cyx _ aX)=> [b bY ab]. set (w:= Zo E (fun z => exists u, [/\ inc u X, sub u b & z = rep u])). have tw: (inc x w) by apply: Zo_i => //; exists a. by exists w => //; apply: setU2_2; apply /funI_P; exists b. move=> a b; case/setU2_P=> h1; case/setU2_P => h2. + move: h1 h2 => /Zo_hi [u au _] /Zo_hi [v bv _]. rewrite au bv; case: (equal_or_not u v) => uv; first by left;ue. by right; apply: disjoint_pr; move=> w /set1_P -> /set1_P. + move: h1 h2 => /Zo_P [aE [x ax nev]] /funI_P [z zY bv]. right; apply: disjoint_pr => u; rewrite ax bv => /set1_P ->. move /Zo_P => [xE [w [wX wz rw]]]; case: nev; ex_tac. + move: h2 h1 => /Zo_P [aE [x ax nev]] /funI_P [z zY bv]. right; apply: disjoint_pr => u; rewrite ax bv. move /Zo_P=> [xE [w [wX wz rw]]] /set1_P => h;case: nev; ex_tac; ue. + move: h1 h2 => /funI_P [x xY av] /funI_P [y yY bv]. rewrite av bv. case: (py3 _ _ xY yY); first by move=> xy; left; rewrite xy. rewrite {1} /disjoint;move=> dixy; right; apply: disjoint_pr. move=> u => /Zo_P [uE [c [cX cx ur]]] /Zo_P [_ [d [dX dx ur']]]. move: (rep_i (px2 _ cX))(rep_i (px2 _ dX)). rewrite -ur -ur' => uc ud; empty_tac1 u. have lr: lattice (coarser E). move: (Exercise1_18a E) => [cl1 cl2]. by split => // u v uE vE;apply: cl2; move=> t; case/set2_P => ->. move: (coarser_osr E) => [or sr]. have auxP: forall u, inc u (substrate r) <-> partition_s u E. by move=> u; rewrite sr; apply: partitionsP. have Xs: inc X (substrate r) by apply /auxP. have Ys: inc Y (substrate r) by apply /auxP. have Zs: inc Z (substrate r) by apply /auxP. exists Z; split; first by exact. move: (lattice_inf_pr lr Xs Zs); rewrite -/r; move => [i1 i2 i3]. have YZ: gle r Y Z. apply /coarser_gleP; split => // t /setU2_P; case. move=> /Zo_P [] /setP_P tE [a ta ap]. have: inc a E by apply: tE; rewrite ta; fprops. rewrite -py1 => /setU_P [y ay yY]. by exists y => //; rewrite ta; apply: set1_sub. move=> /funI_P [z zY tv]; ex_tac;rewrite tv; move=> u /Zo_P. move => [uE [v [vX vz ur]]]; apply: vz; rewrite ur. apply: (rep_i (px2 _ vX)). move: (i3 _ lYX YZ) => Yi. apply: (order_antisymmetry or); last by exact. move: i1 i2 => /coarser_gleP [p1 _ le1] /coarser_gleP [_ _ le2]. apply/coarser_gleP;split => // a aY. set (z:= Zo E (fun z => exists u, [/\ inc u X, sub u a & z = rep u])). have zz: (inc z Z) by apply: setU2_2; apply /funI_P; ex_tac. move: (le2 _ zz) => [b bi zb]; ex_tac => t ta. have tE: (inc t E) by rewrite -py1; union_tac. move: (tE);rewrite -px1 => /setU_P [c tc cX]. move: (cyx _ cX) => [d dY cd]. case: (py3 _ _ aY dY) => ad; last by empty_tac1 t. rewrite -ad in cd; clear dY ad d. move: (rep_i (px2 _ cX)) => rd1. have rcb: inc (rep c) b. by apply: zb; apply: Zo_i; [rewrite -px1;union_tac | ex_tac]. move: (le1 _ cX) => [d di db]. case: (proj2 (proj1 p1) _ _ bi di); first by move=> ->; apply: db. move => bd; empty_tac1 (rep c). rewrite intersection_is_sup2_b //. have Ha: forall a w, inc a X -> inc w X2 -> nonempty (a \cap w) -> a \cap w = (singleton (rep a)). move=> a b aX /funI_P [v vY bv] [q qt]. apply: set1_pr1; first by ex_tac. rewrite bv => w /setI2_P [wa]/Zo_P [wE [c [cX cb wr]]]. case: (px3 _ _ aX cX); first by move=> ->. move=> di; empty_tac1 (rep c); [ ue | apply: (rep_i (px2 _ cX))]. set_extens t. move /setC1_P => [] /setI_covering2_P [a [b [aX bZ ti]]] /nonemptyP net. apply /funI_P; case/setU2_P: bZ. move /Zo_P=>[bE [c bs _]]. have cb: inc c b by rewrite bs; fprops. move/setP_P : bE => bE; move: (bE _ cb) => cE; ex_tac. by apply: (set1_pr1 net); rewrite - ti bs => u /setI2_P [_] /set1_P. rewrite -ti in net;move => bX2; move: (Ha _ _ aX bX2 net) => wi. rewrite -ti wi -px1; exists (rep a)=> //; apply: (@setU_i _ a) => //. apply: (rep_i (px2 _ aX)). move /funI_P => [x xE st]. apply/setC1_P; split; last by rewrite st; apply /nonemptyP/set1_ne. apply /setI_covering2_P. move: (xE); rewrite -px1 => /setU_P [a wa aX]. move: (cyx _ aX) => [b bY ab]. case: (equal_or_not x (rep a)) => ra. set (w:= Zo E (fun z => exists u, [/\ inc u X, sub u b & z = rep u])). have wX2: inc w X2 by apply /funI_P; ex_tac. have nei: nonempty (a \cap w). exists (rep a); apply: setI2_i; first by ue. apply: Zo_i; [rewrite -px1 -ra; union_tac | ex_tac]. exists a, w;rewrite (Ha _ _ aX wX2 nei) -ra st;split => //. by apply: setU2_2. exists a, (singleton x); split => //; first by apply: (Hb _ _ wa aX ra). rewrite st setI2_C; apply: set1_pr. by apply /setI2_P;split;fprops. by move => z /setI2_P [] /set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)