proposition: Lemma enum_codesz_countE n c : is_code_of_size n c -> count_mem c (enum_codesz n) = 1.
proof: Proof. elim: n c => [/= | n IHn] c /andP[]. by move=> _ /nilP ->; rewrite eq_refl addn0. case/lastP: c => [// | c cn] Hcode. rewrite size_rcons eqSS => /eqP Hsz. have {}/IHn Hcount : is_code_of_size n c. rewrite /is_code_of_size Hsz eq_refl andbT. exact: (is_code_rconsK Hcode). rewrite count_flatten -map_comp -/enum_codesz. rewrite (eq_map (g := fun i => i == cn : nat)); first last. move=> i /=; rewrite count_map /=. case (i =P cn) => [Heq | /eqP/negbTE Hneq]. + subst i; rewrite (eq_count (a2 := xpred1 c)); first exact: Hcount. by move=> s /=; apply/idP/idP => [/eqP/rconsK ->| /eqP ->]. + rewrite (eq_count (a2 := pred0)); first by rewrite count_pred0. move=> s /=; apply/negP=> /eqP/(congr1 rev). by rewrite !rev_rcons => [] [/eqP]; rewrite Hneq. rewrite sumn_pred1_iota //= add0n. move/is_codeP: Hcode; rewrite size_rcons ltnS => /(_ _ (ltnSn _)). by rewrite nth_rcons ltnn eq_refl Hsz => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr