proposition: Lemma fpath_f_finv_in p x : last x p \in S -> fpath f (last x p) (rev (belast x p)) -> fpath finv x p.
proof: Proof. by move=> lS /(conj lS)/andP; rewrite -fpath_finv_in => /andP[]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)