proposition: Lemma simple_embedding (g : plane_embedding G) : exists g' : plane_embedding G, simple_hmap (emb_map g').
proof: Proof. case: g => D g emb_g planarD. have [D' [g' [simpleD' emb_g' le_genus]]] := remove_parallel emb_g. have planarD' : planar D' by exact: le_genus_planar planarD. by exists (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)