proposition: Lemma sum_num_occ_size (A : finType) s : (\sum_(a in A) N(a|s))%nat = size s.
proof: Proof. elim: s => [|a s IH] /=. + by apply big1_eq. + by rewrite big_split /= IH -big_mkcond /= (big_pred1 a) // => x; rewrite eq_sym. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2