proposition: Lemma uniq_vect_n_k n k : uniq (vect_n_k n k).
proof: Proof. apply: count_mem_uniq => s. case H : (s \in vect_n_k n k); first by rewrite (count_mem_vect_n_k_eq_1 H). by move: H => /count_memPn ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype seq) tools