proposition: Lemma Exercise1_23aP r X: inc X (nreg_opens r) <-> (open_r r X /\ nonempty X).
proof: Proof. split. by move /Zo_P => [] /Zo_hi xe /set1_P xne;split => //; apply /nonemptyP. move => [pa pb]; apply /Zo_P;split; first by apply reg_opens_i. by move /set1_P; apply /nonemptyP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)