proposition: Lemma matching_of_dimatching (G : sgraph) (A : {set G}) M : dimatching M -> @matching G (matching_of M).
proof: Proof. move => [M1 M2]. split. - move => e. case/imsetP => x /M1 ? ?. apply/edgesP. by exists x.1; exists x.2. - move => e1 e2 /imsetP [x X1 X2] /imsetP [y Y1 Y2] z. subst e1 e2. move => Z1 Z2. by rewrite (M2 x y X1 Y1 z Z1 Z2). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)