proposition: Lemma num_co_occ_sym : N(a, b | ta, tb) = N(b, a | tb, ta).
proof: Proof. rewrite /num_co_occ /num_occ. rewrite (_ : zip tb ta = map (fun x => (x.2, x.1)) (zip ta tb)); last by apply zip_swap. rewrite -2!size_filter filter_map size_map. congr (size _). apply eq_filter; case=> a' b' /=. by rewrite 2!xpair_eqE andbC. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2