proposition: Lemma diskN_node : fclosed node diskN.
proof: Proof. suffices clN'dN: fclosed (finv node) diskN. apply: (intro_closed cnodeC) => x _ /eqP <- dNx. by rewrite (fclosed1 clN'dN) (finv_f nodeI). have nodeI' := finv_inj (@nodeI G). apply: (intro_closed (fconnect_sym nodeI')) => x _ /eqP <- dNx; apply/hasP. case rx: (x \in r); first by exists x; rewrite /dconnect /=. have [z rz z'Dx] := hasP dNx; exists z => //. by apply: connect_trans z'Dx (connect1 _); rewrite /dlink /= rx /clink /= eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)