proposition: Lemma planar1 : ~~ connect (--) x y -> planar D'.
proof: Proof. move => nc_xy; apply: merge_planar; last exact: emb_planar. by rewrite (emb_gcomp (emb_embedding g)) g_dx g_dy nc_xy. 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)