proposition: Lemma card_dimatching_of (G : diGraph) A B n (p : 'I_n -> pathS G) : connector A B p -> #|dimatching_of p| = n.
proof: Proof. move => con_p. rewrite /dimatching_of card_imset ?card_ord // => i j. case. by move/(fst_inj con_p). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)