no goals
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f g : ℕ → R → S
⊢ sum p (f + g) = sum p f + sum p g
simp [sum_def, Finset.sum_add_distrib]