proposition: Lemma del_node_can3: cancel3 (frestrict del_edge_hom) (frestrict del_node_hom) del_node_face_.
proof: Proof. move => x; rewrite /del_node_face_ /= finv_f ?f_finv //. - by apply/frestrict_inj/skip_inj. - apply/frestrict_inj. exact: in2W edgeI. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)