proposition: Lemma union_plane_embedding (G H : sgraph) : plane_embedding G -> plane_embedding H -> plane_embedding (G ∔ H).
proof: Proof. move=> g h; pose D := (emb_map g ∔ emb_map h)%H. pose g' : D -> (G ∔ H)%sg := sumf g h. have emb_g' : embedding g'. { split. - have ? := plane_emb_plain g; have ? := plane_emb_plain h. apply/plainP => -[x|x] _ /=; rewrite inj_eq ?plain_eq ?plain_neq //. exact: inl_inj. exact: inr_inj. - move=> [y|y]; apply/codomP. + by have/codomP [x ->] := plane_emb_surj g y; exists (inl x). + by have/codomP [x ->] := plane_emb_surj h y; exists (inr x). - move => [x|x] [y|y]. all: rewrite /= fconnect_sumf // ?(inj_eq inl_inj) ?(inj_eq inr_inj). all: exact/emb_vertex/emb_embedding. - move => [x|x] [y|y]; rewrite union_adjn //= /edge_rel/=. all: exact: plane_emb_edge. } have : planar D by apply/union_planar; split; exact: emb_planar. exact: Build_plane_embedding emb_g'. 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)