proposition: Lemma genus_mergeG (G : hypermap) (x y : G) : ~~ gcomp x y -> genus (merge x y) = genus G.
proof: Proof. move=> gcNxy. have [? ?] := (@nodeI G, @faceI G). have fI := finv_inj (@faceI G). have xDy : x != y by apply: contraNneq gcNxy => ->. have cxyF : cnode x y = false. apply: contraNF gcNxy. exact: gcompN. have fxyF : cface x y = false. apply: contraNF gcNxy. exact: gcompF. rewrite /genus /Euler_lhs /= -(n_comp_mergeG gcNxy). rewrite doubleS -add2n -addnA -/(Euler_lhs (merge x y)). suff -> : Euler_rhs G = (Euler_rhs (merge x y)).+2. by rewrite -[(Euler_rhs (merge x y)).+2]addn2 addnC subnDr. rewrite /Euler_rhs !fcard_switch // ?(inj_eq fI) 1?eq_sym //. rewrite cxyF. rewrite (@cface1 G) (@cface1r G) !f_finv // cfaceC fxyF /=. rewrite -2!addnS; congr (_ + _); rewrite -addnS -addSn !prednK //. all: by apply/fcard0P => //; exists x. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)