proposition: Lemma num_co_occ_partial_sum_alt a : \sum_(b : B) N(a , b | ta , tb) = N(a | ta).
proof: Proof. elim: n ta tb => [x' y' | m IHm x1 y1]. rewrite (tuple0 x') (tuple0 y') num_occ0. transitivity (\sum_(y0 : B) 0). by apply eq_bigr => b _. by rewrite big_const iter_addn mul0n addn0. rewrite num_occ_thead. transitivity (\sum_y0 (N(a, y0 | [tuple thead x1], [tuple thead y1]) + N(a, y0 | tbehead x1, tbehead y1))). apply eq_bigr => i _. by rewrite {1}/num_co_occ {1}(tuple_eta x1) {1}(tuple_eta y1) /num_co_occ /num_occ /= addn0. rewrite big_split /=. move: {IHm}(IHm (tbehead x1) (tbehead y1)) => ->. congr (_ + _). rewrite (bigD1 (thead y1)) //= num_co_occ1. set tmp := \sum_(_ | _) _. suff : tmp = 0 by move=> ->; rewrite addn0. rewrite {}/tmp. transitivity (\sum_(H | H != thead y1) 0). apply eq_bigr => b Hb. apply/eqP. rewrite /num_co_occ -notin_num_occ_0. move: Hb; apply contra => Hb. case/tnthP : Hb => i. rewrite (tnth_nth (a, b)) /= (ord1 i) /=. by case => _ ->. by rewrite big_const iter_addn mul0n addn0. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2