proposition: Lemma card_matching_of (G : diGraph) (M : {set G * G}) : dimatching M -> #|matching_of M| = #|M|.
proof: Proof. move => [? dim_M]. rewrite /matching_of card_in_imset //. move => e1 e2 /= inM1 inM2 E. apply dim_M with e1.1 => //. all: by rewrite -?E !inE eqxx. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)