case a
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
N n✝ : ℕ
⊢ coeff (reflect N (f + g)) n✝ = coeff (reflect N f + reflect N g) n✝
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
N : ℕ
⊢ reflect N (f + g) = reflect N f + reflect N g
ext
no goals
case a
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
N n✝ : ℕ
⊢ coeff (reflect N (f + g)) n✝ = coeff (reflect N f + reflect N g) n✝
simp only [coeff_add, coeff_reflect]