proposition: Lemma enum_codeszP n : all (is_code_of_size n) (enum_codesz n).
proof: Proof. rewrite /is_code_of_size; elim: n => [| n IHn] //. apply/allP => cn /flatten_mapP[i]. rewrite -/enum_codesz mem_iota /= add0n ltnS => Hi. move=> /mapP[c /(allP IHn) {IHn}] /andP[Hcode /eqP Hsz ->{cn}]. rewrite size_rcons Hsz eq_refl andbT. by apply is_code_rcons; first by rewrite Hsz. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr