proposition: Lemma plane_add_node' (G : sgraph) (g : plane_embedding G) (x y : G) s (A : {set G}) : x \in s -> y \in s -> x != y -> sface g s -> {subset A <= rcons (arc s x y) y} -> uniq s -> x \in A -> y \in A -> exists (g' : plane_embedding (add_node G A)), sface g' [:: Some x, None & [seq Some z | z <- arc s y x]].
proof: Proof. move=> x_s y_s xDy face_s subA uniq_s x_A y_A. have [i s1 s2 arc1 arc2 rot_i] := rot_to_arc uniq_s x_s y_s xDy. rewrite -(arc_rot i) // rot_i right_arc -?rot_i ?rot_uniq //. apply: (plane_add_node (g := g) (s1 := s1)) => //. - rewrite -rot_i. exact: rot_face. - by rewrite -(arc_rot i) // rot_i left_arc -?rot_i ?rot_uniq in subA. 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)