proposition: Lemma next_iter (T : eqType) (x y : T) (s : seq T) : uniq s -> x \in s -> y \in s -> exists n, iter n (next s) x == y.
proof: Proof. move=> uniq_s x_s y_s; have [i s' rot_i] := rot_to x_s. exists (index y (rot i s)); under eq_iter => z do rewrite -(next_rot i) //. have -> : x = head y (rot i s) by rewrite rot_i. by rewrite iter_next_nth ?nth_index ?index_mem ?mem_rot ?rot_uniq. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)