no goals
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r✝ p : R[X]
n d : ℕ
r : R
⊢ coeff (↑(monomial n) r * p) (d + n) = r * coeff p d
rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]