proposition: Lemma prevE x : x \in p -> prev p x = finv x.
proof: Proof. move=> x_p; have /eqP/(congr1 finv) := prev_cycle f_p x_p. by rewrite finv_f_cycle// mem_prev. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)