proposition: Lemma permutations_all_uniq s : uniq s -> all uniq (permutations s).
proof: Proof. by move=> Us; apply/allP=> t; rewrite mem_permutations => /perm_uniq->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)