proposition: Lemma num_co_occ_alt : N(a, b | ta, tb) = #| set_co_occ |.
proof: Proof. rewrite /num_co_occ num_occ_alt /set_occ. apply eq_card => i. rewrite !in_set /zip_tuple (tnth_nth (a, b)) nth_zip ?size_tuple //. by rewrite -2!tnth_nth xpair_eqE. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2