proposition: Lemma edge_plane_embedding (G : sgraph) (V1 V2 : {set G}) (x y : G) : x -- y -> V1 :&: V2 = [set x; y] -> separation V1 V2 -> plane_embedding (induced V1) -> plane_embedding (induced V2) -> inhabited (plane_embedding G).
proof: Proof. move => xy capV sepV. have [xV1 xV2 yV1 yV2] : [/\ x \in V1, x \in V2, y \in V1 & y \in V2]. by split; set_tac. have xDy : x != y by rewrite (sg_edgeNeq xy). set G1 := induced V1; set G2 := induced V2; move => g1 g2. set G12 := (G1 ∔ G2)%sg. have g12 := union_plane_embedding g1 g2. pose x1 : G12 := inl (Sub x xV1); pose x2 : G12 := inr (Sub x xV2). pose y1 : G12 := inl (Sub y yV1); pose y2 : G12 := inr (Sub y yV2). have xy1 : x1 -- y1 by []. have yx2 : y2 -- x2 by rewrite sgP. have nc_x1_x2 : ~~ connect (--) x1 x2 by rewrite sjoin_disconnected. have [xs face_xs] := plane_emb_face g12 xy1. have [ys face_ys] : exists ys, sface g12 (x2 :: rcons ys y2). { have [ys face_ys] := plane_emb_face g12 yx2. by exists ys; move/(rot_face 1) : face_ys; rewrite rot1_cons. } pose Gm := smerge2 G12 x1 x2. have := smerge_plane_embedding_disconnected' nc_x1_x2 face_xs face_ys. rewrite -/Gm => -[g' [s' [face_s' eq_val_s]]]. have y1Gm : y1 != x2 by []. have y2Gm : y2 != x2 :> G12 by rewrite (inj_eq inr_inj) eq_sym -val_eqE. pose y1' : Gm := Sub y1 y1Gm. pose y2' : Gm := Sub y2 y2Gm. pose Gm' := smerge2 Gm y1' y2'. have [y1s' y2s'] : y1' \in s' /\ y2' \in s'. { by rewrite -!(mem_map val_inj) !eq_val_s // !(inE,mem_cat,mem_rcons) /= !eqxx. } have y1Dy2' : y1' != y2' by rewrite -val_eqE. have y1Ny2' : ~~ y1' -- y2'. { by rewrite /edge_rel/= eq_sym (inj_eq inl_inj) -val_eqE /= (negbTE xDy). } have : diso Gm' G by exact: diso_separation2. apply: diso_plane_embedding_inh. exact: smerge_plane_embedding_face face_s'. Qed.
imports: HB(structures) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(sgraph connectivity minor excluded) fourcolor(hypermap geometry walkup color coloring combinatorial4ct) GraphTheory(set_tac) GraphTheory(hmap_ops smerge embedding arc K4plane)