proposition: Lemma Zermelo_ter E (r := worder_of E): worder_on r E /\ Zermelo_like r.
proof: Proof. rewrite /r /worder_of; clear r. pose p a:= a -s1 (rep a). have sp: forall a, sub (p a) a by move=> t; apply:sub_setC. set chain := (Zermelo_chain E). set om := intersection (Zo (\Po (\Po E)) chain). set res := graph_on _ _. have cp: chain (\Po E). split; fprops; first by apply /setP_P. move=> A /setP_P AE;apply/setP_P /(sub_trans (sp A) AE). move=> A AP [x xA]; move: (AP _ xA) => /setP_P xE; apply/setP_P. move=> t ti; exact: (xE _ (setI_hi ti xA)). have co :chain om. have aux: nonempty (Zo (\Po (\Po E)) chain). by exists (\Po E); apply: Zo_i; aw; trivial;apply: setP_Ti. split. + by apply:setI_s1; apply: Zo_i=> //; apply: setP_Ti. + by apply: (setI_i aux) =>y /Zo_hi [_]. + move=> A Ai; apply:(setI_i aux) => y yi. move/Zo_hi: (yi) => / proj43;apply;apply: (setI_hi Ai yi). + move=> A sAi neA; apply: (setI_i aux) => y yi. by move/Zo_hi: (yi) => /proj44; apply => // t /sAi /setI_hi; apply. move: (co)=> [sop Eo po io]. have cio: forall x, chain x -> sub om x. by move=> x [ha hb hc hd]; apply: setI_s1; apply: Zo_i =>//;apply /setP_P. pose m a:= forall x, inc x om -> sub x a \/ sub a x. have am: om = Zo om m. apply: extensionality; last by apply: Zo_S. apply: (cio); split => //. + by apply: sub_trans sop; apply: Zo_S. + by apply: Zo_i=>//; move=> x xom; left;move: (sop _ xom); move/setP_P. + move=> A /Zo_P [Aom mA]; apply: Zo_i; first by apply: (po _ Aom). suff aux: sub om (Zo om (fun x=> sub x (p A) \/ sub A x)). move=> x xom; case: (mA _ xom) => hyp. move: (aux _ xom) => /Zo_hi; case =>xpB; first by left. rewrite (extensionality xpB hyp); right; apply: sp. right; apply: (sub_trans (sp A) hyp). apply: cio; split. - by apply: (@sub_trans om); first by apply: Zo_S. - by apply: Zo_i=>//; right; move: (sop _ Aom);move/setP_P. - move => B /Zo_P [Bom ors]; apply: Zo_i; first by apply: (po _ Bom). case: ors => orsi; first by left; apply: sub_trans orsi; apply: sp. case: (mA _ (po _ Bom)) => aux; last by right. case: (inc_or_not (rep B) A)=> aux2. rewrite (extensionality orsi _); first by left. move=> t tB; case: (equal_or_not t (rep B)); first by move=> ->. by move=> trB; apply: aux; apply/setC1_P; split. right; move=> t tA;apply/setC1_P;split; [ by apply: orsi| dneg trB; ue]. - move=> B sB neB; apply: Zo_i. apply: io =>//; apply: (sub_trans sB) ; apply: Zo_S. case: (p_or_not_p (exists x, inc x B /\ sub x (p A))) => H. move: H=> [x [xB xp]]; left; move=> t ti; apply:(xp _ (setI_hi ti xB)). right; move=> t tA; apply: setI_i=>//. move=> y yB; move: (sB _ yB) => /Zo_P [yom ]; case; last by apply. by move => sy; case: H; exists y. + move=> A sAZ neA; apply: Zo_i. apply: io =>//; apply: (sub_trans sAZ); apply: Zo_S. move=> x xom. case: (p_or_not_p (exists2 y, inc y A & sub y x)) => H. move: H=> [y yA yx]; right; move => t ti;apply: (yx _ (setI_hi ti yA)). left; move=> t tx; apply: setI_i=>//. move=> y yA; move: (sAZ _ yA)=> /Zo_P [yom my]. case: (my _ xom);[ by apply| move=> yx; case: H;ex_tac; apply: Zo_S]. have st: forall a b, inc a om -> inc b om -> sub a b \/ sub b a. move=> a b; rewrite {2} am; move => aom /Zo_P [bom ba]; apply: (ba _ aom). pose d p := intersection (Zo om (sub p)). have dpo: forall X, sub X E -> inc (d X) om. by move=> X XE; rewrite /d; apply: io;[ apply:Zo_S | exists E;apply: Zo_i]. have pdp: forall X, sub X E -> sub X (d X). rewrite /d=> X XE t tX; apply: setI_i; first by exists E; apply: Zo_i. by move => y /Zo_hi; apply. have dpq: forall X Y, inc Y om -> sub X Y -> sub X E -> sub (d X) Y. by rewrite /d=> X Y Yom XY XE; apply: setI_s1; apply: Zo_i. have rdq: forall X, sub X E -> nonempty X -> inc (rep (d X)) X. move=> X XE neX; case: (inc_or_not (rep (d X)) X)=>// ni. have ned: nonempty (d X) by exists (rep X); apply: pdp => //; apply: rep_i. move: (conj (pdp _ XE) ni) => /subsetC1_P aux. case:(setC1_1 ((dpq _ _ (po _ (dpo _ XE)) aux XE) _ (rep_i ned))). have qdp: forall X Y, inc Y om -> sub X Y -> inc (rep Y) X -> Y = d X. move => X Y Yom sXY YX. have sXE: sub X E by apply: (sub_trans sXY); apply /setP_P; apply: sop. apply: extensionality (dpq _ _ Yom sXY sXE). case: (st _ _ (dpo _ sXE) (po _ Yom)) => ch. by case /setC1_P: (ch _ ( (pdp _ sXE) _ YX)) => _. rewrite - (setC1_K (sXY _ YX)); apply:(setU1_sub ch ((pdp _ sXE) _ YX)). pose R x := d (singleton x). have Rp: forall x, inc x E -> [/\ inc (R x) om, inc x (R x) & rep (R x) = x]. move => x xE. have p1: sub (singleton x) E by apply: set1_sub. split; [ by apply: dpo | exact:(pdp _ p1 _ (set1_1 x)) | ]. exact:(set1_eq (rdq _ p1 (set1_ne x))). have Ri:forall x y, inc x E -> inc y E -> R x = R y -> x = y. move=> x y xE yE; move: (Rp _ xE)(Rp _ yE). by move=> [_ _ p1][_ _ p2] p3; rewrite -p3 in p2; rewrite -p1 -p2. have Rrq: forall X, inc X om -> nonempty X -> R (rep X) = X. move=> X Xom neX; symmetry; apply: qdp =>//; last by fprops. by move=> t /set1_P ->; apply: rep_i. have sRR: forall x y, inc x E -> inc y E -> inc x (R y) -> (sub (R x) (R y)). move=> x y xE yE xRy. move: (Rp _ xE)(Rp _ yE) => [Rom xRx rR] [Rom' yRy rR']. case: (st _ _ Rom Rom') =>// hyp. move: (sub_set2 xRy yRy) => p1; move: (sub_trans p1 hyp) => p2. have p3: (inc (rep (R x)) (doubleton x y)) by rewrite rR; fprops. have p4: (inc (rep (R y)) (doubleton x y)) by rewrite rR'; fprops. by rewrite (qdp _ _ Rom p2 p3) (qdp _ _ Rom' p1 p4). have [or sr]:order_on res E. split; last by apply: graph_on_sr => a _. apply: order_from_rel1. + by move=> x y z /= xy yz; apply: sub_trans yz xy. + by move=> u v uE vE vu uv; apply: Ri=>//; apply: extensionality. + by move => u ue. have wor:worder res. apply:(worder_prop_rev or)=> x; rewrite sr => xsr nex. move:(rdq x xsr nex) => rdx. ex_tac=> a ax; apply/graph_on_P1; split => //; try apply: xsr => //. move: ((pdp _ xsr) _ ax)=> adx; apply: sRR; fprops. have ne: (nonempty (d x)) by exists a. by rewrite (Rrq _ (dpo _ xsr) ne). split=>//;split=>//; rewrite sr -/res => x xE. suff: (segment_r res x) = R x by move => ->; exact:(proj33 (Rp _ xE)). set_extens t. move /segment_rP /(graph_on_P0 (fun x y=> sub (R y) (R x)) E x t). move => [_ tE ]; apply; exact (proj32 (Rp _ tE)). move => tR; move: ((setP_hi (sop _ (proj31 (Rp _ xE)))) _ tR) => tE. by apply/segment_rP; apply/graph_on_P1; split => //; apply: sRR. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)