proposition: Lemma fpath_finv_f_cycle q : {in p, forall x, fpath finv x q -> fpath f (last x q) (rev (belast x q))}.
proof: Proof. exact: fpath_finv_f_in. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)