proposition: Lemma add_edge_can3 : cancel3 add_edge_edge add_edge_node add_edge_face.
proof: Proof. case => [||z]; rewrite /= ?eqxx ?[y == x]eq_sym ?(negbTE xDy) //. case: (altP (face (edge z) =P x)) => /= [<-|Dx]; first by rewrite edgeK. case: (altP (face (edge z) =P y)) => /= [<-|Dy]; first by rewrite edgeK. by rewrite (negbTE Dx) (negbTE Dy) edgeK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)