∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoidWithOne M] [inst_1 : AddCommGroup G] (f : M → G) (n : ℕ) {R : ℕ},
  1 ≤ R →
    (fwdDiff 1)^[n + R] f 0 =
      -∑ j ∈ Finset.range (R - 1), R.choose (j + 1) • (fwdDiff 1)^[n + (j + 1)] f 0 +
        ∑ k ∈ Finset.range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)