∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (k₁ k : ℤ) (init p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.d_stepk_certC k₁ p₁ k₂ m₂ p₂ p c = true →
    ↑k * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p₁ →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 →
        ↑(k₁ * k) * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p