proposition: Lemma min_sum_num_occ (k : nat) : minn (sum_num_occ k) (sum_num_occ k.+1) = sum_num_occ k.
proof: Proof. apply/minn_idPl; by apply sum_num_occ_inc. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2