proposition: Lemma adjn_mergeC (G : hypermap) (x y : G) : @adjn[merge G x y] =2 @adjn[merge G y x].
proof: Proof. by move=> u v; rewrite -(hiso_adjn (mergeC_hiso x y)). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)