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 ∣ ↑C a * q
r : R[X]
hr : ↑C a * q = p * r
⊢ q = p * (↑C a⁻¹ * r)
rw [mul_left_comm p, ← hr, ← mul_assoc, ← C.map_mul, _root_.inv_mul_cancel ha, C.map_one,
  one_mul]