proposition: Lemma kconnected_induced (G : sgraph) (A : {set G}) k : (k + #|~: A|).-connected G -> k.-connected (induced A).
proof: Proof. move => [cardG sepG]; split => [|S]. - by rewrite card_sig -(leq_add2r #|~: A|) cardsC addSn. - move/induced_vseparator/sepG. rewrite cardsU card_imset //. rewrite [#|_ :&: _|]eq_card0 ?subn0 ?leq_add2r // => z. by apply: contraTF isT => /setIP [/imsetP[x _ ->]]; rewrite inE (valP x). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)