proposition: Lemma diskF_face : fclosed face diskF.
proof: Proof. apply: (intro_closed cfaceC) => x _ /eqP <- /andP[/= F'x dNx]. rewrite inE /= -(fclosed1 (fbandF r)) F'x. have [y ry y'Dx] := hasP dNx; apply/hasP; exists y => //=. rewrite /dconnect /= (connect_trans y'Dx) ?connect1 /dlink //= clinkF andbT. by apply: contra F'x => rx; apply: (subsetP (ring_fband r)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)