proposition: Lemma sum_num_occ_seq1 : \sum_(i in A) N(i | [:: a]) = 1.
proof: Proof. rewrite (bigID (pred1 a)) /= big_pred1_eq /= eqxx /= addn0. rewrite (_ : \sum_(_ | _) _ = \sum_(a' : A | a' != a) 0). by rewrite sum_nat_const muln0. apply eq_bigr => a'' /negbTE Ha''; by rewrite eq_sym Ha''. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2