proposition: Lemma n_comp_mergeX (G : hypermap) (x y : G) (xDy : x != y) : cnode x y (+) cface x y -> n_comp glink (merge x y) = n_comp glink G.
proof: Proof. move => c_xy. 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 (n_comp_merge_rest xDy). suff -> : (gcomp : rel G) x y = (gcomp : rel (merge x y)) x y by []. apply/idP/idP => _; case: (boolP (cnode x y)) c_xy => /= N F. - apply: (@gcompF (merge x y)) => /=. eapply connect_trans with (finv face x). + apply: fconnect_f_switch => //; first by rewrite cface1 f_finv // cfaceC. by rewrite cface1r f_finv. + apply: connect1 => /=. rewrite eqxx. by case: (finv face x =P _) => [->|]; rewrite f_finv. - apply: (@gcompN (merge x y)) => /=. eapply connect_trans with (node y). + apply: connect1 => /=; by rewrite eqxx. apply: fconnect_f_switch => //; by rewrite -?cnode1r -?cnode1. + exact: gcompN. + exact: gcompF. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)