proposition: Lemma permutationsE s : 0 < size s -> perm_eq (perms s) [seq x :: t | x <- undup s, t <- perms (rem x s)].
proof: Proof. move=> nt_s; apply/uniq_perm=> [||t]; first exact: permutations_uniq. apply/allpairs_uniq_dep=> [|x _|]; rewrite ?undup_uniq ?permutations_uniq //. by case=> [_ _] [x t] _ _ [-> ->]. rewrite mem_permutations; apply/idP/allpairsPdep=> [Dt | [x [t1 []]]]. rewrite -(perm_size Dt) in nt_s; case: t nt_s => // x t _ in Dt *. have s_x: x \in s by rewrite -(perm_mem Dt) mem_head. exists x, t; rewrite mem_undup mem_permutations; split=> //. by rewrite -(perm_cons x) (permPl Dt) perm_to_rem. rewrite mem_undup mem_permutations -(perm_cons x) => s_x Dt1 ->. by rewrite (permPl Dt1) perm_sym perm_to_rem. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)