{K : Type u} →
  [inst : CommRing K] →
    {P : Sort v} →
      RatFunc K →
        (f : Polynomial K → Polynomial K → P) →
          (∀ {p q p' q' : Polynomial K},
              q ∈ nonZeroDivisors (Polynomial K) →
                q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q') →
            P