proposition: Lemma permutations_uniq s : uniq (permutations s).
proof: Proof. have{s} [n [bs [-> Dn _ Ubs]]] := permsP s. elim: n => //= n IHn in bs Dn Ubs *; rewrite -[bs]cats0 /unzip1 in Dn Ubs. elim: bs [::] => [|[x [|m]] bs IHbs] //= bs2 in Dn Ubs *. by case/andP: Ubs => _ /IHbs->. rewrite /= cons_permsE cat_uniq has_sym andbCA andbC. rewrite {}IHbs; first 1 last; first by rewrite (perm_size (perm_tseq bsCA)). by rewrite (perm_uniq (perm_map _ bsCA)). rewrite (map_inj_uniq (rcons_injl x)) {}IHn {Dn}//=. have: x \notin unzip1 bs by apply: contraL Ubs; rewrite map_cat mem_cat => ->. move: {bs2 m Ubs}(perms_rec n _ _ _) (_ :: bs2) => ts. elim: bs => [|[y [|m]] bs IHbs] //= /[1!inE] bs2 /norP[x'y /IHbs//]. rewrite cons_permsE has_cat negb_or has_map => ->. by apply/hasPn=> t _; apply: contra x'y => /mapP[t1 _ /rcons_inj[_ ->]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)