proposition: Lemma edge_separator (G : sgraph) (x y : G) : 4 < #|G| -> 3.-connected G -> x -- y -> ~ 3.-connected (smerge2 G x y) -> exists z, vseparatorb [set x;y;z].
proof: Proof. move => largeG conn3G xy nconn3Gxy. have conn2Gxy : 2.-connected (smerge2 G x y) by apply: smerge_konnected. have [|S /cards2P [z[w [zDw ->] [sep_zw small_zw]]]] := kconnected_bounds _ conn2Gxy nconn3Gxy; first by rewrite -ltnS card_smerge2. have xDy : x != y by rewrite sg_edgeNeq. pose x' : smerge2 G x y := Sub x xDy. have x_in : x' \in [set z; w]. { apply: contraPT conn3G => Hx [_ min3]. have /min3 := separator_from_smerge2 sep_zw Hx. by rewrite card_imset // cards2; case: (_ == _). } wlog have: z w zDw sep_zw {x_in small_zw} / w = x' => [W|]; last subst w. { case/set2P : x_in => /esym; last exact: W sep_zw. rewrite eq_sym setUC in sep_zw zDw. exact: W sep_zw. } exists (val z); apply/vseparatorP. have := smerge2_separator sep_zw. by rewrite imsetU !imset_set1 /= [[set _;x]]setUC setUA [[set _;x]]setUC. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)