proposition: Lemma smerge_plane_embedding_face s : x \in s -> y \in s -> x != y -> ~~ x -- y -> sface g s -> inhabited (plane_embedding (smerge2 G x y)).
proof: Proof. move => x_s y_s xDy xNy []; rewrite -/D => dz def_s. rewrite def_s in x_s y_s. have [dx fdx /esym g_dx] := mapP x_s. have [dy fdy /esym g_dy] := mapP y_s. pose D' := merge D dx dy. have emb_g' : embedding (@g' dx dy xDy). apply: embedding_g' => //. exact: negbTE. constructor; apply: Build_plane_embedding emb_g' _. apply: merge_planar; last exact: emb_planar. rewrite plane_emb_vertex g_dx g_dy (negbTE xDy) /=. rewrite -!fconnect_orbit in fdx fdy. by rewrite (connect_trans _ fdy) // cfaceC. 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)