proposition: Lemma plane_add_node_simple (G : sgraph) (g : plane_embedding G) s (A : {set G}) x : x \in A -> sface g s -> {subset A <= s} -> inhabited (plane_embedding (add_node G A)).
proof: Proof. have [gt1A _ {x} face_s subA|le1A xA] := ltnP 1 #|A|; last first. - have/eqP eq_A : A == [set x]; last subst A. { by apply/eq_set1P; split => // y yA; apply: (card_le1_eqP le1A). } move=> face_s subXs; have x_s : x \in s by apply: subXs; rewrite in_set1. have [i s' rot_i] := rot_to x_s; move/(rot_face i): face_s; rewrite rot_i. by case/plane_add_node1. - have : exists x y s1 s2 i, rot i s = x :: s1 ++ y :: s2 /\ x != y /\ [disjoint A & s2] /\ x \in A /\ y \in A. { have [x [y [s1 [s2 [s3 [xA yA xDy def_s disA]]]]]] := foo gt1A subA. exists y,x,(s3++s1),s2,(size (s1 ++ x :: s2)). by rewrite def_s -!cat_cons catA rot_size_cat eq_sym /= -catA. } move => [x] [y] [s1] [s2] [i] [rot_i [xDy [disjA [xA yA]]]]. move/(rot_face i) in face_s; rewrite rot_i in face_s. have [|//|//|//] := @plane_add_node _ _ _ _ _ _ A xDy face_s. move=> a aA; move: (aA) => /subA. rewrite -(mem_rot i) rot_i !(inE,mem_cat,mem_rcons) (disjointFr disjA) //. by rewrite orbF => /or3P[->|->|->]. 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)