proposition: Lemma next_rot : next (rot n0 p) =1 next p.
proof: Proof. move=> x; have n_p := cycle_next; rewrite -(rot_cycle n0) in n_p. case p_x: (x \in p); last by rewrite !next_nth mem_rot p_x. by rewrite (eqP (next_cycle n_p _)) ?mem_rot. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)