proposition: Lemma sum_num_occ_inc (k l : nat) : k <= l -> sum_num_occ k <= sum_num_occ l.
proof: Proof. move=> kl. have -> : l = k + (l - k) by rewrite subnKC. set m := l - k. elim: m => [|n' IH]. - by rewrite addn0 leqnn. - by rewrite (leq_trans IH _) // addnS sum_num_occ_inc_loc. Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2