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