proposition: Lemma plane_add_edge' (G : sgraph) (g : plane_embedding G) (x y : G) (s : seq G) : x != y -> sface g s -> x \in s -> y \in s -> uniq s -> exists g' : plane_embedding (add_edge x y), sface g' (rcons (arc s x y) y) /\ sface g' (rcons (arc s y x) x).
proof: Proof. Abort. Section AddEdges2. Variables (G : sgraph) (U V : {set G}). Definition add_edges2_rel := [rel u v : G | u -- v || (u != v) && ((u \in U) && (v \in V) || (u \in V) && (v \in U))]. Fact add_edges2_irrefl : irreflexive add_edges2_rel. Proof. by move=> x /=; rewrite sg_irrefl eqxx. 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)