proposition: Lemma n_comp_mergeG (G : hypermap) (x y : G) : ~~ gcomp x y -> (n_comp glink (merge x y)).+1 = (n_comp glink G).
proof: Proof. move=> gcNxy. have xDy : x != y by apply: contraNneq gcNxy => ->. pose a := closure glink (pred2 x y). pose b := closure (@glink (merge x y)) (pred2 x y). have eq_b_a : b =i a by apply closure_merged. rewrite (n_compC b) (n_compC a) !n_comp_closure2; try exact:glinkC. rewrite gcNxy /= add2n addSn -(n_comp_merge_rest xDy) -/a. rewrite [connect _ _ _](_ : _ = true) //. apply: (@gcompN (merge x y)). rewrite fconnect_switched => //; last exact: (@nodeI G). apply: contraNN gcNxy. exact: gcompN. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)