proposition: Lemma Exercise4_8t x: inc x (substrate r) -> exists K, all_uncomp_inP K /\ K \Eq (minimals x).
proof: Proof. move=> xsr. pose f y := choose (fun z => inc z (E47S r y) /\ ~ inc z (E47S r x)). move: lr => [or _ ]. have fpr: forall y, inc y (minimals x) -> (inc (f y) (E47S r y) /\ ~ inc (f y) (E47S r x)). move=> y ysr; apply choose_pr. move: ysr => /Zo_P [ysr [[xle xney] ymin]]. move: (Exercise4_7k xle) => p1. case: (emptyset_dichot ((E47S r y) -s (E47S r x))) => ne. move: (Exercise4_7m ysr xsr (empty_setC ne)) => yx. case: xney; order_tac. by move:ne => [z] /setC_P aux; exists z. have fpr1: forall y, inc y (minimals x) -> sup r x (f y) = y. move=> y ysm; move: (fpr _ ysm) => [p1 p2]. move: p1 =>/Zo_P [fsr [firr le1]]. move: (lattice_sup_pr lr xsr fsr) => [p3 p4 p5]. have p9: glt r x (sup r x (f y)). split => //; dneg xs; apply: Zo_i => //; split => //; ue. move: ysm => /Zo_P [p6 [p7 p8]]. apply: p8 => //; apply: p5 => //; order_tac. set K:= fun_image (minimals x) f. have KP: sub K E48P. move=> t /funI_P [z zm ->]; move: (fpr _ zm). move => [] /Zo_P [p1 [p2 p3]] p4; apply /setC1_P;split; first by apply: Zo_i. dneg fzl; apply /Zo_P;split => //; split => //; rewrite fzl. by move: (the_least_pr or Exercise4_7c) => [_ tle]; apply: tle. have auK: all_uncomp_inP K. split => // u v /funI_P [y ym ->] /funI_P [z zm ->] le1. move:(fpr _ ym)(fpr _ zm)=> [] /Zo_P [p1 [p2 p3]] p4 [] /Zo_P [p5 [p6 p7]] p8. move: (lattice_sup_pr lr xsr p1) => [_ _ q2]. move: (lattice_sup_pr lr xsr p5) => [q1 q4 _]. have: gle r (sup r x (f y)) (sup r x (f z)) by apply: q2 => //; order_tac. rewrite (fpr1 _ ym) (fpr1 _ zm) => le2. move: ym zm => /Zo_P [r1 [r2 r3]] /Zo_P [r4 [r5 r6]]. by move: (r6 _ r2 le2) => ->. exists K;split => //; apply: EqS;exists (Lf f (minimals x) K);saw. apply: lf_bijective. move => t ts; apply /funI_P; ex_tac. by move=> u v um vm sf; rewrite -(fpr1 _ um) -(fpr1 _ vm) sf. by move=> y /funI_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)