∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) [Lean.Grind.NoNatZeroDivisors α]
  (k : ℤ) (lhs rhs : Lean.Grind.CommRing.Expr) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.imp_keq_cert lhs rhs k p₁ p₂ = true →
    ↑k * Lean.Grind.CommRing.Poly.denote ctx p₁ = Lean.Grind.CommRing.Poly.denote ctx p₂ →
      Lean.Grind.CommRing.Expr.denote ctx lhs = Lean.Grind.CommRing.Expr.denote ctx rhs