fact: Definition dimatching (G : diGraph) (M : {set G * G}) := (forall e, e \in M -> e.1 -- e.2) /\ {in M &, forall e1 e2 x, x \in [set e1.1;e1.2] -> x \in [set e2.1 ; e2.2] -> e1 = e2}.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)