proposition: Lemma Exercise2_4 r (pworder := fun F => forall X, sub X F -> total_order (induced_order r X) -> worder (induced_order r X)): order r -> exists2 F, pworder F & cofinal r F.
proof: Proof. move=> or. set (FF:= Zo (\Po (substrate r)) pworder). pose f x y := forall a b, inc a x -> inc b (y -s x) -> ~ gle r b a. set (r' := graph_on (fun x y => sub x y /\ f x y) FF). have r'P: forall x y, gle r' x y <-> [/\ inc x FF, inc y FF, sub x y & f x y]. move=> x y; split; first by move /Zo_P => [] /setXp_P[xf yf][];aw. move => [pa pb pc pd]; apply /Zo_P;split => //; aw; last by split. by apply /setXp_P. have HpP: forall F, sub F (substrate r) -> (pworder F <-> (forall X, sub X F -> nonempty X -> total_order (induced_order r X) -> has_least (induced_order r X))). move => G Fsr;split. move=> pwog X XG neX toX; move: (pwog _ XG toX)=> [_]. move: (sub_trans XG Fsr) => Xsr. rewrite iorder_sr // => wor. move: (wor _ (@sub_refl X) neX); rewrite iorder_trans //. move=> h X XG torX; move: (torX) =>[orX _]. move: (sub_trans XG Fsr) => Xsr. split; fprops; rewrite iorder_sr //; move=> x xX neX. have aux := (iorder_trans r xX). rewrite aux; apply: h => //; first by apply: sub_trans XG. rewrite - aux; apply: total_order_sub => //; rewrite iorder_sr//. have Hf: forall x F, inc x (substrate r) -> inc F FF -> inc (F +s1 x) FF. move=> x F xsr =>/Zo_P [] /setP_P Fsr pwf. have stF: (sub (F +s1 x) (substrate r)). move=> t /setU1_P; case; [apply: Fsr | by move => ->]. apply: Zo_i; first by apply /setP_P. apply/(HpP _ stF) => X Xt neX toX. move: pwf => /(HpP _ Fsr) pwf. case: (inc_or_not x X) => tX; last first. apply: pwf =>// w wX; move: (Xt _ wX); case /setU1_P => // wx; case: tX; ue. move: (sub_trans Xt stF) => Xsr. case: (equal_or_not X (singleton x)) => eq. exists x; split;rewrite iorder_sr //; move=> t;rewrite eq => /set1_P ->. by apply /iorder_gle0P;fprops;order_tac; apply: Xsr. move:(@subsetI2r X F)(@subsetI2l X F); set (Y := X \cap F) => sYF sYX. move: (sub_trans sYF Fsr) => Ysr. case: (emptyset_dichot Y) => Ye. case: eq; set_extens t; last by move /set1_P ->. move => tx; move: (Xt _ tx);case /setU1_P; last by move => ->; fprops. by move => tf; empty_tac1 t; apply /setI2_P. have tos: (total_order (induced_order r Y)). have ->: (induced_order r Y) = (induced_order (induced_order r X) Y). by rewrite iorder_trans. by apply: total_order_sub => //; rewrite iorder_sr. move: (pwf _ sYF Ye tos) => [y []]; rewrite iorder_sr // => yY yl. move: (total_order_lattice toX) => lX. move: (sYX _ yY) => yX. have xsX: inc x (substrate (induced_order r X)) by rewrite iorder_sr. have ysX: inc y (substrate (induced_order r X)) by rewrite iorder_sr. move: (lattice_inf_pr lX xsX ysX). set z := (inf (induced_order r X) x y). move=> [p1 p2 p3]; exists z;red; rewrite iorder_sr//. move: (iorder_gle3 p1)(iorder_gle1 p1) (iorder_gle1 p2) => [zX _] zx zy. split => // w wx; apply /iorder_gle0P => //. move: (Xt _ wx); case /setU1_P => ezx; last by ue. have wY: inc w Y by apply: setI2_i. by move:(yl _ wY) => wy; move: (iorder_gle1 wy) => p4; order_tac. have or' :(order r'). apply: order_from_rel;split => //. move=> y x z [xy fxy] [yz fyz]; split => //;first by apply: sub_trans yz. move=> a b ax /setC_P [bz nbx]. case: (inc_or_not b y) => iby; first by apply: fxy =>//; apply /setC_P. apply: fyz =>//; [by apply: xy | apply /setC_P; split => // ]. by move=> x y [xy _] [yx _ ]; apply: extensionality. by move=> x y _; split => //; split => // a b ax /setC_P; case. have sr': substrate r' = FF. by apply: graph_on_sr=> x xp; split => //; move=> a b ax => /setC_P []. have isr': inductive r'. move=> X Xsr []; rewrite iorder_sr// => orX' tor'. have tor'': forall x y, inc x X -> inc y X -> ((sub x y /\ f x y) \/ (sub y x /\ f y x)). move=> x y xX yX. case: (tor' _ _ xX yX) =>h; move: (iorder_gle1 h) => /r'P. move=> [_ _ xy fxy]; left; split => //. move=> [_ _ xy fxy]; right; split => //. have su: sub (union X) (substrate r). move=> t /setU_P [y ty yX]; move: (Xsr _ yX); rewrite sr' => /Zo_P []. by move=> /setP_P ysr _; apply: ysr. have uxf: (inc (union X) FF). apply: Zo_i => //; first by apply /setP_P. move => t tu tort; move: (sub_trans tu su) => tsr. move: (iorder_osr or tsr) => [or1 sr1]. split => //; rewrite sr1 => x xt [u ux]; rewrite iorder_trans //. move: (tu _ (xt _ ux)) => /setU_P [i ui iX]. set (K:=x \cap i). move: (Xsr _ iX); rewrite sr' => /Zo_P [isr pwoi]. have K1: (sub K i) by apply: subsetI2r. move: (sub_trans xt tsr) => xsr. have K2: (sub K t) by apply: sub_trans xt; apply: subsetI2l. move: (sub_trans K2 tsr) => K3. have to3:(total_order (induced_order r K)). have ->: (induced_order r K) = (induced_order (induced_order r t) K). by rewrite iorder_trans. apply: total_order_sub => //; rewrite iorder_sr//. have neK: nonempty K by exists u; apply /setI2_P. move:isr pwoi => /setP_P isr / (HpP _ isr) pwoi. move: (pwoi _ K1 neK to3). move=> [y []]; rewrite iorder_sr// => yK ylK. have yx: inc y x by apply: (setI2_1 yK). exists y; split; rewrite iorder_sr//. move=> v vx; move: (tu _ (xt _ vx)) => /setU_P [w vw wX]. apply /iorder_gle0P => //. case: (inc_or_not v i) => vi. have wK: (inc v K) by apply: setI2_i. move: (ylK _ wK) => ge1; apply: (iorder_gle1 ge1). case: (tor'' _ _ wX iX); first by move=> [wi _]; case: vi; apply: wi. move=> [i3 fiw]. have vc: inc v (w -s i) by fprops. move: (fiw _ _ (K1 _ yK) vc) => r1. move: (xt _ yx) (xt _ vx) => yt vt. move: tort => [_ ]; rewrite iorder_sr// => tor1. case: (tor1 _ _ yt vt) => h; move: (iorder_gle1 h) => //. exists (union X); split; first by ue. move=> y yX; apply /r'P; split => //. by rewrite - sr'; apply: Xsr. by apply: setU_s1. move=> a b ay => /setC_P [bu iby]; move: bu => /setU_P [z bz zX]. case: (tor'' _ _ zX yX); first by move=> [yz _]; case: iby; apply: yz. move=> [yz fyz]; apply: fyz => //; apply /setC_P;split => //. move: (Zorn_lemma or' isr') => [a []]; rewrite sr' => aFF h. move: (aFF) => /Zo_P [] /setP_P asr pwoan; exists a => //. split => // x xsr. case: (inc_or_not x a)=> xa; first by ex_tac;order_tac. ex_middle aux;case: xa. suff rat: (gle r' a (a +s1 x)) by rewrite -(h _ rat); fprops. have pa: sub a (a +s1 x) by fprops. apply /r'P; split => //; first by apply: Hf => //. move => t s ta /setC_P [] /setU1_P; case => //. by move => -> _ ha; case: aux; exists t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)