proposition: Lemma Exercise4_8v K: all_uncomp_inP K -> exists x, inc x (substrate r) /\ (cardinal K) <=c (cardinal (minimals x)).
proof: Proof. move=> [kp1 kp2]. pose c x := K -s1 x. have Ks: sub K (substrate r). by move => t tk;move: (kp1 _ tk) =>/setC1_P [] /Zo_P []. have cp: forall x, inc x K -> sub (c x) (substrate r). by rewrite /c => x xK t /setC1_P [tK _]; apply: Ks. pose f x:= supremum r (c x). set u := supremum r K. have fpr0: forall x, inc x K -> least_upper_bound r (c x) (f x). by move => x xK;move: (supremum_pr1 (proj1 lr) (Exercise4_7i(cp _ xK))). have fpr1: forall x, inc x K -> u = sup r (f x) x. move => x xK; move: (cp _ xK) => asr. move: (supremum_setU1 lr asr (Exercise4_7i asr) (Ks _ xK)). by rewrite {1} /c (setC1_K xK). move: lr => [or _]. have fpr2: forall x, inc x K -> glt r (f x) u. move => x xK;move: (cp _ xK) => csr; move: (fpr0 _ xK). move => /(lubP or csr) [[fs1 _] _]. move: (lattice_sup_pr lr fs1 (Ks _ xK)) => [p1 p2 p3]. split; first by rewrite (fpr1 _ xK); apply: p1. move=> fxu; rewrite -(fpr1 _ xK) -fxu in p2. have six: sup_irred r x. by move: (kp1 _ xK) => /setC1_P [] /Zo_P []. have Kir: sub K (irreds r) by apply: (@sub_trans E48P) => //; apply: sub_setC. have cir: sub (c x) (irreds r). apply: (@sub_trans K) => //; apply: sub_setC. case: (emptyset_dichot (c x)) => ec; last first. move: (Exercise4_8c1 (Ks _ xK) six cir p2 ec). by move=> [v ] /setC1_P [vK vx] xv;case: vx; move: (kp2 _ _ xK vK xv). move: (fpr0 _ xK); rewrite ec lub_set0 // fxu => lu. have Ksx: K = singleton x. by apply: set1_pr => // t tk; ex_middle tx; empty_tac1 t; apply /setC1_P. move: (supremum_singleton or (Ks _ xK)); rewrite -Ksx -/u => ux. move: (kp1 _ xK) => /setC1_P [_]; case. move: (the_least_pr or Exercise4_7c) => ol. by apply: (unique_least or) => //; rewrite - ux. have fpr3: forall x y, inc x K -> inc y K -> x <> y -> gle r x (f y). move => x y xK yK xy; move: (cp _ yK) => cK; move: (fpr0 _ yK). by move=> /(lubP or cK) [[_ ub] _]; apply: ub; apply /setC1_P. have fpr4: forall x y, inc x K -> inc y K -> x <> y -> sup r (f x) (f y) = u. move=> x y xK yK xy. move: (fpr2 _ xK) (fpr2 _ yK) => [p1 _] [p2 _]. have fxs: inc (f x) (substrate r) by order_tac. have fys: inc (f y) (substrate r) by order_tac. move: (lattice_sup_pr lr fxs fys) => [p3 p4 p5]. move: (p5 u p1 p2) => p6. have p7: gle r u (sup r (f x) (f y)). rewrite (fpr1 _ xK). move: (lattice_sup_pr lr fxs (Ks _ xK)) => [p3a p4a p5a]. apply: p5a => //; move: (fpr3 _ _ xK yK xy) => aux; order_tac. order_tac. have fpr5: forall x y, inc x K -> inc y K -> f x = f y -> x = y. move=> x y xK yK sf; ex_middle xny; move: (fpr2 _ xK) => [ _ ]; case. have fxs:inc (f x) (substrate r) by move: (fpr2 _ xK) => xx; order_tac. by move: (fpr4 _ _ xK yK xny); rewrite /sup - sf supremum_singleton. set L := fun_image K f. have lp1: sub L (substrate r). move=> t /funI_P [z zK ->]; move: (fpr2 _ zK) => xx; order_tac. have ->: cardinal K = cardinal L. apply /card_eqP. exists (Lf f K L); saw ;apply: lf_bijective; aw; trivial. move=> t tK; apply /funI_P; ex_tac. by move=> y /funI_P. pose d x := L -s1 x. have dp: forall x, inc x L -> sub (d x) (substrate r). by rewrite /d => x xK t /setC1_P [tK _]; apply: lp1. pose g x:= infimum r (d x). set v := infimum r L. have lp2: forall x, inc x L -> greatest_lower_bound r (d x) (g x). by move => x xK;move: (infimum_pr1 or (Exercise4_7i1 (dp _ xK))). have lp3: forall x, inc x L -> v = inf r (g x) x. move => x xK; move: (dp _ xK) => asr. move: (infimum_setU1 lr asr (Exercise4_7i1 asr) (lp1 _ xK)). by rewrite {1} /d (setC1_K xK). have lp4: forall x, inc x L -> glt r v (g x). move => x xL;move: (dp _ xL) => csr; move: (lp2 _ xL). move /(glbP or csr) => [[fs1 _] _]. move: (lattice_inf_pr lr fs1 (lp1 _ xL)) => [p1 p2 p3]. split; first by rewrite (lp3 _ xL); apply: p1. move=> gxv; rewrite -(lp3 _ xL) gxv in p2. move: (sup_comparable1 or p2); rewrite sup_C. rewrite (distributive_rec (lp1 _ xL) csr). set aux2 := fun_image _ _. case: (emptyset_dichot (d x)) => de. have -> : aux2 = emptyset. by apply /set0_P => y; rewrite /aux2 de => /funI_P [z /in_set0]. move: (the_greatest_pr or Exercise4_7c1) => ol. move: xL => /funI_P [z zK fz] ie. move: (fpr2 _ zK) ol;rewrite -Exercise4_8u ie fz; move => lt [_ xv]. have usr: inc u (substrate r) by order_tac. by move: (xv _ usr) => le2; order_tac. move: de => [y yd]. have: inc (sup r y x) aux2 by apply /funI_P;ex_tac. move: yd xL => /setC1_P [] /funI_P [z1 z1k eq1] yx /funI_P [z2 z2K eq2]. have nz12: z1 <> z2 by dneg z12; rewrite eq1 eq2; ue. rewrite eq1 eq2 fpr4 // => ua. have ->: aux2 = singleton u. apply: set1_pr => // t /funI_P [z zd ->]. move : zd => /setC1_P [] /funI_P [s sk fs3] zx. by rewrite fs3 eq2; apply fpr4 => // => h; case: zx; rewrite fs3 h. move: (fpr2 _ z2K) => [lt2 ne2]. have usr: inc u (substrate r) by order_tac. by rewrite -/(inf r u u) inf_comparable1=> //; [ apply:nesym | order_tac]. have lp5: forall x y, inc x L -> inc y L -> x <> y -> gle r (g y) x. move => x y xL yL xy; move: (dp _ yL) => cL; move: (lp2 _ yL). move=> /(glbP or cL) [[_ ub] _]; apply: ub; apply /setC1_P;split => //. have lp6: forall x y, inc x L -> inc y L -> x <> y -> inf r (g x) (g y) = v. move=> x y xL yL xy. move: (lp4 _ xL) (lp4 _ yL) => [p1 _] [p2 _]. have fxs: inc (g x) (substrate r) by order_tac. have fys: inc (g y) (substrate r) by order_tac. move: (lattice_inf_pr lr fxs fys) => [p3 p4 p5]. move: (p5 v p1 p2) => p6. have p7: gle r (inf r (g x) (g y)) v. rewrite (lp3 _ xL). move: (lattice_inf_pr lr fxs (lp1 _ xL)) => [p3a p4a p5a]. apply: p5a => //; move: (lp5 _ _ xL yL xy) => aux; order_tac. order_tac. pose h x := choose (fun a => gle r a (g x) /\ minimal_in_int v a). have lp7: forall x, inc x L -> (gle r (h x) (g x) /\ minimal_in_int v (h x)). move=> x xL; apply choose_pr. set U:= Zo (substrate r) (fun a => glt r v a /\ gle r a (g x)). have Usr: sub U (substrate r) by apply: Zo_S. have neU: nonempty U. move:(lp4 _ xL) => lt1;exists (g x); apply: Zo_i=> //;try order_tac. split => //; order_tac; order_tac. move: (finite_set_minimal1 Usr neU) => [a aU etc]. move: aU => /Zo_P [a1 [a2 a3]]. exists a; split => //; split => // b bv ba. apply: etc => //; apply: Zo_i => //; try split => //; order_tac. set M := fun_image L h. have Mm: sub M (minimals v). move=> t /funI_P [z zL ->]; move: (lp7 _ zL) => [p1 p2]. apply: Zo_i => //; order_tac. have ->: cardinal L = cardinal M. apply /card_eqP; exists (Lf h L M); saw; apply: lf_bijective. move=> t tL; apply /funI_P; ex_tac. move => a b aL bL sh. move: (lp7 _ aL) (lp7 _ bL) => [p1 [p2 p3]] [p4 [p5 p6]]. ex_middle nab;rewrite - sh in p4. have gasr: inc (g a) (substrate r) by order_tac. have gbsr: inc (g b) (substrate r) by order_tac. move: (lattice_inf_pr lr gasr gbsr)=> [g1 g2 g3]. move: (g3 _ p1 p4); rewrite (lp6 _ _ aL bL nab) => g4;order_tac. by move=> y /funI_P. exists v;split => //; last by apply: sub_smaller. by move: (infimum_pr1 or (Exercise4_7i1 lp1)) => /(glbP or lp1) [[ok _] _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)