proposition: Lemma adjnI (G : hypermap) (z x y : G) : cnode x z -> cnode y (edge z) -> adjn x y.
proof: Proof. by move => ? ?; apply/exists_inP; exists z. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)