proposition: Lemma fpath_finv_cycle q x : (x \in p) && (fpath finv x q) = (last x q \in p) && fpath f (last x q) (rev (belast x q)).
proof: Proof. exact: fpath_finv_in. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)