proposition: Lemma add_edge_cnodeXXe : cnode (IcpX : H) IcpXe = cnode x y.
proof: Proof. by rewrite cnode1 cnode1r add_edge_cnodeE -cnode1 -cnode1r. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)