proposition: Lemma size_permuted_tuple (t : n.-tuple T) : size (permuted_tuple t) = n`!.
proof: Proof. Proof using. rewrite /permuted_tuple size_map -cardE; exact: card_Sn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles