proposition: Fact embd_face_subproof (u : ddart) : embd_face (sval u) \in bc.
proof: Proof. rewrite /embd_face; case: ifP (edge_perimeter (face (val u))) => //= _. by rewrite inE /= (canRL edgeK (e2c _)) -(fclosed1 rcN). 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)