proposition: Lemma filter_pred1_num_occ (t : seq A) : filter (pred1 a) t = nseq N(a | t) a.
proof: Proof. set lhs := (X in X = _). rewrite (_ : N(a | t) = size lhs); last by rewrite size_filter. apply/all_pred1P/all_filterP; by rewrite filter_id. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2