proposition: Lemma enum_partns_countE sm sz p : is_part_of_ns sm sz p -> count_mem p (enum_partns sm sz) = 1.
proof: Proof. rewrite /enum_partns. case: p => /= [/and3P[/eqP<- /eqP<-] // | p0 p] /and4P[Hsz Hsum Hhead Hpart]. rewrite enum_partnsk_countE //=. - rewrite -(eqP Hsum); apply: (@leq_trans p0); last exact: leq_addr. have /part_head_non0 /= : is_part (p0 :: p) by rewrite /= Hhead Hpart. by rewrite lt0n. - by rewrite Hsz Hsum Hhead Hpart -(eqP Hsum) leq_addr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype