proposition: Lemma num_occ_map_filter (B : finType) (f : B -> A) (s : {set B}) (p : pred A) (pa : p a) : N(a | [seq f i | i <- enum s & p (f i)]) = N(a | [seq f i | i in s]).
proof: Proof. rewrite /num_occ count_map count_filter /= count_map. apply eq_count => /= m0 /=; by rewrite andb_idr // => /eqP ->. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2