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 (p * ↑(monomial n) r) (d + n) = coeff p d * r
rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]