proposition: Lemma notin_num_occ_0 (t : seq A) : (a \notin t) = (N(a | t) == O).
proof: Proof. apply/esym. case/boolP : (a \notin t) => [/count_memPn | ]. rewrite /num_occ; by move=> ->. apply: contraNF; by move/eqP/count_memPn. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2