proposition: Lemma prev_rot : prev (rot n0 p) =1 prev p.
proof: Proof. move=> x; have p_p := cycle_prev; rewrite -(rot_cycle n0) in p_p. case p_x: (x \in p); last by rewrite !prev_nth mem_rot p_x. by rewrite (eqP (prev_cycle p_p _)) ?mem_rot. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)