fact: Definition permuted_tuple (t : n.-tuple T) := [seq [tuple tnth t (aperm i p) | i < n] | p : 'S_n ].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles