proposition: Lemma all_permuted (s : n.-tuple T) : all (fun x : n.-tuple T => perm_eq s x) (permuted_tuple s).
proof: Proof. Proof using. apply/allP => t /mapP[/= perm _ ->{t}]. by rewrite perm_sym; apply/tuple_permP; exists perm. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles