proposition: Lemma small_planar (G : sgraph) : #|G| <= 4 -> no_isolated G -> inhabited (plane_embedding G).
proof: Proof. move=> smallG no_isoG. exact: subgraph_plane_embedding (sub_Kn smallG) no_isoG K4_plane_emb. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry) GraphTheory(preliminaries digraph sgraph) GraphTheory(hmap_ops embedding)