case a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
r : R
N n✝ : ℕ
⊢ coeff (reflect N (↑C r * f)) n✝ = coeff (↑C r * reflect N f) n✝
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
r : R
N : ℕ
⊢ reflect N (↑C r * f) = ↑C r * reflect N f
ext
no goals
case a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
r : R
N n✝ : ℕ
⊢ coeff (reflect N (↑C r * f)) n✝ = coeff (↑C r * reflect N f) n✝
simp only [coeff_reflect, coeff_C_mul]