proposition: Lemma prods_codesz_bij : bijective prods_codesz.
proof: Proof. Proof using. apply inj_card_bij => [/= c1 c2 Heq|]; last by rewrite card_codesz card_Sn. suff {c1 c2 Heq} /image_injP Hinj : #|image prods_codesz {:codesz n}| == #|{:codesz n}| by exact: (Hinj c1 c2). rewrite card_codesz (eq_card (B := 'S_n)) ?card_Sn // => /= s. rewrite !inE; apply/mapP. have Hcode : is_code_of_size n (cocode s). by rewrite /is_code_of_size cocodeP size_cocode /=. exists (CodeSZ Hcode); first by rewrite enumT. by rewrite /prods_codesz /= -cocodeE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr