proposition: Lemma connectP x y : reflect (exists2 p, path e x p & y = last x p) (connect x y).
proof: Proof. apply: (equivP (dfsP _ x y)). by split=> [] [p e_p ->]; exists p => //; rewrite (eq_path rgraphK) in e_p *. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)