proposition: Lemma Exercise6_31_r z: inc z Z <-> (z <> emptyset /\ open_r r' z).
proof: Proof. rewrite /Z/nreg_opens. split; first by move => /setC1_P [/Zo_hi za znz]. move =>[aa /reg_opens_i qb]; apply/setC1_P; split => //. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)