proposition: Lemma bip_separation_vcover (G : sgraph) (A S : {set G}) : bipartition A -> separator G A (~: A) S -> vcover S.
proof: Proof. move => bip_A sep_S. apply/vcoverP => x y xy. wlog/andP [xA yNA] : x y xy / (x \in A) && (y \notin A). { move: (bip_A x y xy). case: (boolP (y \in A)) => /= yA xA; last by apply. rewrite or_comm. apply; by rewrite 1?sgP ?xA ?yA. } move: (sep_S _ _ (edgep xy)). rewrite xA inE yNA. case => // s sS. rewrite mem_edgep => /orP [/eqP<-|/eqP<-]; by tauto. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)