proposition: Lemma num_occ_alt : N(a | t) = #| set_occ |.
proof: Proof. rewrite cardE -sum1_size big_filter /= /num_occ -sum1_count big_tuple. apply/eq_bigl => i; by rewrite !inE. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2