proposition: Lemma pairwise_uniq xs : irreflexive r -> pairwise r xs -> uniq xs.
proof: Proof. move=> r_irr; rewrite uniq_pairwise; apply/sub_pairwise => x y. by apply: contraTneq => ->; rewrite r_irr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)