proposition: Lemma dvdn_card_permuted : \prod_(x : seq_sub w) (count_mem (val x) w)`! %| n`!.
proof: Proof. Proof using. by apply/dvdnP; exists #|[set: permuted w]|; rewrite card_permuted_prod. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles