proposition: Fact dface_subproof (u : ddart) : snipd_face (val u) \in diskN.
proof: Proof. rewrite /= /snipd_face (fclosed1 diskN_node) diskN_E. case ru: (val u \in r); first by rewrite edgeK mem_prev ru. by rewrite orbC (fclosed1 diskE_edge) faceK inE /= ru (valP u). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)