proposition: Lemma connectedVseparator (G : sgraph) k : k < #|G| -> k.-connected G + { S : {set G} | #|S| < k & vseparator S}.
proof: Proof. move => gtk. case: (boolP (kconnectedb k G)) => [/kconnectedP|]; first by left. rewrite negb_and gtk /= => /forallPn => ex_S. have := xchooseP (ex_S); rewrite negb_imply -ltnNge => /andP [/vseparatorP ? ?]. by right; exists (xchoose ex_S). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)