∀ {ι : Type u_1} [inst : Fintype ι] (k : ℕ),
  (↑(k + 1) + 1 - -↑(k + 1)).toNat ^ Finset.univ.card - (↑k + 1 - -↑k).toNat ^ Finset.univ.card ≤
    2 * Fintype.card ι * (2 * k + 3) ^ (Fintype.card ι - 1)