proposition: Lemma sum_num_occ_inc_loc (k : nat) : sum_num_occ k <= sum_num_occ k.+1.
proof: Proof. case/boolP : (k < #|A|) => Hcase. - move: (sum_num_occ_rec (Ordinal Hcase)) => /= ->; by apply leq_addr. - rewrite -leqNgt in Hcase. rewrite !full_sum_num_occ //; by apply (leq_trans Hcase). Qed.
imports: mathcomp(all_ssreflect fingroup perm zmodp ssralg) ssr_ext f2