proposition: Lemma separator_min A B S : separator A B S -> #|A :&: B| <= #|S|.
proof: Proof. move/separator_cap. exact: subset_leq_card. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)