∀ {K : Type u_1} [inst : CommRing K] {x x_1 : Polynomial K} {q q' : ↥(nonZeroDivisors (Polynomial K))}
  (motive : (∃ c, ↑c * (↑(x_1, q').2 * (x, q).1) = ↑c * (↑(x, q).2 * (x_1, q').1)) → Prop)
  (x_2 : ∃ c, ↑c * (↑(x_1, q').2 * (x, q).1) = ↑c * (↑(x, q).2 * (x_1, q').1)),
  (∀ (val : Polynomial K) (property : val ∈ nonZeroDivisors (Polynomial K))
      (mul_eq : ↑⟨val, property⟩ * (↑(x_1, q').2 * (x, q).1) = ↑⟨val, property⟩ * (↑(x, q).2 * (x_1, q').1)),
      motive ⋯) →
    motive x_2