proposition: Lemma fpath_finv_in p x : (x \in S) && (fpath finv x p) = (last x p \in S) && (fpath f (last x p) (rev (belast x p))).
proof: Proof. elim: p x => //= y p IHp x; rewrite rev_cons rcons_path. transitivity [&& y \in S, f y == x & fpath finv y p]. apply/and3P/and3P => -[xS /eqP<- fxp]; split; by rewrite ?f_finv_in ?finv_f_in ?finv_in ?f_in. rewrite andbCA {}IHp !andbA [RHS]andbC -andbA; congr [&& _, _ & _]. by case: p => //= z p; rewrite rev_cons last_rcons. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)