proposition: Lemma fpath_f_finv_cycle q x : last x q \in p -> fpath f (last x q) (rev (belast x q)) -> fpath finv x q.
proof: Proof. exact: fpath_f_finv_in. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)