proposition: Lemma Exercise1_23k r: order r -> anti_directed (nregs_order r).
proof: Proof. move=> or. move:(sub_osr (nreg_opens r)) =>[pa pb]. set (r':= nregs_order r). move: (opp_osr pa) => [or' prb]. have sr': (substrate r' = nreg_opens r) by rewrite /r' prb. set (aux:=(fun x y => forall z, gle r' x z -> gle r' y z -> False)). have p1: (forall x y, inc x (substrate r') -> inc y (substrate r') -> (disjoint x y) -> aux x y). by move=> x y xsr' ysr' dxy; rewrite /aux /r' Exercise1_23j // pr2. have Hv:substrate r' = nreg_opens r. rewrite /r' /nregs_order; aww; ue. set (i := fun x y => open_bar r (Zo x (fun u => forall t, gle r u t -> ~ (inc t y)))). have p2: (forall x y, inc x (substrate r') -> inc y (substrate r') -> [/\ open_r r (i x y), sub (i x y) x, disjoint (i x y) y & (i x y = emptyset -> sub x y)]). move=> x y xsr' ysr'. set (z:= Zo x (fun u => forall t, gle r u t -> ~ (inc t y))). have zx: sub z x by apply: Zo_S. move: xsr' ysr';rewrite Hv=> /Exercise1_23aP [ox nex]/Exercise1_23aP [oy ney]. move: (ox)(oy) => [[xsr xop] _] [oy1 _]. have zsr: (sub z (substrate r)) by apply: (@sub_trans x). have oz: (open_o r z). split => // u v /Zo_P [ux xp] uv; apply /Zo_P;split. apply: (xop _ _ ux uv). move => t vt; apply: (xp _ (order_transitivity or uv vt)). move: (Exercise1_22i or oz) => oi; rewrite /i -/z; split => //. rewrite(Exercise1_22p or ox); apply: Exercise1_22j => //. rewrite/disjoint (Exercise1_22p or oy); apply: Exercise1_22k => //. apply /set0_P => u /setI2_P [] /Zo_P [ux p] uy. by case: (p u) => //; order_tac; apply: xsr. move=> bze t tx. rewrite(Exercise1_22p or oy); apply: (Exercise1_22h or oy1 (xsr _ tx)). move=> u ut; move: (xop _ _ tx ut)=> ux. ex_middle ep; empty_tac1 u; apply: Exercise1_22e => //. apply: Zo_i => // v uv. by case: (inc_or_not v y)=> // vy; case: ep; exists v. have p3: (forall x y, inc x (substrate r') -> inc y (substrate r') -> (inc (i x y) (substrate r') \/ sub x y)). move=> x y xsr' ysr';move: (p2 _ _ xsr' ysr') => [oi si di ai]. rewrite Hv; case: (emptyset_dichot (i x y)) => ei; first by right; apply: ai. by left; apply /Exercise1_23aP. apply /(Exercise1_23hP or'); split. move=> x y xy. have xsr': (inc x (substrate r')) by order_tac. have ysr': (inc y (substrate r')) by order_tac. move: xy=> [] /(Exercise1_23bP or) [nex ney ox oy yx] xy. case: (p3 _ _ xsr' ysr') => p3c; last by case: xy; apply: extensionality. move: (p2 _ _ xsr' ysr')=> [oi si di ai]. exists (i x y); first split. + apply /Exercise1_23bP => //; split => //. by move: p3c;rewrite Hv => /Exercise1_23aP []. + move=> xi; red in di;move: ney => [t ty]; empty_tac1 t. apply: setI2_i=> //; ue. + move: (disjoint_S di) => di'; apply: (p1 _ _ ysr' p3c di'). move=> x y xsr' ysr'. move: (xsr')(ysr') ; rewrite Hv => /Exercise1_23aP [ox nex] /Exercise1_23aP[oy ney]. case: (p3 _ _ xsr' ysr') => p3c; last by constructor 2; apply /Exercise1_23bP. move: (p3c); rewrite Hv => /Exercise1_23aP [oi nei]. move: (p2 _ _ xsr' ysr')=> [oi2 si di ai]. constructor 3; exists (i x y); last by apply: p1. by apply /Exercise1_23bP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)