proposition: Lemma prev_neq x p : x \in p -> uniq p -> 1 < size p -> x != prev p x.
proof: Proof. move => x_p uniq_p lt1p. have := @next_neq (prev p x) _ _ uniq_p lt1p. by rewrite mem_prev next_prev // eq_sym; apply. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)