proposition: Lemma kconnected_bounds (G : sgraph) k : k.+1 < #|G| -> k.-connected G -> ~ k.+1.-connected G -> exists2 S : {set G}, #|S| == k & smallest vseparator S.
proof: Proof. move => large_G [_ min_k]. move/kconnectedP; rewrite negb_and large_G /= => /forall_inPn [S]. move/vseparatorP; rewrite -leqNgt => S1 S2; exists S => //. - by rewrite eqn_leq S2 min_k. - split => // V /min_k. exact: leq_trans. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)