proposition: Lemma plane_emb_vertex d1 d2 : cnode d1 d2 = (g d1 == g d2).
proof: Proof. exact: emb_vertex. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)