proposition: Lemma svseparator_connected S : smallest vseparator S -> 0 < #|S| -> connected [set: G].
proof: Proof. move => SS gt0 x y _ _. have: (connect (restrict [predC set0] sedge) x y). { apply (@separatesNE x y set0); rewrite ?inE => //. rewrite -(@cards0 G) in gt0. move: (below_smallest SS gt0). exact: vseparatorNE. } rewrite !restrictE //; intro; rewrite !inE //. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)