proposition: Lemma emb_inv_node d : cnode d (emb_inv (f d)).
proof: Proof. by rewrite (emb_vertex (emb_f)) emb_invK. 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)