proposition: Lemma plane_add_node (G : sgraph) (g : plane_embedding G) (x y : G) s1 s2 (A : {set G}) : x != y -> sface g (x :: s1 ++ y :: s2) -> {subset A <= x :: rcons s1 y} -> x \in A -> y \in A -> exists (g' : plane_embedding (add_node G A)), sface g' [:: Some x, None & [seq Some z | z <- y::s2]].
proof: Proof. move=> xDy face_s subA x_A y_A. suff [h face_h] : exists h : plane_embedding (add_edges2 (add_node G [set x]) [set None] (Some @: (A :\ x))), sface h [:: Some x, None & [seq Some z | z <- y :: s2]]. { set i := add_node_diso x_A; exists (diso_plane_embedding h i). by move: face_h; rewrite (diso_face _ i) map_id_in. } have [g'] := plane_add_node1 face_s. set G' := add_node _ _; rewrite map_cat /=. set y' := Some y; set x' := Some x; set s1' := map Some s1; set s2' := map Some s2. set A' := Some @: (A :\ x). move/(rot_face 1) => face_g'. have {face_g'} face_g' : sface g' (None :: (x'::s1') ++ y' :: rcons s2' x'). { by move: face_g'; rewrite rot1_cons /= rcons_cat /=. } have y_A' : y' \in A' by rewrite imset_f // !inE eq_sym xDy. have subA' : {subset A' <= x' :: rcons s1' y'}. { move=> ? /imsetP [u /setD1P [uDx /subA uA] ->]. by move: uA; rewrite -(mem_map Some_inj) /= map_rcons. } have [//||h face_h] := plane_add_fan _ face_g' _ y_A' subA'. by apply/negP=>/imsetP [?]. exists h. move/(rotr_face 1) : face_h. by rewrite -!rcons_cons rotr1_rcons. 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)