proposition: Lemma add_node_adjnXeXe : adjn (IcpXe : h_add_node) IcpXe = false.
proof: Proof. apply/negbTE/negP=>/exists_inP [z]; rewrite inE add_node_cnodeXe => /eqP->. by rewrite inE add_node_cnodeXe. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)