proposition: Lemma num_co_occ1 (a' : A) : N(a, b | [:: a'], [:: b]) = N(a | [:: a']).
proof: Proof. by rewrite /num_co_occ /num_occ /= !addn0 xpair_eqE eqxx andbC. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2