proposition: Lemma card_codesz n : #|{:codesz n}| = n`!.
proof: Proof. rewrite factE /= cardE -(size_map val) enum_codeszE. elim: n => [//=| n IHn]. rewrite size_flatten -/enum_codesz /shape -map_comp. rewrite (eq_map (g := fun => fact_rec n)); first last. by move=> i /=; rewrite size_map. by rewrite sumnE big_map big_const_seq count_predT size_iota iter_addn_0 mulnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr