fact: Definition add_edge_node (z : ecp_dart G) : ecp_dart G := match z with | IcpX => Icp (node x) | IcpXe => Icp (node y) | Icp z' => if z' == x then IcpX else if z' == y then IcpXe else Icp (node z') end.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)