∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ : Lean.Grind.CommRing.Poly),
  p₁.NonnegCoeffs →
    p₂.NonnegCoeffs →
      Lean.Grind.CommRing.Poly.denoteS ctx (p₁.combine p₂) =
        Lean.Grind.CommRing.Poly.denoteS ctx p₁ + Lean.Grind.CommRing.Poly.denoteS ctx p₂