proposition: Lemma genus_merge (G : hypermap) (x y : G) : ~~ gcomp x y || (cnode x y (+) cface x y) -> genus (merge x y) = genus G.
proof: Proof. case/orP; [exact: genus_mergeG|exact: genus_mergeX]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)