fact: Definition del_node_face_ := finv (frestrict del_node_hom) \o finv (frestrict del_edge_hom).
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)