proposition: Lemma adjn_node1 (G : hypermap) (x y : G) : adjn x y = adjn (node x) y.
proof: Proof. by apply: eq_existsb => z; rewrite !inE -cnode1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)