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