proposition: Lemma add_node_adjnXe u : adjn (IcpXe : h_add_node) (Icp u) = cnode x u.
proof: Proof. apply/exists_inP/idP => [[z]|x_u]. rewrite !inE add_node_cnodeXe cnodeC => /eqP->. by rewrite cnode1 add_node_cnodeE -cnode1. exists IcpXe; rewrite !inE // cnode1r [edge _]/=. by rewrite add_node_cnodeE -cnode1r cnodeC. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)