proposition: Lemma adjn_edge (G : hypermap) (x : G) : adjn x (edge x).
proof: Proof. exact: (adjnI G x). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)