proposition: Lemma count_mem_mset a A : count_mem a A = A a.
proof: Proof. rewrite unlock count_flatten sumn_map big_map. rewrite (eq_bigr _ (fun _ _ => esym (sum1_count _ _))) /=. rewrite (eq_bigr _ (fun _ _ => big_nseq_cond _ _ _ _ _ _)) /= -big_mkcond /=. have [aNA|aA] := finsuppP. by rewrite big1_fset // => i iA /eqP eq_ia; rewrite -eq_ia iA in aNA. rewrite big_fset_condE/= (big_fsetD1 a) ?inE ?eqxx ?andbT //= iter_addn mul1n. rewrite (_ : (_ `\ _)%fset = fset0) ?big_seq_fset0 ?addn0//. by apply/fsetP=> i; rewrite !inE; case: (i == a); rewrite ?(andbF, andbT). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap