proposition: Lemma genus_mergeX (G : hypermap) (x y : G) : cnode x y (+) cface x y -> genus (merge x y) = genus G.
proof: Proof. move => cn_cf_xy. have xDy : x != y by apply: contraTneq cn_cf_xy => ->; rewrite !connect0. have fI := finv_inj faceI; have nI := finv_inj nodeI. rewrite /genus /Euler_lhs /= (n_comp_mergeX xDy cn_cf_xy) -/(Euler_lhs G). rewrite {1}/Euler_rhs /= !fcard_switch ?inj_eq // 1?eq_sym //; last exact: fI. move: cn_cf_xy. rewrite -{2}[x](f_finv faceI) -{2}[y](f_finv faceI) -cface1 -cface1r cfaceC. case: (boolP (cnode x y)) => /= => [_ /negbTE->|_ ->]. - rewrite addSnnS prednK //; apply/fcard0P => //; [exact: faceI|by exists x]. - rewrite -addSnnS prednK //; apply/fcard0P => //; [exact: nodeI|by exists x]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)