proposition: Lemma n_comp_merge_rest (G : hypermap) (x y : G) (xDy : x != y) : n_comp glink [predC closure glink (pred2 x y)] = n_comp (glink : rel (merge x y)) [predC closure (@glink (merge x y)) (pred2 x y)].
proof: Proof. set a := closure glink (pred2 x y). set b := closure (@glink (merge x y)) (pred2 x y). have eq_b_a : b =i a by apply closure_merged. have C_ab : [predC b] =i [predC a] by move=>z;rewrite [in RHS]inE/= -eq_b_a. have [? ?] : x \in pred2 x y /\ y \in pred2 x y by rewrite !inE !eqxx. rewrite (eq_n_comp_r C_ab); apply: (@in_eq_n_comp). - move => u v /=. exact: glinkC. - move => u v /=. exact: (@glinkC (merge x y)). - apply/predC_closed/closure_closed. exact: glinkC. - apply/predC_closed; rewrite -(eq_closed_r eq_b_a). apply: closure_closed. exact: (@glinkC (merge x y)). - move => u v Hu _. rewrite !inE/= in Hu; rewrite /glink /= !ifF //. + apply: contraNF Hu => /eqP->. apply/closureP; exists x => //. apply gcompF. by rewrite cface1 f_finv. + apply: contraNF Hu => /eqP->. apply/closureP; exists y => //. apply gcompF. by rewrite cface1 f_finv. + apply: contraNF Hu => /eqP->. exact: mem_closure. + apply: contraNF Hu => /eqP->. exact: mem_closure. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)