proposition: Lemma del_node_cnode (u v : del_node) : cnode u v = cnode (val u) (val v).
proof: Proof. by rewrite fconnect_frestrict fconnect_skip //; apply: valP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)