proposition: Lemma size_permuted_seq s : size (permuted_seq s) = (size s)`!.
proof: Proof. Proof using. by rewrite /permuted_seq size_map size_permuted_tuple. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles