proposition: Lemma num_co_occ_sum : \sum_(a : A) \sum_ (b : B) N( a , b | ta , tb) = n.
proof: Proof. rewrite pair_big /=. rewrite (_ : \sum_p N(p.1, p.2 | ta, tb) = \sum_p N(p | zip_tuple ta tb)). by rewrite sum_num_occ_alt. f_equal. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2