proposition: Lemma ltn_size_undup s : (size (undup s) < size s) = ~~ uniq s.
proof: Proof. by elim: s => //= x s IHs; case s_x: (x \in s); rewrite //= ltnS size_undup. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)