no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : Field R
p q : R[X]
ha : a ≠ 0
x✝ : p ∣ q
r : R[X]
hr : q = p * r
⊢ q = ↑C a * p * (↑C a⁻¹ * r)
rw [mul_assoc, mul_left_comm p, ← mul_assoc, ← C.map_mul, _root_.mul_inv_cancel ha, C.map_one,
  one_mul, hr]