proposition: Lemma Exercise1_22qP: (doubletonp (reg_opens r)) <-> (nonempty (substrate r) /\ (right_directed r)).
proof: Proof. have pa: inc emptyset (reg_opens r). apply /Zo_P; split; [apply /setP_P; fprops | apply: Exercise1_22m]. have pb: inc (substrate r) (reg_opens r). apply /Zo_P; split; [apply /setP_P; fprops | apply: Exercise1_22n]. split. move=> [a [b [ab sd]]]. have : (inc a (reg_opens r)) by rewrite sd; fprops. have : (inc b (reg_opens r)) by rewrite sd; fprops. move /Zo_P => [] /setP_P bsr ob /Zo_P [] /setP_P asr oa. split. case: (emptyset_dichot a); last by move=> [a' a'a]; exists a'; apply: asr. case: (emptyset_dichot b); last by move=> [b' b'b]; exists b'; apply: bsr. by move => be ae; case: ab; rewrite ae be. ex_middle nrd; move:(Exercise1_22o nrd) =>[u [v [ou ov neu nev uv]]]. have uo := reg_opens_i ou. have vo := reg_opens_i ov. have c2: ~ (inc emptyset (doubleton u v)). case/set2_P => h' ;[ case: neu | case: nev]; move=> y; rewrite -h'; case; case. rewrite sd in uo vo pa. case/set2_P: uo => vu; case/set2_P:vo => vv; try (rewrite -vu in vv; case: uv; fprops); case: c2;rewrite vu vv //; rewrite set2_C //. move=> [ner rdr]; exists emptyset; exists (substrate r); split => //. by move=> esr; rewrite -esr in ner; case /nonemptyP: ner. set_extens t; last by case/set2_P => ->. move /Zo_P=> [tse ot]; case: (emptyset_dichot t); first by move => ->; fprops. move=> [y yt]; apply /set2_P; right; move /setP_P: tse => tse. apply: extensionality => // u usr. move: (ot) => [ot1 _]; rewrite (Exercise1_22p ot); apply: Exercise1_22h => //. move=> v uv. have vsr: inc v (substrate r) by order_tac. move: rdr => /right_directedP [_ h]. move: (h _ _ (tse _ yt) vsr) => [z [zy zv]]. move: ot1 =>[_ ot2]; move: (ot2 _ _ yt zy)=> zt; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)