proposition: Lemma sum_num_occ_leq_n (k : nat) : sum_num_occ k <= n.
proof: Proof. case/boolP : (k < #|A|) => Hcase. - rewrite -(@full_sum_num_occ_n #|A| _); last by apply leqnn. apply ltnW in Hcase. by apply sum_num_occ_inc. - rewrite -leqNgt in Hcase. by rewrite full_sum_num_occ_n. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2