proposition: Lemma nth_uniq s i j : i < size s -> j < size s -> uniq s -> (nth s i == nth s j) = (i == j).
proof: Proof. by move=> lti ltj /nthK/can_in_eq->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)