proposition: Lemma num_co_occ_num_occ {A B : finType} : forall n (ta : n.-tuple A) (tb : n.-tuple B) a, \sum_(b in B) N(a, b | ta, tb) = N(a | ta).
proof: Proof. elim => [ta tb a | n IH ta tb a]. rewrite (tuple0 ta) (tuple0 tb) /= (eq_bigr (fun=> 0)) //. by rewrite big_const iter_addn !Monoid.simpm. move: {IH}(IH (tbehead ta) (tbehead tb) a) => IH. rewrite [in X in _ = X]/num_occ /= in IH. rewrite (tuple_eta ta) (tuple_eta tb) /= [in RHS]/num_occ. rewrite (eq_bigr (fun b => N(a, b | [:: thead ta], [:: thead tb]) + N(a, b | tbehead ta, tbehead tb))). by rewrite big_split /= IH num_co_occ_num_occ1. move=> b' _; by rewrite /num_co_occ num_occ_thead. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2