proposition: Lemma vertex_plane_embedding (G : sgraph) (V1 V2 : {set G}) (x : G) : V1 :&: V2 = [set x] -> separation V1 V2 -> plane_embedding (induced V1) -> plane_embedding (induced V2) -> inhabited (plane_embedding G).
proof: Proof. move => capV sepV g1 g2. have [xV1 xV2] : x \in V1 /\ x \in V2 by split; set_tac. pose G1 := induced V1; pose G2 := induced V2. have : diso (smerge2 (G1 ∔ G2) (inl (Sub x xV1)) (inr (Sub x xV2))) G. exact: diso_separation1. apply: diso_plane_embedding_inh. apply: smerge_plane_embedding_disconnected. by apply: union_plane_embedding. exact: sjoin_disconnected. 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)