proposition: Lemma component_separation (G : sgraph) (A S : {set G}) x : smallest vseparator S -> x \in A -> [disjoint A & S] -> connected A -> {in A & ~: A, forall x y, x--y -> y \in S} -> proper_separation (A :|: S) (~: A :|: S).
proof: Proof. move=> [sepS minS] x_A dis_A_S conA compA. case: sepS => [u[v sep_uv]]. have Huv : (u \notin A) || (v \notin A). { apply: contraTT (dis_A_S); rewrite negb_or !negbK => /andP [u_A v_A]. have uDv := separatesNeq sep_uv. have/(connect_irredRP uDv) [p Ip /subsetP subA] := conA _ _ u_A v_A. case: sep_uv => uNS vNS /(_ p) [z /subA ? ?]. by apply/pred0Pn; exists z. } wlog uNA : u v sep_uv {Huv} / u \notin A => [W|]. { case/orP: Huv; apply: W;[|rewrite separates_sym]; exact: sep_uv. } case: (sep_uv) => uNS vNS sepS. split; first split. - by move => z; rewrite !inE; case: (z \in A). - move => x1 x2. rewrite !inE !negb_or !negbK => /andP [x1_A x1NS] /andP [x2_A]. by apply: contraNF => /compA; apply; rewrite ?inE. - by exists x,u; rewrite !inE x_A (disjointFr dis_A_S) //= negb_or uNA uNS. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)