proposition: Lemma add_node_cnodeXe u : cnode (IcpXe : h_add_node) u = (u == IcpXe).
proof: Proof. by apply/idP/eqP => [/connectP []|-> //]; elim => //= a p IH /andP[/eqP<-]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)