proposition: Lemma connector_dimatching (G : diGraph) (A : {set G} ) n (p : 'I_n -> pathS G) : connector A (~:A) p -> dimatching (dimatching_of p).
proof: Proof. move => con_p. split. + move => e. case/imsetP => i _ -> /=. by case: (connectorC_edge i con_p). + move => [a b] [a' b'] /imsetP [i _ [-> ->]] /imsetP [j _ [-> ->]] /= x /set2P [->|->]. * case/set2P; by [move/(fst_inj con_p) -> | move/(fst_lst_eq con_p) ->]. * case/set2P; by [move/(lst_inj con_p) -> | move/esym/(fst_lst_eq con_p) ->]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)