proposition: Lemma smerge_plane_embedding_disconnected : ~~ connect (--) x y -> inhabited (plane_embedding (smerge2 G x y)).
proof: Proof. move => n_xy. have [dx /esym g_dx] := codomP (plane_emb_surj g x). have [dy /esym g_dy] := codomP (plane_emb_surj g y). have xDy : x != y by apply: contraNneq n_xy => ->. have emb_g' : embedding (@g' dx dy xDy). by apply: embedding_g' => //; apply: contraNF n_xy; exact: connect1. constructor; apply: Build_plane_embedding emb_g' _. exact: planar1. 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)