proposition: Lemma Zermelo_aux E s p (r := union (Zo (\Po coarse E) (Zermelo_ax E p s))): sub s (\Po E) -> (forall x, inc x s -> inc (p x) (E -s x)) -> Zermelo_ax E p s r /\ (~ (inc (substrate r) s)).
proof: Proof. move=> sp pp. rewrite /r;set (m:= Zo _ _); clear r. pose co r r' := Zo ((substrate r) \cap (substrate r')) (fun x => segment r x = segment r' x /\ (seg_order r x) = (seg_order r' x)). have aux0 r r': co r r' = co r' r. rewrite /co setI2_C. set_extens t; move/Zo_P => [pa [pb pc]]; apply: Zo_i => //. have aux1 r r': worder r -> worder r' -> segmentp r (co r r'). rewrite /co => wor wor'. split; first by move=> t /Zo_S /setI2_P []. move=> x y. case: (equal_or_not y x); first by move=> ->. move => nyx /Zo_P [pa [pb pc]] pd. have ltyx:glt r y x by split. have sry: inc y (segment r x) by apply /segmentP. have sry': inc y (segment r' x) by rewrite - pb. have syr: inc y (substrate r) by apply: (sub_segment sry). have syr': inc y (substrate r') by apply: (sub_segment sry'). rewrite /seg_order/induced_order - pb in pc. have or: order r by fprops. have or': order r' by fprops. have sryy': (segment r y = segment r' y). set_extens t; move/segmentP => [ty nty]; apply /segmentP; split=>//; suff: (inc (J t y) (r \cap (coarse (segment r x)))). - by rewrite pc; case/setI2_P. - apply/setI2_i => //; apply/setXp_i => //; apply/segmentP; order_tac. - by case /setI2_P. - have aux: glt r' y x by apply/segmentP; rewrite -pb; apply/segmentP. rewrite pc pb;apply:setI2_i => //; apply:setXp_i;apply/segmentP =>//. order_tac. apply: Zo_i; [ fprops | split=>// ]. rewrite /seg_order/induced_order - sryy'. move: (coarse_segment_monotone or pd)=> p1. set_extens z; move/setI2_P =>[zr zc]; suff: (inc z (r \cap (coarse (segment r x)))). - by rewrite pc; case/setI2_P => qa qb; apply: setI2_i => //; apply: p1. - by apply /setI2_i => //; apply: p1. - by move /setI2_P => [qa qb]; apply :setI2_i. - by rewrite pc;apply/setI2_i => //; apply: p1. have aux2 r r': worder r -> worder r' -> sub (induced_order r (co r r')) (induced_order r' (co r r')). move=> wor wor'. have or: order r' by fprops. move=> t /setI2_P [tr] /setX_P [pt Pt Qt]. apply/setI2_P; split; last by apply /setX_P. move: Qt => /Zo_P [] /setI2_P [Qtr Qtr'] [ss io]. case: (equal_or_not (P t) (Q t)) => eq. by rewrite -pt eq; order_tac. rewrite -pt in tr. have: inc (P t) (segment r (Q t)) by apply: segment_inc. rewrite ss -{3} pt => aux. exact: (proj1 (inc_segment aux)). pose qp r r' := [/\ sub (substrate r) (substrate r'), r = induced_order r' (substrate r) & segmentp r' (substrate r)]. have aux3 r r': Zermelo_ax E p s r -> Zermelo_ax E p s r' -> qp r r' \/ qp r' r. move=> [wor srE prx] [wor' srE' pry]. move: (aux1 _ _ wor' wor)(aux1 _ _ wor wor'). rewrite aux0; set (v:= co r r'). move=> svr' svr. have io: (induced_order r v = induced_order r' v). apply: extensionality; first by apply: aux2. by rewrite /v aux0; apply: aux2. move: (sub_segment1 svr)(sub_segment1 svr')=> vsr vsr'. case: (equal_or_not v (substrate r)) => evr. left; rewrite /qp -evr; split => //. rewrite -io evr;symmetry; apply: iorder_substrate; fprops. case: (equal_or_not v (substrate r')) => evr'. right; rewrite /qp -evr'; split => //. rewrite io evr';symmetry; apply: iorder_substrate; fprops. case: (emptyset_dichot ((substrate r) -s v)) => cr. by case: evr; apply: extensionality=>//; apply: empty_setC. case: (emptyset_dichot (complement (substrate r') v)) => co'. by case: evr'; apply: extensionality=>//; apply: empty_setC. have sc: (sub ((substrate r) -s v) (substrate r)). by apply: sub_setC. have sc': (sub ((substrate r') -s v) (substrate r')). by apply: sub_setC. move:(worder_total wor) (worder_total wor')=> tor tor'. move:wor=> [or wo]; move: (wo _ sc cr)=> [x []]. rewrite iorder_sr // => /setC_P [xs xc] px. move:wor'=> [or' wo']; move: (wo' _ sc' co')=> [y []]. rewrite iorder_sr // => /setC_P [ys yc] py. have p1: (segment r x = v). set_extens z => zs. ex_middle aux. move: (inc_segment zs) => zx. have zc: inc z ((substrate r) -s v) by apply/setC_P; split=>//; order_tac. move: (iorder_gle1 (px _ zc)) => h; order_tac. apply /segmentP. case: (total_order_pr2 tor (vsr _ zs) xs)=>// xz. case: xc; exact: ((proj2 svr) _ _ zs xz). have p2: (segment r' y = v). set_extens z => zs. ex_middle aux. move: (inc_segment zs) => zx. have zc: inc z ((substrate r') -s v) by apply/setC_P;split=>//;order_tac. move: (iorder_gle1 (py _ zc)) => h; order_tac. apply /segmentP. case: (total_order_pr2 tor' (vsr' _ zs) ys)=>// yz. case: yc; exact: ((proj2 svr') _ _ zs yz). have xy: x = y by rewrite - (proj2(prx _ xs)) -(proj2(pry _ ys)) p1 p2. case: xc. apply: Zo_i; first by apply :setI2_i => //; ue. by rewrite /seg_order p1 xy p2. have ha x: inc x m -> worder x by move => /Zo_hi []. have hb a b: inc a m -> inc b m -> segmentp a (substrate b) \/ segmentp b (substrate a). move => /Zo_hi za /Zo_hi zb. by case: (aux3 _ _ za zb); move => [_ _]; [right | left ]. have hc a b: inc a m -> inc b m -> sub (substrate a) (substrate b) -> order_extends a b. move => am bm sab; move:(am)(bm) =>/Zo_hi za /Zo_hi zb. case: (aux3 _ _ za zb);move=> [sba bi siab]; first exact. have ssab: (substrate a = substrate b) by apply: extensionality. move:(iorder_substrate (proj1 (ha _ am))) => H. by move: bi; rewrite/order_extends - ssab H; move ->. have hcw a b: inc a m -> inc b m -> sub (substrate a) (substrate b) -> sub a b. by move => am bm h; rewrite (hc _ _ am bm h) => t /setI2_P []. have sxm x: inc x m -> sub x (coarse E) by move /Zo_S/setP_P. have eVVg a b: inc a m -> inc b m -> exists c, [/\ inc c m, sub (substrate a) (substrate c) & sub (substrate b) (substrate c)]. move => am bm. by case: (hb _ _ am bm) => - [sa _]; [ exists a | exists b]; split. set G := union m. have gu: sgraph G. move=> t /setU_hi [y ty /sxm yc]; exact:(setX_pair (yc _ ty)). pose D := Zo E (fun z => exists2 x, inc x m & inc z (substrate x)). have ur y: inc y D -> related G y y. move =>/Zo_hi[x xm ysx]; apply/setU_P; ex_tac. by move:(proj42 (proj1 (ha _ xm)) y ysx). have su: substrate G = D. set_extens x; last by move/ur => rr; substr_tac. case /(substrate_P gu) => [] [y Ju]; move: (setU_hi Ju)=> [z zdg zp]. move:((sxm _ zp) _ zdg) => /setXp_P [xE _]. apply: (Zo_i xE); exists z => //; substr_tac. move:((sxm _ zp) _ zdg) => /setXp_P [_ yE ]. apply: (Zo_i yE); exists z => //; substr_tac. have sGP x: inc x (substrate G) <-> exists2 t, inc t m & inc x (substrate t). split; first by rewrite su; move/Zo_hi. move => [t tm xsr]. move:(proj42 (proj1 (ha _ tm)) x xsr) => txx. have hh: inc (J x x) G by apply/setU_P; exists t. substr_tac. have cov x y: inc x G -> inc y G -> exists u, [/\ inc u m, inc x u & inc y u]. move=> /setU_P [a adg ap] /setU_P [b bdg bp]. case: (hb _ _ ap bp) =>- [asub _]. by move:(hcw _ _ bp ap asub) => sba; exists a; split => //; apply: sba. by move:(hcw _ _ ap bp asub) => sba; exists b; split => //; apply: sba. have oG: order G. split. + exact. + by hnf; rewrite su. + move => x y z p1 p2; move: (cov _ _ p1 p2)=> [c [cm p1c p2c]]. move: (ha _ cm) => [/proj43 or _]; exact:(setU_i (or _ _ _ p1c p2c) cm). + move => x y p1 p2; move: (cov _ _ p1 p2)=> [c [cdg p1c p2c]]. move: (ha _ cdg)=> [or _]; order_tac. have Vag a: inc a m -> induced_order G (substrate a) = a. rewrite /induced_order. move => am;set_extens x => xs; last first. apply/setI2_P; split; first by rewrite /G; union_tac. by apply:(sub_graph_coarse_substrate (proj41 (proj1 (ha _ am)))). move/setI2_P:xs => [/setU_P [z xz zm] xaa]. move: (eVVg _ _ am zm) => [t [tm sa sz]]. have xt:= ((hcw z t zm tm sz) _ xz). by rewrite (hc _ _ am tm sa); apply/setI2_P. have p1 a: inc a m -> sub (substrate a) (substrate G). move => am t tsa; apply/sGP; ex_tac. have p0 a x y: inc x (substrate a) -> gle G y x -> inc y (substrate G) -> inc a m -> inc y (substrate a). move => xs/setU_P [u Jv udg] ys am. case: (hb _ _ am udg) => h; first by apply:(proj1 h); substr_tac. exact: (proj2 h _ _ xs Jv). have p2 a: inc a m -> segmentp G (substrate a). move=> am;split; first by apply: p1. move=> x y xs yx;exact: (p0 a _ _ xs yx (arg1_sr yx) am). have p3 a x: inc a m -> inc x (substrate a) -> segment a x = segment G x. move=> am xs; set_extens y => ys; move: (inc_segment ys) => [yx nyx]. apply /segmentP; split=>//; apply: setU_i yx am. apply/segmentP; split => //;rewrite - (Vag _ am);apply/iorder_gle0P => //. exact: (p0 a _ _ xs yx (arg1_sr yx) am). have p4 a x: inc a m -> segmentp a x -> segmentp G x. move=> am sa; case: (well_ordered_segment (ha _ am) sa). by move=> ->; apply: p2. by move=> [y ysV ->]; rewrite (p3 _ _ am ysV); apply: segment_segment. have woG: worder G. apply:(worder_prop_rev oG) => x xsr [y yx]. move /sGP: (xsr _ yx) => [a am ysa]. set (x1:= x \cap (substrate a)). have sx1s: (sub x1 (substrate a)) by apply: subsetI2r. have nx1: nonempty x1 by exists y; apply: setI2_i. move: (worder_prop (ha _ am) sx1s nx1)=> [z zs zle]. have zx: inc z x by apply: (setI2_1 zs). have zVa: inc z (substrate a) by apply: (setI2_2 zs). exists z => // t tx. move: (xsr _ tx) => /sGP [b bm bV]. have aux: inc t (substrate a) -> gle G z t. move=> hyp. by move:(zle _ (setI2_i tx hyp));rewrite - (Vag _ am) => /iorder_gle1. case: (hb _ _ am bm); move => [px py]; first by apply: (aux (px _ bV)). move: (px _ zVa)=> zVb. case: (total_order_pr2 (worder_total (ha _ bm)) bV zVb). move=> [tz ntz]; apply: (aux (py _ _ zVa tz)). by rewrite - (Vag _ bm) => /iorder_gle1. have ssGE: sub (substrate G) E by rewrite su; apply/Zo_S. have ssG x: inc x (substrate G) -> inc (segment G x) s /\ p (segment G x) = x. move => /sGP [y ym xsy]; move: (ym) => /Zo_hi [_ _ zp2]. by rewrite - (p3 y x ym xsy); apply: zp2. have Za: (Zermelo_ax E p s G) by []. split => // sGs. case/setC_P:(pp _ sGs); set (a:= p (substrate G)) => [aE nas]. move:(worder_adjoin_greatest woG nas). move: (order_with_greatest_pr (worder_or woG) nas). set Ga := order_with_greatest G a; move => [[oGa sGa] Gai [aGA ala]] woGa. have seGa: segment Ga a = (substrate G). set_extens x => xs. move:(inc_segment xs)=> [xa xna]. have: inc x (substrate Ga) by order_tac. by rewrite sGa => /setU1_P;case. have nax: x <> a by dneg axx; rewrite -axx. apply /segmentP; split=>//; apply: ala; rewrite sGa; fprops. have asa x: inc x (substrate Ga) -> x = a \/ segment Ga x = segment G x. rewrite sGa => /setU1_P; case; last by left. move=> xsr; right. have xsre: inc x (substrate Ga) by rewrite sGa; aw; fprops. set_extens y; move /segmentP=> [yx nyx]; apply/segmentP; split => //. rewrite Gai; apply/iorder_gleP => //. move: (arg1_sr yx); rewrite sGa => /setU1_P; case => // eya. move: (ala _ xsre); rewrite -/Ga - eya => xy; case: nyx; order_tac. by move: yx; rewrite Gai; apply: iorder_gle1. have Zae: (Zermelo_ax E p s (order_with_greatest G a)). move: Za=> [q1 q2 q3]. have H t: inc t (substrate G) -> segment (order_with_greatest G a) t = segment G t. move => ts; move: (setU1_r (p (substrate G)) ts); rewrite - sGa => /asa. by case => // hyp; case: nas; rewrite - hyp. split=>//; rewrite sGa => t /setU1_P; case. - apply: q2. - by move=> ->. - by move=> ts; rewrite (H _ ts); apply: q3. - by move => ->; rewrite seGa. have um:inc (order_with_greatest G a) m. apply: Zo_i =>//;apply /setP_P. apply: sub_trans (setX_Sll (proj32 Zae)). apply: sub_graph_coarse_substrate; fprops. case: nas; apply/sGP; ex_tac; rewrite sv; apply: setU1_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)