proposition: Lemma add_node_adjn u v : adjn (Icp u : h_add_node) (Icp v) = adjn u v.
proof: Proof. apply/exists_inP/exists_inP => [|[z Z1 Z2]]; last by exists (Icp z); rewrite inE add_node_cnodeE. move=> [[||z] Z1 Z2]; rewrite !inE [edge _]/= in Z1 Z2. - by rewrite cnodeC add_node_cnodeXe in Z2. - by rewrite cnodeC add_node_cnodeXe in Z1. - by exists z; rewrite inE -add_node_cnodeE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)