proposition: Fact embd_edge_subproof (u : ddart) : embd_edge (sval u) \in bc.
proof: Proof. rewrite /embd_edge; case: ifPn => // bc'eu. have:= edge_perimeter (node (edge (val u))). by rewrite inE /= -(fclosed1 rcN) -implyNb bc'eu. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring patch) fourcolor(snip revsnip kempe birkhoff contract)