proposition: Lemma Exercise1_23hP r: order r -> let aux := (fun x y => forall z, gle r x z -> gle r y z -> False) in (anti_directed r) <-> ((forall x y, glt r x y -> exists2 z, glt r x z & aux y z) /\ forall x y, inc x (substrate r) -> inc y (substrate r) -> [\/ gle r x y, gle r y x, (exists2 x', gle r x x' & aux x' y) | (exists2 y', gle r y y' & aux x y')]).
proof: Proof. move=> or aux. have p1: (forall x y, inc x (substrate r) -> inc y (substrate r) -> (inc y (canonical_reg_open r x) <-> forall z, gle r y z -> ~ (aux x z))). move=> x y xsr ysr; apply: (iff_trans (Exercise1_23e or xsr ysr)); split. move=> h z yz h1; move: (h _ yz)=> [t zt xt]; apply: (h1 _ xt zt). move=> h z yz; move: (h _ yz) => h1;ex_middle h2; case: h1. by move=> t xt zt; case: h2; exists t. have Hb:forall x y, gle r x y -> sub (canonical_reg_open r y) (canonical_reg_open r x). move=> x y xy; move: (Exercise1_23f or xy) => /(Exercise1_23bP or). by move => [_ _ _]. have Hc:forall x y, aux x y -> aux y x. move => x y h z s1 s2; apply: (h _ s2 s1). split; last first. move=> [C1 C2] x y xsr ysr cxy; ex_middle nxy. have xc: (inc x (canonical_reg_open r x)) by apply: Exercise1_23d1. have yc: (inc y (canonical_reg_open r y)) by apply: Exercise1_23d1. case: (C2 _ _ xsr ysr) => c2p. + have ltxy: glt r x y by split. move: (C1 _ _ ltxy) => [z [xz _] yz]. by move: xc; rewrite cxy => /(p1 _ _ ysr xsr) h; case: (h _ xz). + have ltxy: glt r y x by split => //; apply:nesym. move: (C1 _ _ ltxy) => [z [xz _] yz]. by move: yc; rewrite - cxy => /(p1 _ _ xsr ysr) h; case: (h _ xz). + case: c2p=> [t xt ty]. by move: xc; rewrite cxy => /(p1 _ _ ysr xsr) h; case: (h _ xt); apply: Hc. + case: c2p=> [t xt ty]. by move: yc; rewrite - cxy=> /(p1 _ _ xsr ysr) h; case: (h _ xt). move=> adr. have p2: (forall x y, inc x (substrate r) -> inc y (substrate r) -> (sub (canonical_reg_open r x) (canonical_reg_open r y) \/ (exists2 x', gle r x x' & aux x' y))). move=> x y xsr ysr. case: (p_or_not_p (exists2 x', gle r x x' & aux x' y)); first by right. move=> ne; left. move: (Exercise1_23d2 or ysr) => /Exercise1_23aP [o1 ne1]. rewrite(Exercise1_22p or o1); apply: Exercise1_22j => //. by apply: Exercise1_23c. by case: o1. move=> t /Zo_P [tsr xt]. apply/ (p1 _ _ ysr tsr) => z tz; case: (p_or_not_p (aux y z)) => // ayt. by case: ne; exists z; fprops; order_tac. suff:(forall x y : Set, glt r x y -> exists2 z, glt r x z & aux y z). move=> hs; split => // x y xsr ysr. case: (p_or_not_p (gle r x y)) => lexy; first by constructor 1. case: (p_or_not_p (gle r y x)) => leyx; first by constructor 2. case: (p2 _ _ xsr ysr) => q1. case: (p2 _ _ ysr xsr)=> q2. by case: lexy; rewrite (adr _ _ xsr ysr (extensionality q1 q2));order_tac. by constructor 4; move: q2 => [t t1 t2]; exists t => //; apply: Hc. by constructor 3; move: q1 => [t t1 t2]; exists t. move=> x y [xy nxy]. have xsr:(inc x (substrate r)) by order_tac. have ysr:(inc y (substrate r)) by order_tac. case: (p2 _ _ xsr ysr) => h. move: (Exercise1_23f or xy) => /(Exercise1_23bP or) [_ _ _ _ h']. by case: nxy; rewrite (adr _ _ xsr ysr (extensionality h h')). move: h => [u xyu uy]; exists u; fprops;split => // xu. by case: (uy y); [ ue | order_tac]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)