proposition: Lemma closure_merged (G : hypermap) (x y : G) (xDy : x != y) : closure (@glink (merge x y)) (pred2 x y) =i closure glink (pred2 x y).
proof: Proof. wlog suff S : G x y xDy / closure (@glink (merge x y)) (pred2 x y) \subset closure glink (pred2 x y). { apply/subset_eqP/andP; split; first exact: S. suff E: @glink (@merge (merge x y) x y) =2 @glink G. rewrite -(eq_subset (eq_closure _ (eq_connect E))). exact: S. case: G x y {xDy} => D e n f eK x y. pose i := merge_inv x y. by apply: (hiso_id_glink i). } apply/subsetP => z /closureP [x0]; rewrite !inE => x_or_y. wlog -> : G x y xDy z x0 {x_or_y} / x0 = x. { move => W. case/pred2P : x_or_y => [|A B]; first exact: W. have {B} B : (gcomp : rel (merge y x)) z x0 by rewrite -(eq_connect (hiso_id_glink (mergeC x y) _)). have {W} W := W G y x _ z x0 A B. rewrite (eq_closure_r (_ : pred2 x y =i pred2 y x)) ?W 1?eq_sym //. by move => u ; rewrite !inE orbC. } rewrite -clink_glink ; case/connectP => p. elim: p z => /= [z _ -> |z p IH z' /andP [l_z'_z pth_p] lst_p]; first by apply: mem_closure; rewrite !inE eqxx. have {IH pth_p lst_p} IHp := IH _ pth_p lst_p. rewrite -(eq_closure _ (@clink_glink _)); rewrite -(eq_closure _ (@clink_glink _)) in IHp. have [? ?] : x \in pred2 x y /\ y \in pred2 x y by rewrite !inE !eqxx. case/clinkP : l_z'_z => [E|]. - rewrite {}E /=. case: (altP (z =P x)) => [Ez|zDx]; last case: (altP (z =P y)) => [Ez |zDy]. + apply/closureP; exists y => //. by rewrite connect1 // clinkN. + apply/closureP; exists x => //. by rewrite connect1 // clinkN. + apply: closure_connect IHp. by rewrite connect1 // clinkN. - have F (u:G) : connect clink (finv face u) u. { apply: connect_trans (connect1 clinkF) _. by rewrite (f_finv faceI). } case: (altP (z' =P finv face y)) => [-> _|N1]; first by apply/closureP; exists y. case: (altP (z' =P finv face x)) => [-> _|N2 E]; first by apply/closureP; exists x. rewrite /= (negbTE N1) (negbTE N2) in E; rewrite -[z'](finv_f faceI) E. apply: closure_connect IHp. apply: connect_trans (connect1 clinkF) _. by rewrite (f_finv faceI). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)