proposition: Lemma kconnectedW n k G : (k+n).-connected G -> k.-connected G.
proof: Proof. case => lt_kn_G sep_kn; split; first exact: leq_ltn_trans (leq_addr _ _) lt_kn_G. by move=> S /sep_kn; apply/leq_trans/leq_addr. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)