proposition: Lemma Exercise2_7B3 F: cofinal r F -> worder (induced_order r F) -> ~ (has_greatest r) -> exists F1 F2, [/\ cofinal r F1, worder (induced_order r F1), cofinal r F2, worder (induced_order r F2) & disjoint F1 F2].
proof: Proof. move => [sfE cof] wo1 nger. move:(iorder_sr or sfE) => sif. pose aux X:= sub X F /\ forall x, inc x F -> exists2 y, inc y X & gle r x y. have Ha X: aux X -> cofinal r X. move => [ss hyp]; split; first by apply: (sub_trans ss sfE). move => t /cof [y /hyp [z za zb] zc]; ex_tac; order_tac. suff: exists F1 F2, [/\ aux F1, aux F2 & disjoint F1 F2]. move => [f1 [f2 [ha hb he]]]; exists f1, f2. move:(Ha _ ha)(Ha _ hb) => cf1 cf2. move: (proj1 ha)(proj1 hb); rewrite - sif => hb' hd'. move:(induced_wor wo1 hb') (induced_wor wo1 hd'). rewrite (iorder_trans _ (proj1 ha)) (iorder_trans _ (proj1 hb)) => hb'' hd''. done. move:(the_ordinal_iso1 wo1)(OS_ordinal wo1); set f := the_ordinal_iso _. set alpha := ordinal _ => isf oa. move: isf =>[ora orf]; rewrite ordinal_o_sr sif; move => [bf sf tf] fiso. move: (proj1 (proj1 bf)) => ff. have alim x: inc x alpha -> inc (osucc x) alpha. move => xa; case: (ordinal_limA oa). - rewrite /ord_zero;move => h; empty_tac1 x. - move => [y oy yv]. have ya: inc y alpha by rewrite yv; fprops. set z := Vf f y; case nger; exists z. have zF: inc z F by rewrite /z; Wtac. have zE: inc z E by exact: (sfE _ zF). split => // t /cof [u ua ub]. rewrite - tf in ua; move: (proj2 (proj2 bf) _ ua) =>[v vsf vv]. rewrite - sf in ya. have le1: gle (ordinal_o alpha) v y. apply/ordo_leP; rewrite - sf; split => //. by move: vsf; rewrite sf yv; apply: ordinal_sub3. move/(fiso v y vsf ya): le1 => /iorder_gle1. rewrite -/z - vv=> le2; order_tac. - by move/limit_ordinal_P => [_ ] h; apply/(oltP oa)/h /(oltP oa). have osa x: inc x alpha -> ordinalp x by apply: Os_ordinal. pose even x := orem x \2o = \0o. pose evena x := inc x alpha /\ even x. pose odda x := inc x alpha /\ ~even x. have ooq x: ordinalp x -> ordinalp (oquo x \2c). move => ox; exact: (proj41 (oquoremP ox olt_02)). have evenp1 x: ordinalp x -> even x -> x = \2o *o oquo x \2o. move => ox ex; move: (proj43 (oquoremP ox olt_02)). by rewrite ex (osum0r (OS_prod2 OS2 (ooq _ ox))). have evens x: evena x -> odda (osucc x). move: OS1 olt_12 => qa qb [ha hb]; split; [by apply: alim | move => bad]. move: (osa _ ha) => ox; move: (ooq _ ox) => op. move: (sym_eq (osucc_pr ox)). rewrite {2} (evenp1 _ ox hb) => eq1. have dp: (odiv_pr0 (osucc x) \2o (oquo x \2o) \1c) by split. move: (proj2(oquoremP2 (OS_succ ox) olt_02 dp)); rewrite bad. exact: C1_ne_C0. have odds x: odda x -> evena (osucc x). move =>[ax nex]; split; first by apply: alim. move: (osa _ ax) => ox. move:(oquoremP ox olt_02)=> [orq orr qv]. rewrite - {2}osucc_one; move/oltSleP. case: (equal_or_not(orem x \2o) \1o); last first. move => q1 q2; move: (conj q2 q1);rewrite - osucc_zero; move/oltSleP. by move/ole0=> bad; case: nex. move => eq1 _. have qa := (OS_succ orq). have dp: (odiv_pr0 (osucc x) \2o (osucc (oquo x \2o)) \0c). split;[ exact: qa | exact: OS0 | | exact: olt_02]. rewrite (osum0r (OS_prod2 OS2 qa)) (oprod2_succ OS2 orq) - {3} osum_11_2. by rewrite (osumA (OS_prod2 OS2 orq) OS1 OS1) -{1} eq1 - qv osucc_pr. by move: (proj2(oquoremP2 (OS_succ ox) olt_02 dp)). have bde x: inc x alpha -> exists2 y, evena y & x <=o y. move => xa;move:(osa _ xa) => ox; case: (p_or_not_p (even x)) => ex. exists x; split => //. move: (odds x (conj xa ex))=> ey. by exists (osucc x) => //; apply: oleS. have bdo x: inc x alpha -> exists2 y, odda y & x <=o y. move => xa;move:(osa _ xa) => ox; case: (p_or_not_p (even x)) => ex. exists (osucc x); [ exact:(evens _ (conj xa ex)) | by apply: oleS]. by exists x; split. set F1 := Zo F (fun z => even (Vf (inverse_fun f) z)). set F2 := Zo F (fun z => ~even (Vf (inverse_fun f) z)). exists F1, F2; split. - split; [ apply: Zo_S | move => x xf]; set y := Vf (inverse_fun f) x. have xtf: inc x (target f) by ue. have ya: inc y alpha by rewrite - sf; apply:(inverse_Vis bf). move:(bde _ ya) => [z [za zb]] le1. have le2: gle (ordinal_o alpha) y z. by apply/ordo_leP; split => //; case: le1. rewrite - sf in ya za. move/(fiso _ _ ya za): le2 => /iorder_gle1. rewrite /y (inverse_V bf xtf) => eq1; exists (Vf f z) => //. apply/Zo_P; rewrite (inverse_V2 bf za); split => //; Wtac. - split; [ apply: Zo_S | move => x xf]; set y := Vf (inverse_fun f) x. have xtf: inc x (target f) by ue. have ya: inc y alpha by rewrite - sf; apply:(inverse_Vis bf). move:(bdo _ ya) => [z [za zb]] le1. have le2: gle (ordinal_o alpha) y z. by apply/ordo_leP; split => //; case: le1. rewrite - sf in ya za. move/(fiso _ _ ya za): le2 => /iorder_gle1. rewrite /y (inverse_V bf xtf) => eq1; exists (Vf f z) => //. apply/Zo_P;rewrite (inverse_V2 bf za); split => //; Wtac. - by apply: disjoint_pr => t /Zo_P [_ ha] /Zo_P [_]; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)