proposition: Lemma num_co_occ_num_occ1 {A B : finType} a' b' (a : A) : \sum_(i in B) N(a, i | [tuple of [:: a']], [tuple of [:: b']]) = (a' == a).
proof: Proof. case/boolP : (a' == a) => [/eqP ->{a'} | a'a]. - rewrite /num_co_occ /num_occ /= (bigD1 b') //= eqxx /= addn0 add1n; congr S. rewrite (eq_bigr (fun=> 0)). by rewrite big_const iter_addn. move=> b bb'; by rewrite xpair_eqE eqxx /= addn0 eq_sym (negbTE bb'). - rewrite (eq_bigr (fun=> 0)). by rewrite big_const iter_addn. move=> b _; by rewrite /num_co_occ /num_occ /= xpair_eqE (negbTE a'a). Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2