proposition: Lemma dfsP x y : reflect (exists2 p, path (grel g) x p & y = last x p) (y \in dfs #|T| [::] x).
proof: Proof. apply: (iffP (dfs_pathP _ _ _)); rewrite ?card0 // => [] [p]; exists p => //. by rewrite disjoint_sym disjoint0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)