proposition: Lemma Exercise2_6h a: inc a (source f) -> worder (induced_order r (chainx a)).
proof: Proof. move=> asf. set (E:= substrate r). set(M0 := Zo (\Po E) (fun z => inc a z /\ exists b, least_upper_bound r z b)). have aE: inc a E by rewrite /E sf. have p0: forall x, inc x M0 -> sub x (substrate r). by move=> x => /Zo_P [] /setP_P. have p1: (forall z, inc z M0 -> least_upper_bound r z (supremum r z)). move=> z /Zo_P [zp [az [b leb]]]. by apply: supremum_pr1 => //; exists b. have p2: forall x, inc x M0 -> (inc (supremum r x) (substrate r) /\ inc (Vf f (supremum r x)) (substrate r)). move => x xM0; move: (p0 _ xM0) => xE; move: (p1 _ xM0). move => /(lubP or xE) [[sE _] _]; split => //;move: (fxx sE) => aux;order_tac. pose sif x := glt r x (Vf f x). set (M1 := Zo M0 (fun z => ~ (inc (supremum r z) z))). set (M2 := Zo M0 (fun z => sif (supremum r z))). set(M:= (M1 \cup M2) +s1 emptyset). pose p x := Yo (x= emptyset) a (Yo (inc x M1) (supremum r x) (Vf f (supremum r x))). have Ha:sub (M1 \cup M2) M0 by apply: setU2_12S; apply: Zo_S. have p3: (forall x, inc x M -> (inc (p x) (E -s x))). move=> x xM; rewrite /p; apply/setC_P. Ytac xe; first by split => // xie; empty_tac1 a. Ytac xM1. by move: xM1 => /Zo_P [/p2 [xM0 _] ni]. move: xM; case /setU1_P;[ case /setU2_P => // H | done]. move /Zo_P:H => [xM0 lt1]; move: (p2 _ xM0) => [p3 p4]; split => //. move=> h; move: (p0 _ xM0) => xE;move: (p1 _ xM0); move /(lubP or xE). rewrite /sif in lt1; move=> [ [_ ub ] _]; move: (ub _ h) => p5; order_tac. have p4: sub M (\Po E). move=> t th; apply /setP_P. case /setU1_P: th => h; [ apply: (p0 _ (Ha _ h)) | rewrite h; fprops]. move: (Zermelo_aux p4 p3). rewrite /Zermelo_ax; set r' := union _; set (q:= substrate r'). move=> [[wor' qE xqp] nqM]. have aq: (inc a q). case: (emptyset_dichot q) => qe; first by case: nqM; rewrite /M qe; fprops. move: (worder_has_empty_seg wor' qe) => [x xsr' se]. by move: (proj2 (xqp _ xsr')); rewrite se /p Y_true // => ->. have compat: (forall u v, gle r' u v -> gle r u v). move=> u v uv. have vq: (inc v q) by rewrite /q; order_tac. have bE: inc v E by apply: qE. case: (equal_or_not u v) => auv; first by rewrite auv; order_tac. have suv:(inc u (segment r' v)) by apply: segment_inc. have nes: segment r' v <> emptyset by apply/nonemptyP; ex_tac. move: (proj1 (xqp _ vq)); case /setU1_P => // h. move: (p1 _ (Ha _ h)); set c := supremum r _. have ss: sub (segment r' v) (substrate r). apply: (@sub_trans q) => //; apply: sub_segment. move=> /(lubP or ss) [[_ p5] _]; move: (p5 _ suv) => le1. have csr: (inc c (substrate r)) by order_tac. move: (proj2(xqp _ vq)); rewrite /p ; Ytac0; Ytac c1; first by move => <-. move: h; case /setU2_P; first by move => H. move /Zo_P => [_ [le2 _]] eq1; rewrite eq1 in le2; order_tac. move: (wor') => [or' _]. have p5: forall y, least_upper_bound r q y -> (inc y q /\ Vf f y = y). move=> y ley. have qM0: inc q M0 by apply: Zo_i; [ apply /setP_P | split => //; exists y]. case: (inc_or_not y q) => yq. case: (equal_or_not y (Vf f y)) => w //. move: nqM => /setU1_P; case; left; apply /setU2_P; right. apply /Zo_i => //; red; rewrite - (supremum_pr2 or ley); split =>//. by apply: fxx; apply: qE. move: nqM => /setU1_P; case; left; apply /setU2_P; left. by apply /Zo_i => //; rewrite - (supremum_pr2 or ley). have stable: (forall x, inc x q -> inc (Vf f x) q). move=> x xq; set (m:=Zo q (fun z => glt r' x z)). case: (emptyset_dichot m) => em. have gx: (greatest r' x). split => // y ysr; case: (total_order_pr2 (worder_total wor') xq ysr)=>//. move=> bad; empty_tac1 y;apply: Zo_i => //; order_tac. have gx':(greatest (induced_order r q) x). split;rewrite iorder_sr//; move=> y yq; apply /iorder_gle0P => //; apply: compat. by move: gx => [_]; apply. move: (greatest_is_sup or qE gx') => sq. by move: (p5 _ sq) => [r1 r2]; rewrite r2. move: (Exercise2_6g wor' xq em) => [z zsr]. case: (xqp _ zsr); set s := segment r' z => p5' p6 ss. have xs: inc x s by rewrite - ss; apply: inc_bound_segmentc. have ssr': sub s (substrate r') by apply: sub_segment. have ssr: sub s (substrate r) by apply: (@sub_trans q). have aux y: inc y s -> gle r' y x by rewrite - ss => /segmentcP. have gx: (greatest (induced_order r' s) x). by split;rewrite iorder_sr// => y ysr; apply /(iorder_gle0P _ ysr xs); apply: aux. have gx':(greatest (induced_order r s) x). by split; rewrite iorder_sr // => y yq; apply /iorder_gle0P => //; apply: compat; apply: aux. move: (greatest_is_sup or ssr gx') => sq. move:(supremum_pr2 or sq) => xsq. move: p5' p6; rewrite /p; Ytac se; first by empty_tac1 x. case /setU1_P => //; Ytac nsm1. move: nsm1 => /Zo_hi;rewrite -xsq //. case /setU2_P; [ done | by rewrite -xsq;move=> _ -> ]. move: (worder_total wor') => [_ tor']. have toq: forall a b, inc a q -> inc b q -> gle r a b \/ glt r b a. move => u v uq vq. case:(equal_or_not u v) => uv; first by rewrite uv; left;order_tac; apply: qE. rewrite /glt; case: (tor' _ _ uq vq) => h; move: (compat _ _ h);fprops. have compat': forall u v, inc u q -> inc v q -> gle r u v -> gle r' u v. move=> u v uq vq uv. case: (tor' _ _ uq vq) => h; move: (compat _ _ h) => //. by move=> vu; move: h; rewrite (order_antisymmetry or uv vu). have aux: (forall N y, sub N q -> nonempty N -> least_upper_bound r N y -> inc y q). move => N y Nq neN infN. move: (sub_trans Nq qE) => NE. move: infN => /(lubP or NE) [[ys uny] luny]. set (bN:=Zo q (fun z=> gle r y z)). case: (emptyset_dichot bN) => bne. suff le1: (least_upper_bound r q y) by exact: (proj1 (p5 _ le1)). apply /(lubP or qE); split; last first. by move=> z [zr uz]; apply: luny; split => // t tn; apply: uz; apply: Nq. split =>// z zq; case: (p_or_not_p (exists t, inc t N /\ glt r z t)). move => [t [/uny tN [zt _]]]; order_tac. move =>bad; empty_tac1 z; apply: Zo_i => //. apply: luny; split; first by apply: qE. move=> t tN; case: (toq _ _ (Nq _ tN) zq) => // zt; case: bad; ex_tac. have bNq: (sub bN q) by apply: Zo_S. move: (proj2 wor' _ bNq bne) => [z []];rewrite iorder_sr// => zbN zlbn. move: (zbN) => /Zo_P [zq yz]. case: (inc_or_not z N) => zN. by move: (uny _ zN) => zy; rewrite (order_antisymmetry or yz zy). have zlb1: (forall u, inc u q -> gle r y u -> gle r' z u). move=> u uq r1; have ub: (inc u bN) by apply: Zo_i. exact: (iorder_gle1 (zlbn _ ub)). have Ns: (sub N (segment r' z)). move=> t tN ; apply /segmentP; split; last by dneg tz; ue. move: (uny _ tN) => ty; apply: compat' => //;[ by apply: Nq | order_tac]. have /nonemptyP Nes: (nonempty (segment r' z)). by move: neN => [w wN]; exists w; apply: Ns. case: (xqp _ zq); case /setU1_P; last by done. rewrite /p;Ytac0; move=> aux; move: (p1 _ (Ha _ aux)). have aux1: sub (segment r' z) (substrate r) by apply: (@sub_trans q) => //; apply: sub_segment. set s := (supremum r (segment r' z)); move /(lubP or aux1)=> [[p6 p7] p8]. have ys1: (gle r y s) by apply: luny; split => // t tn; apply: p7; apply: Ns. have sz: (gle r s z). by apply: p8; split;fprops; move => t /segmentP [le _]; apply: compat. have sns: ~ (inc s (segment r' z)) . move / segmentP => [r1 r2]. have sq: (inc s q) by rewrite / q; order_tac. move: (zlb1 _ sq ys1) => aux2; case: r2; order_tac. have p9: (inc (segment r' z) M1) by apply: Zo_i => //; apply: Ha. Ytac0; move=> sz1. suff:(gle r s y) by move=> sy; rewrite - (order_antisymmetry or sy ys1) sz1. apply: p8; split => // t /segmentP tz. have tq: (inc t q) by rewrite /q; order_tac. case: (p_or_not_p (exists2 u, inc u N & glt r t u)). move=> [u uN [tu _]]; move: (uny _ uN) => uy; order_tac. move=> bad. have good: (forall u, inc u N -> gle r u t). move=> u uN; case: (toq _ _ (Nq _ uN) tq) => // tu; case: bad; ex_tac. have ubt: (upper_bound r N t) by split =>//; apply: qE. move:(zlb1 _ tq (luny _ ubt)) => p10; order_tac. have sc: (sub (chainx a) q). move => t tc; apply: (setI_hi (y:=q) tc);apply: Zo_i => //. apply: Zo_i; [ by apply /setP_P | split => //]. move: (sub_trans sc qE) => sE. move: (iorder_osr or sE) => [or1 sr1]. split => //; rewrite sr1 => x xc nex; move: (sub_trans xc sc) => xcq. move: (sub_trans xcq qE) => xE. move: wor' => [_ wor''];move: (wor'' _ xcq nex) => [z []]; rewrite iorder_sr//. move=> zx zl; exists z; rewrite iorder_trans //;split => //;rewrite iorder_sr//. move=> b bx;apply /iorder_gle0P => //. apply:(compat _ _ (iorder_gle1 (zl _ bx))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)