proposition: Lemma prev_iter (T : eqType) (x y : T) (s : seq T) : uniq s -> x \in s -> y \in s -> exists n, iter n (prev s) x == y.
proof: Proof. move=> uniq_s x_s y_s; have [n /eqP eq_x] := next_iter uniq_s y_s x_s. by exists n; rewrite -eq_x iterK //; apply: prev_next. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)