proposition: Lemma diso_plane_embedding_inh (G H : sgraph) : inhabited (plane_embedding G) -> diso G H -> inhabited (plane_embedding H).
proof: Proof. move => [g i]; constructor. exact: diso_plane_embedding i. 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)