proposition: Lemma Exercise1_22o: ~ (right_directed r) -> exists a b, [/\ open_r r a, open_r r b, nonempty a, nonempty b & a <> b].
proof: Proof. move=> nrd. pose i x := Zo (substrate r) (gle r x). have io: (forall x, inc x (substrate r) -> open_o r (i x)). move=> x xsr; split; first by apply: Zo_S. move => a b /Zo_P [asr xa] ab; apply /Zo_P;split; order_tac. have obi: (forall x, inc x (substrate r) -> open_r r (open_bar r (i x))). by move=> x xsr; apply: Exercise1_22i =>//; apply: io. have bne1: forall x, inc x (substrate r) -> inc x (open_bar r (i x)). move=> x xsr; apply: Exercise1_22e =>//; [ apply: io => //| apply: Zo_i =>//]. by order_tac. pose p a b := [/\ inc a (substrate r),inc b (substrate r) & disjoint (i a) (i b)]. case: (p_or_not_p (exists a b, p a b)). move=> [a [b [asr bsr iabe]]]. move: (bne1 _ asr) (bne1 _ bsr) => a1 b1. exists (open_bar r (i a)); exists (open_bar r (i b)); split;fprops. by exists a. by exists b. move: (Exercise1_22k (io _ asr) (io _ bsr) iabe). rewrite /disjoint. by move=> ie sv; rewrite sv in ie; empty_tac1 b; apply: setI2_i. move=> h; case: nrd; apply /right_directedP; split => //. move=> x y xsr ysr; ex_middle ep; case: h. exists x, y; split => //. apply /set0_P; move=> t /setI2_P [] /Zo_P [tsr xt] /Zo_P [_ yt]. by case: ep; exists t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)