proposition: Proposition min_max_cover (M : {set {set G}}) : vcover -> matching M -> #|M| = #|V| -> V \subset cover M.
proof: Proof. move => cov_V match_V MV. wlog [x0] : / inhabited G. { move => W. case: (set_0Vmem V) => [-> //|[x _]]; first by rewrite sub0set. exact: W. } case: (matching_cover_map x0 match_V cov_V) => f F1 F2. pose f' (e : { e | e \in M}) := f (val e). have inj_f' : injective f'. { case => e1 M1. case => e2 M2. rewrite /f' /= => E. apply/eqP. change (e1 == e2). by rewrite (F2 _ _ M1 M2 E). } move: (inj_card_onto_pred (P := (mem V)) inj_f') => /=. case/(_ _ _)/Wrap. - case => e inM. by case/setIP : (F1 _ inM). - by rewrite card_sig. - move => X. apply/subsetP => v vV. case/mapP : (X _ vV) => /= [[e inM] _ E]. apply/bigcupP. exists e => //. rewrite E /f' /=. by case/setIP : (F1 _ inM). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)