proposition: Lemma matching_cover_map (x0 : G) M : matching M -> vcover -> exists2 f : {set G} -> G, (forall e : {set G}, e \in M -> f e \in V :&: e) & {in M&, injective f}.
proof: Proof. move => [M1 M2] cover_V. pose f (A : {set G}) := if [pick x | x \in V :&: A] is Some x then x else x0. have fP e : e \in M -> f e \in V :&: e. { move/M1. case/edgesP => x [y] [E xy]. rewrite /f. case: pickP => [//|]. case/(vcoverP cover_V) : xy => xV; [move/(_ x)|move/(_ y)]; by rewrite E !inE xV eqxx ?orbT. } exists f => // e1 e2 eM1 eM2. move: (eM1) (eM2) => /fP /setIP [V1 E1] /fP /setIP [V2 E2] E. apply M2 with (f e1) => //. by rewrite E. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)