no goals
K : Type u
inst✝ : CommRing K
P : Sort v
f : K[X] → K[X] → P
H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q
p q p' q' : K[X]
hq : q ≠ 0
hq' : q' ≠ 0
h : q' * p = q * p'
⊢ f (q' * p) (q' * q) = f (q * p') (q * q')
rw [h, mul_comm q']