proposition: Fact snipd_subproof : cancel3 dedge dnode dface.
proof: Proof. move=> u; apply: val_inj; rewrite /= /snipd_edge. case ru: (val u \in r); rewrite /snipd_face. by rewrite mem_next ru edgeK (prev_next Ur). have dEu: edge (val u) \in diskE. by rewrite -(fclosed1 diskE_edge) inE /= ru (valP u). by case/andP: dEu => /negPf/=->; rewrite edgeK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan color geometry patch)