proposition: Lemma subgraph_plane_embedding (G H : sgraph) : subgraph G H -> no_isolated G -> plane_embedding H -> inhabited (plane_embedding G).
proof: Proof. move=> sub_G_H no_isoG [D g emb_g] planarD. have [D'[g' [emb_g']]] := subgraph_embedding sub_G_H no_isoG emb_g. rewrite (eqP planarD) (leqn0) -/(planar D') => planarD'. by exists; apply: Build_plane_embedding emb_g' planarD'. 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)