proposition: Lemma kconnectedP k G : reflect (kconnected k G) (kconnectedb k G).
proof: Proof. apply: (iffP andP) => [[gtk /forall_inP sepG]|[gtk sepG]]; split => //. - move => S /vseparatorP; exact: sepG. - apply/forall_inP => S /vseparatorP; exact: sepG. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)