fact: Fixpoint enum_codesz n := if n is n'.+1 then flatten [seq [seq rcons c i | c <- enum_codesz n'] | i <- iota 0 n] else [:: [::]].
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr