proposition: Lemma Exercise1_23l r y: order r -> let r' := nregs_order r in inc y (nreg_opens r') -> exists ! x, (inc x (nreg_opens r) /\ y = canonical_reg_open r' x).
proof: Proof. move=> or r' ys. set (E:=nreg_opens r). set (E':=nreg_opens r'). move:(sub_osr (nreg_opens r)) =>[pa pb]. move: (opp_osr pa) => [or' prb]. have sr': (substrate r' = nreg_opens r) by rewrite /r' prb. have se: (E = substrate r') by ue. apply /unique_existence;split; last first. move => u v [uE up][vE vp]; apply: (Exercise1_23k or). by rewrite - se. by rewrite - se. ue. have p1: (forall x t, inc x E -> inc t E -> (inc t (canonical_reg_open r' x) <-> (forall u, gle r' t u -> nonempty (u \cap x)))). move=> x t xE tE; move: (xE) (tE); rewrite se => xs ts. apply:(iff_trans (Exercise1_23e or' xs ts)); split. move=> h u tu; move: (h _ tu) => [v]. move /(Exercise1_23bP or)=> [_ [w wv] _ _ vu] /(Exercise1_23bP or) [_ _ _ _ vx]. by exists w; apply: setI2_i; [apply: vu | apply: vx]. move=> h z zx; move: (h _ zx) => [w] /setI2_P [wz wx]. have zs: (inc z (substrate r')) by order_tac. rewrite - se in zs; move: (Exercise1_23i or wx xE) => le1. move: (Exercise1_23i or wz zs) => le2. by exists (canonical_reg_open r w). have p2: (forall x t, inc x E -> inc t E -> (inc t (canonical_reg_open r' x) <-> (forall a, inc a t -> (exists2 b, inc b x & gle r a b)))). move=> x t xE tE; rewrite p1 //; split. move => h a iat; move: (h _ (Exercise1_23i or iat tE)) => [u us]. move: xE =>/Exercise1_23aP [xo [w wx]]. move: us => /setI2_P;rewrite /canonical_reg_open (Exercise1_22p or xo). set z:= Zo _ _; case: (emptyset_dichot (z \cap x)) => ie. move: (xo) => [xo1 _] [h1 h2]. move:(Exercise1_22k or (Exercise1_23c a or) xo1 ie) => ie2. case: (in_set0 (x:= u)); rewrite -ie2; apply/setI2_P; split => //. move: ie => [v] /setI2_P [] /Zo_P [vsr le1] vx _. by exists v => //; apply: Exercise1_22e => //; case: xo. move=> h u => /(Exercise1_23bP or) [_ [b bu] ot ou ut]. move: (h _ (ut _ bu)) => [c cx bc]; exists c; apply: setI2_i =>//. move: ou => [[_ ou] _]; apply: (ou _ _ bu bc). have p3: (forall x t, nonempty x -> open_o r x -> inc t E -> (inc t (canonical_reg_open r' (open_bar r x)) <-> (forall a, inc a t -> (exists2 b, inc b x & gle r a b)))). move=> x t [z zx] o tE. have bE: (inc (open_bar r x) E). apply /Exercise1_23aP; split => //; first by apply: Exercise1_22i => //. exists z; apply: Exercise1_22e => //. rewrite (p2 _ _ bE tE); split. move=> h a ait; move: (h _ ait) => [c cb ac]. move: cb => /setU_P [d cd] /Zo_P [] /setP_P dsr [od]. move =>/(cofinal_inducedP or dsr) [xd h']. move: (h' _ cd) => [e ex ey]; ex_tac; order_tac. move=> h a ait; move: (h _ ait) => [b bx ab]. exists b => //; apply: Exercise1_22e => //. have Hu:forall x, inc x y -> open_r r x. move=> x xy; move: ys => /Exercise1_23aP [[[q1 q2] q3] ney]. by move: (q1 _ xy); rewrite - se => /Exercise1_23aP []. have Hv: (sub (union y) (substrate r)). move=> t /setU_P [x tx xy]; move: (Hu _ xy)=> [[h _] _]; by apply: h. have Hw: (open_o r (union y)). by apply: Exercise1_22c=> //; move=> x xy; case: (Hu _ xy). set (T:=Zo E (fun z => forall a, inc a z -> exists2 b, inc b (union y) & gle r a b)). set (y':= canonical_reg_open r' (open_bar r (union y))). have neuy: (nonempty (union y)). move: ys => /Exercise1_23aP [[[q1 q2] q3] ney]. move: ney => [z zy]; move: (q1 _ zy); rewrite - se => /Exercise1_23aP. move => [_ [t tz]]; exists t; union_tac. have Hx :inc (open_bar r (union y)) E. apply /Exercise1_23aP; split; first by apply: Exercise1_22i =>//. by move: neuy => [t tu]; exists t; apply: Exercise1_22e. have Ty: (T = y'). suff: (forall t, inc t E -> (inc t T <-> inc t y')). have p4: sub y' E. have p5: (inc (open_bar r (union y)) (substrate r')) by rewrite - se. move: (Exercise1_23d2 or' p5) => /Zo_P [ ] /Zo_P [] /setP_P. by rewrite se -/y'. move=> tp; set_extens t => ts. by rewrite -tp //; move: ts => /Zo_P []. by rewrite tp //; apply: p4. move=> t tE; rewrite /y'; rewrite (p3 _ _ neuy Hw tE). split; first by move => /Zo_P []. by move => h; apply: Zo_i. have syy': (sub y y'). move: ys =>/Exercise1_23aP [[[q1 _] _] _]. move=> t ty;rewrite -Ty; apply: Zo_i; first by rewrite se; apply: q1. move=> a ait; have au: (inc a (union y)) by union_tac. ex_tac; order_tac. by move: (q1 _ ty); rewrite - se =>/Exercise1_23aP [[[h _] _] _]; apply: h. have oy': open_o r' y'. rewrite /y'; rewrite se in Hx. move: (Exercise1_23d2 or' Hx) => /Exercise1_23aP. by move=> [[oo _] _]. have cf: substrate (induced_order r' y') = y'. rewrite iorder_sr // - se -Ty; apply: Zo_S. Abort. Definition branched r := order r /\ (forall x, inc x (substrate r) -> exists y z, [/\ gle r x y, gle r x z & (forall t, gle r y t -> gle r z t -> False)]). Lemma Exercise1_24a r: order r -> anti_directed r -> (forall x, inc x (substrate r) -> ~ maximal r x) -> branched r. Proof. move=> or ar nm; split => // x xsr. move: ar => /(Exercise1_23hP or) [ar1 ar2]. move: (nm _ xsr)=> xnm. have [y xy]: (exists y, glt r x y). ex_middle xy; case: xnm;split => //. by move=> z xz; symmetry;ex_middle exz; case: xy; exists z. move: (ar1 _ _ xy) => [z xz h]. by move: xy xz => [xy _][ xz _]; exists y; exists z. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)