proposition: Lemma uniqPn s : reflect (exists i j, [/\ i < j, j < size s & nth s i = nth s j]) (~~ uniq s).
proof: Proof. apply: (iffP idP) => [|[i [j [ltij ltjs]]]]; last first. by apply: contra_eqN => Us; rewrite nth_uniq ?ltn_eqF // (ltn_trans ltij). elim: s => // x s IHs /nandP[/negbNE | /IHs[i [j]]]; last by exists i.+1, j.+1. by exists 0, (index x s).+1; rewrite !ltnS index_mem /= nth_index. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)