proposition: Lemma smerge_plane_embedding_disconnected' xs ys : ~~ connect (--) x y -> sface g (x :: xs) -> sface g (y :: ys) -> exists (g' : plane_embedding (smerge2 G x y)) s', sface g' s' /\ {subset [predD1 x :: xs ++ ys & y] <= map val s'}.
proof: Proof. move => n_xy. case => dx. move: (fconnect_orbit face dx). case: (orbit_case face dx) => dxs -> /= f_dx [/esym g_dx def_xs]. case => dy. move: (fconnect_orbit face dy). case: (orbit_case face dy) => dys -> /= f_dy [/esym g_dy def_ys]. have xDy : x != y by apply: contraNneq n_xy => ->. have dxDdy : dx != dy by apply: contra_neq xDy => E; rewrite -g_dx E g_dy. have emb_g' : embedding (@g' dx dy xDy). by apply: embedding_g' => //; apply: contraNF n_xy; exact: connect1. pose D' := merge D dx dy. have planarD' : planar D' by apply: planar1. have fI := @faceI D. have fxy : @cface[D'] (finv face dy) (finv face dx). { rewrite fconnect_switched // ?(inj_eq (finv_inj fI)) 1?eq_sym //. rewrite (@cface1 D) (@cface1r D) !f_finv // cfaceC. apply: contraNN n_xy; rewrite -g_dx -g_dy. exact: face_connect. } have subDD' : subrel @cface[D] @cface[D']. { apply switch_subrel; rewrite // -fconnect_switched //. by rewrite ?(inj_eq (finv_inj fI)) 1?eq_sym. } pose h := Build_plane_embedding emb_g' planarD'; exists h. exists (map h (@orbit D' face (finv (@face D) dx))); split; first by exists (finv face dx). move => z /andP [zDy /= Hz]. suff: exists2 dz : D, g dz = z & @cface[D'] (finv face dx) dz. { case => dz g_dz; rewrite fconnect_orbit -map_comp => orb_z. by apply/mapP; exists dz => //=; rewrite /g' altF ?g_dz. } move: Hz; rewrite !(inE,mem_cat) def_xs def_ys => /or3P[/eqP -> {zDy z}||]. - exists dx => //. rewrite cfaceC. apply: connect_trans fxy. rewrite cfaceC. apply: connect1. by rewrite /= eqxx f_finv. - case/mapP => dz Hdz /esym g_dz; exists dz => //. apply: subDD'. by rewrite cface1 f_finv // f_dx inE Hdz. - case/mapP => dz Hdz /esym g_dz; exists dz => //; rewrite cfaceC. apply: connect_trans fxy. apply: subDD'. by rewrite cfaceC cface1 f_finv // f_dy inE Hdz. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)