proposition: Lemma iter_next_rot x0 s n : n < size s -> uniq s -> iter n (next s) (head x0 s) = head x0 (rot n s).
proof: Proof. elim: n s => [|n IHn] s; first by move => *; rewrite rot0. case: s => [_ /= |x s]; first by rewrite (@eq_iter _ _ id) ?iter_id. move => n_lt_s uniq_s. rewrite iterSr rotS 1?ltnW // rot_rot rot1_cons. rewrite (next_cons x0). under eq_iter => z do rewrite -(next_rot 1) ?rot1_cons //. by rewrite IHn // ?size_rcons ?rcons_uniq // ltnW. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)