proposition: Lemma diskN_E x : (x \in diskN) = (x \in r) || (x \in diskE).
proof: Proof. rewrite !inE; case r_x: (x \in r) => //=. rewrite -[x](f_finv nodeI) -(fclosed1 diskN_node). by apply/hasP; exists x; last apply: connect0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)