proposition: Lemma next_map p : uniq p -> forall x, next (map h p) (h x) = h (next p x).
proof: Proof. move=> Up x; case p_x: (x \in p); last by rewrite !next_nth (mem_map Ih) p_x. case/rot_to: p_x => i p' def_p. rewrite -(next_rot i Up); rewrite -(map_inj_uniq Ih) in Up. rewrite -(next_rot i Up) -map_rot {i p Up}def_p /=. by case: p' => [|y p''] //=; rewrite !eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)