proposition: Lemma add_node_can3 : cancel3 add_node_edge add_node_node add_node_face.
proof: Proof. case => [||z]; rewrite /= ?eqxx //. case: (eqVneq (face (edge z)) x) => /= [<-|Dx]; by rewrite ?(negbTE Dx) edgeK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)