proposition: Lemma plane_add_fan (G : sgraph) (g : plane_embedding G) x y s1 s2 (A : {set G}) : x != y -> sface g (x :: s1 ++ y :: s2) -> x \notin A -> y \in A -> {subset A <= rcons s1 y} -> exists g' : plane_embedding (add_edges2 G [set x] A), sface g' [:: x, y & s2].
proof: Proof. move=> xDy face_g xNA y_A subA. pose As := undup [seq z <- s1 | z \in A :\ y]. have subAs : subseq As s1. by apply: subseq_trans (undup_subseq _) _; apply: filter_subseq. have yNAs : y \notin As by rewrite mem_undup mem_filter !inE eqxx. have xNAs : x \notin As by rewrite mem_undup mem_filter !inE (negPf xNA). have -> : A = y |: [set z in As]. apply/setP => u; rewrite !inE mem_undup mem_filter !inE. have [-> //|/= uDy] := eqVneq u y. rewrite andb_idr // => /subA. by rewrite mem_rcons inE (negPf uDy). have uniq_As : uniq As by apply: undup_uniq. move: As subAs xNAs yNAs uniq_As => {A y_A xNA subA} As. have [n Hn] := ubnP (size As). elim: n G g x y s1 s2 xDy face_g As Hn => // n IH G g x y s1 s2 xDy face_g. case => [_ _ _ _ _|z As /= /ltnSE lt_As_n]. - rewrite set_nil setU0. have [h _ face_h] := plane_add_edge xDy face_g. set i := add_edge11_diso x y; exists (diso_plane_embedding h i). by move/(diso_face h i): face_h; rewrite map_id_in. - rewrite !inE !negb_or => subAs /andP[xDz xNAs] /andP [yDz yNAs] /andP[zNAs uniq_As]. have z_s1 : z \in s1 by apply/(mem_subseq subAs)/mem_head. case/splitPr def_s1 : _ / z_s1 => [p1 p2 zNp1]. have/plane_add_edge: sface g (x :: p1 ++ z :: p2 ++ y :: s2). by move: face_g; rewrite def_s1 /= -catA. move/(_ xDz) => [g' _ face_g']. have [//||//|//|//|h face_h] := IH (add_edge G x z) g' x y (z::p2) s2 xDy _ _ lt_As_n. + by move: subAs; rewrite def_s1; exact: subseq_notin. + set G' := add_edges2 _ _ _. have @i: diso (add_edges2 (add_edge G x z) [set x] (y |: [set z0 in As])) G'. { apply: eq_diso. abstract (rewrite set_cons setUA [[set _;_]]setUC -setUA; exact: add_edge1n_diso_proof). } exists (diso_plane_embedding h i). by move/(diso_face h i): face_h; rewrite map_id_in. 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)