proposition: Lemma uniqP s : reflect {in gtn (size s) &, injective (nth s)} (uniq s).
proof: Proof. apply: (iffP idP) => [/nthK/can_in_inj// | nth_inj]. apply/uniqPn => -[i [j [ltij ltjs /nth_inj/eqP/idPn]]]. by rewrite !inE (ltn_trans ltij ltjs) ltn_eqF //=; case. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)