proposition: Lemma uniq_pairwise xs : uniq xs = pairwise [rel x y | x != y] xs.
proof: Proof. elim: xs => //= x xs ->; congr andb; rewrite -has_pred1 -all_predC. by elim: xs => //= x' xs ->; case: eqVneq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)