proposition: Lemma next_neq x p : x \in p -> uniq p -> 1 < size p -> x != next p x.
proof: Proof. move => x_p; have [i p' rot_p uniq_p] := rot_to x_p. move: (uniq_p); rewrite -(next_rot i) // -(size_rot i) -(rot_uniq i) {}rot_p. case: p' => //= y p'. rewrite inE eqxx. by case: (x == y). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)