proposition: Lemma cover_matching (M :{set {set G}}) : matching M -> vcover -> #|M| <= #|V|.
proof: Proof. move => [M1 M2] cover_V. wlog [x0] : / inhabited G. { move => W. case: (set_0Vmem M) => [->|[e /M1]]; first by rewrite cards0. case/edgesP => x _. exact: W. } case: (matching_cover_map x0 (conj M1 M2) cover_V) => f F1 F2. have f_V e : e \in M -> f e \in V by move/F1 => /setIP[]. rewrite -(card_in_image F2). apply: subset_leq_card. apply/subsetP => y /mapP [x Hx ->]. apply: f_V. by rewrite mem_enum in Hx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)