fact: Definition adjn {D : hypermap} (x y : D) := [exists z in cnode x, edge z \in cnode y].
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)