∀ {R : Type u_1} [inst : Ring R] {r s : R} (k : ℕ),
  Commute r s →
    (descPochhammer ℤ k).smeval (r + s) =
      ∑ ij ∈ Finset.antidiagonal k,
        ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)