proposition: Lemma del_node_faceE : @face del_node =1 (frestrict del_face_hom).
proof: Proof. suff: cancel3 (frestrict del_edge_hom) (frestrict del_node_hom) (frestrict del_face_hom). { move/canF_sym. apply: inj_can_eq (@faceK del_node) _. by move => x y /edgeI/nodeI. } move => x. apply/val_inj; rewrite !val_frestrict /del_node_face. case: (boolP (face (edge (val x)) \in N)) => H. - have Hz : ~~ cnode z (face (edge (val x))). { apply: contraNN (valP x). rewrite cnode1r edgeK. exact: mem_closure. } have H' := del_node_neighbor1' Hz H. by rewrite skip2 // f_finv // edgeK. - rewrite skip1 // edgeK //. exact: valP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)