proposition: Lemma min_vcover_matching (G : sgraph) (A V : {set G}) : bipartition A -> smallest vcover V -> exists2 M, @matching G M & #|V| = #|M|.
proof: Proof. move => bip_A [cover_V min_V]. have sep_A S : separator G A (~:A) S -> #|V| <= #|S|. { move/bip_separation_vcover => /(_ bip_A). exact: min_V. } case: (Menger sep_A) => p conn_p. move/connector_dimatching : (conn_p) => dim_M. exists (matching_of (dimatching_of p)). exact: matching_of_dimatching. by rewrite card_matching_of // (card_dimatching_of conn_p). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)