∀ (c : ℕ) (motive : (_ : Lean.Grind.CommRing.Poly) ×' Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k₁ k₂ : ℤ),
      motive ⟨Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂⟩
        (Lean.Grind.CommRing.Poly.num ((k₁ + k₂) % ↑c))) →
    (∀ (k₁ k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly),
        motive ⟨Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂⟩
          ((Lean.Grind.CommRing.Poly.add k₂ m₂ p₂).addConstC k₁ c)) →
      (∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ),
          motive ⟨Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂⟩
            ((Lean.Grind.CommRing.Poly.add k₁ m₁ p₁).addConstC k₂ c)) →
        (∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ)
            (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly),
            m₁.grevlex m₂ = Ordering.eq →
              have k := (k₁ + k₂) % ↑c;
              (k == 0) = true →
                motive ⟨p₁, p₂⟩ (Lean.Grind.CommRing.Poly.combineC._unary c ⟨p₁, p₂⟩) →
                  motive ⟨Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂⟩
                    (Lean.Grind.CommRing.Poly.combineC._unary c ⟨p₁, p₂⟩)) →
          (∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ)
              (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly),
              m₁.grevlex m₂ = Ordering.eq →
                have k := (k₁ + k₂) % ↑c;
                (k == 0) = false →
                  motive ⟨p₁, p₂⟩ (Lean.Grind.CommRing.Poly.combineC._unary c ⟨p₁, p₂⟩) →
                    motive ⟨Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂⟩
                      (Lean.Grind.CommRing.Poly.add k m₁ (Lean.Grind.CommRing.Poly.combineC._unary c ⟨p₁, p₂⟩))) →
            (∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ)
                (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly),
                m₁.grevlex m₂ = Ordering.gt →
                  motive ⟨p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂⟩
                      (Lean.Grind.CommRing.Poly.combineC._unary c ⟨p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂⟩) →
                    motive ⟨Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂⟩
                      (Lean.Grind.CommRing.Poly.add k₁ m₁
                        (Lean.Grind.CommRing.Poly.combineC._unary c ⟨p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂⟩))) →
              (∀ (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ)
                  (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly),
                  m₁.grevlex m₂ = Ordering.lt →
                    motive ⟨Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, p₂⟩
                        (Lean.Grind.CommRing.Poly.combineC._unary c ⟨Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, p₂⟩) →
                      motive ⟨Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂⟩
                        (Lean.Grind.CommRing.Poly.add k₂ m₂
                          (Lean.Grind.CommRing.Poly.combineC._unary c ⟨Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, p₂⟩))) →
                ∀ (_x : (_ : Lean.Grind.CommRing.Poly) ×' Lean.Grind.CommRing.Poly),
                  motive _x (Lean.Grind.CommRing.Poly.combineC._unary c _x)