proposition: Lemma adjnC (G : hypermap) (x y : G) : plain G -> adjn x y = adjn y x.
proof: Proof. move=> plain_G. wlog suff S : x y / adjn x y -> adjn y x; first by apply/idP/idP; exact: S. case/exists_inP => z; rewrite !inE => x_z z_ez. by apply/exists_inP; exists (edge z); rewrite // plain_eq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)