proposition: Lemma enum_partn_countE sm p : is_part_of_n sm p -> count_mem p (enum_partn sm) = 1.
proof: Proof. rewrite /enum_partn /= => /andP[Hsum Hpart]. rewrite count_cat enum_partnsE /= Hsum Hpart !andbT. case/altP: (size p =P 0) => Hsize. - rewrite count_flatten -map_comp. set empty := map _ _; have {empty} -> : empty = [seq 0 | i <- iota 1 sm]. rewrite {}/empty -eq_in_map => i /=. rewrite mem_iota add1n ltnS => /andP[/lt0n_neq0 Hi _]. apply/count_memPn => /=; move: Hi; apply: contra. move/(allP (enum_partns_allP _ _)) => /= /andP[/eqP <- _]. by rewrite Hsize. suff -> : sumn (map (fun=> 0) _) = 0 by rewrite addn0. by move=> T; elim => [|l0 l /= ->]. - rewrite /= add0n count_flatten -map_comp. rewrite (eq_map (g := fun i => i == size p : nat)); first last. move=> i /=; rewrite enum_partnsE /=. by rewrite Hsum Hpart !andbT eq_sym. by rewrite sumn_pred1_iota add1n ltnS lt0n Hsize /= -(eqP Hsum) size_part. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype