proposition: Lemma uniq_next (T : eqType) (p : seq T) : uniq p -> injective (next p).
proof: Proof. Proof using. move=> Huniq x y Heq. by rewrite -(prev_next Huniq x) Heq prev_next. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)