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