proposition: Fact add_edge_node_y : node (Icp y : H) = IcpXe.
proof: Proof. by rewrite /= eqxx eq_sym (negbTE xDy). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)