proposition: Lemma Exercise2_7B4 F: cofinal r F -> worder (induced_order r F) -> ~ (has_greatest r) -> nonempty E -> exists u v, [/\ inc u closures, inc v closures & ~ has_supremum closure_ordering (doubleton u v)].
proof: Proof. move => cof wor nge be. move: (Exercise2_7B3 cof wor nge)=> [F1 [F2 [cof1 wor1 cof2 wor2 dis]]]. move:(Exercise2_7B2 cof1 wor1) (Exercise2_7B2 cof2 wor2) =>[u ua ub] [v va vb]. exists u,v; split => //. move: (Exercise2_7b) => [oce sce] hs. move: (ua)(va); rewrite - sce => ua' va'. case: (sup_pr oce ua' va' hs); set w := sup _ _ _ => wa wb _. move/Exercise2_7aP:(wa)=> [_ wc _]. move/(Exercise2_7dP ua wc): wa; rewrite ub => qa. move/(Exercise2_7dP va wc): wb; rewrite vb => qb. move: be => [x xE]. move/Zo_P: wc => [/functionsP [fw sw tw] [qc qd qe]]. have xzf: inc (Vf w x) (fixpoints w). by apply/Zo_P; split; [ rewrite sw; Wtac| apply: qe]. empty_tac1 (Vf w x). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)