no goals
R✝ : Type ?u.380823
M : Type ?u.380826
R : Type u_1
inst✝¹ : CommMonoid M
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ i in range (n + 2), ↑(Nat.choose (n + 1) i) * f i (n + 1 - i) =
    ∑ i in range (n + 1), ↑(Nat.choose n i) * f i (n + 1 - i) +
      ∑ i in range (n + 1), ↑(Nat.choose n i) * f (i + 1) (n - i)
simpa only [nsmul_eq_mul] using sum_choose_succ_nsmul f n