no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff (↑(expand R p) f) (n * p) = coeff f n
rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp]