def Lean.Grind.CommRing.Expr.denoteS {α : Type u_1} [Semiring α] (ctx : Context α) : Expr → α

def Lean.Grind.CommRing.Expr.denoteSAsRing {α : Type u_1} [Semiring α] (ctx : Context α) : Expr → Ring.OfSemiring.Q α

theorem Lean.Grind.CommRing.Expr.denoteAsRing_eq {α : Type u_1} [Semiring α] (ctx : Context α) (e : Expr) : denoteSAsRing ctx e = ↑(denoteS ctx e)

def Lean.Grind.CommRing.Expr.toPolyS : Expr → Poly

def Lean.Grind.CommRing.Expr.toPolyS_nc : Expr → Poly

inductive Lean.Grind.CommRing.Poly.NonnegCoeffs : Poly → Prop

• num (c : Int) : c ≥ 0 → (Poly.num c).NonnegCoeffs
• add (a : Int) (m : Mon) (p : Poly) : a ≥ 0 → p.NonnegCoeffs → (Poly.add a m p).NonnegCoeffs

def Lean.Grind.CommRing.denoteSInt {α : Type u_1} [Semiring α] (k : Int) : α

theorem Lean.Grind.CommRing.denoteSInt_eq {α : Type u_1} [Semiring α] (k : Int) : denoteSInt k = ↑k.toNat

def Lean.Grind.CommRing.Poly.denoteS {α : Type u_1} [Semiring α] (ctx : Context α) (p : Poly) : α

theorem Lean.Grind.CommRing.Poly.denoteS_ofMon {α : Type u_1} [Semiring α] (ctx : Context α) (m : Mon) : denoteS ctx (ofMon m) = Mon.denote ctx m

theorem Lean.Grind.CommRing.Poly.denoteS_ofVar {α : Type u_1} [Semiring α] (ctx : Context α) (x : Var) : denoteS ctx (ofVar x) = Var.denote ctx x

theorem Lean.Grind.CommRing.Poly.denoteS_addConst {α : Type u_1} [Semiring α] (ctx : Context α) (p : Poly) (k : Int) : k ≥ 0 → p.NonnegCoeffs → denoteS ctx (p.addConst k) = denoteS ctx p + ↑k.toNat

theorem Lean.Grind.CommRing.Poly.denoteS_insert {α : Type u_1} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) : k ≥ 0 → p.NonnegCoeffs → denoteS ctx (insert k m p) = ↑k.toNat * Mon.denote ctx m + denoteS ctx p

theorem Lean.Grind.CommRing.Poly.denoteS_concat {α : Type u_1} [Semiring α] (ctx : Context α) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteS ctx (p₁.concat p₂) = denoteS ctx p₁ + denoteS ctx p₂

theorem Lean.Grind.CommRing.Poly.denoteS_mulConst {α : Type u_1} [Semiring α] (ctx : Context α) (k : Int) (p : Poly) : k ≥ 0 → p.NonnegCoeffs → denoteS ctx (mulConst k p) = ↑k.toNat * denoteS ctx p

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

theorem Lean.Grind.CommRing.Poly.denoteS_mulMon {α : Type u_1} [CommSemiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) : k ≥ 0 → p.NonnegCoeffs → denoteS ctx (mulMon k m p) = ↑k.toNat * Mon.denote ctx m * denoteS ctx p

theorem Lean.Grind.CommRing.Poly.addConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCoeffs → (p.addConst k).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.insert_Nonneg (k : Int) (m : Mon) (p : Poly) : k ≥ 0 → p.NonnegCoeffs → (insert k m p).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.denoteS_mulMon_nc_go {α : Type u_1} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p acc : Poly) : k ≥ 0 → p.NonnegCoeffs → acc.NonnegCoeffs → denoteS ctx (mulMon_nc.go k m p acc) = ↑k.toNat * Mon.denote ctx m * denoteS ctx p + denoteS ctx acc

theorem Lean.Grind.CommRing.Poly.num_zero_NonnegCoeffs : (num 0).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.denoteS_mulMon_nc {α : Type u_1} [Semiring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly) : k ≥ 0 → p.NonnegCoeffs → denoteS ctx (mulMon_nc k m p) = ↑k.toNat * Mon.denote ctx m * denoteS ctx p

theorem Lean.Grind.CommRing.Poly.mulConst_NonnegCoeffs {p : Poly} {k : Int} : k ≥ 0 → p.NonnegCoeffs → (mulConst k p).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.mulMon_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) : k ≥ 0 → p.NonnegCoeffs → (mulMon k m p).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.mulMon_nc_go_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) {acc : Poly} : k ≥ 0 → p.NonnegCoeffs → acc.NonnegCoeffs → (mulMon_nc.go k m p acc).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.mulMon_nc_NonnegCoeffs {p : Poly} {k : Int} (m : Mon) : k ≥ 0 → p.NonnegCoeffs → (mulMon_nc k m p).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.concat_NonnegCoeffs {p₁ p₂ : Poly} : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.concat p₂).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.combine_NonnegCoeffs {p₁ p₂ : Poly} : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.combine p₂).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.mul_go_NonnegCoeffs (p₁ p₂ acc : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (mul.go p₂ p₁ acc).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.mul_NonnegCoeffs {p₁ p₂ : Poly} : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.mul p₂).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.mul_nc_go_NonnegCoeffs (p₁ p₂ acc : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → (mul_nc.go p₂ p₁ acc).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.mul_nc_NonnegCoeffs {p₁ p₂ : Poly} : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.mul_nc p₂).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.pow_NonnegCoeffs {p : Poly} (k : Nat) : p.NonnegCoeffs → (p.pow k).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.pow_nc_NonnegCoeffs {p : Poly} (k : Nat) : p.NonnegCoeffs → (p.pow_nc k).NonnegCoeffs

theorem Lean.Grind.CommRing.Poly.denoteS_mul_go {α : Type u_1} [CommSemiring α] (ctx : Context α) (p₁ p₂ acc : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → denoteS ctx (mul.go p₂ p₁ acc) = denoteS ctx acc + denoteS ctx p₁ * denoteS ctx p₂

theorem Lean.Grind.CommRing.Poly.denoteS_mul {α : Type u_1} [CommSemiring α] (ctx : Context α) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteS ctx (p₁.mul p₂) = denoteS ctx p₁ * denoteS ctx p₂

theorem Lean.Grind.CommRing.Poly.denoteS_mul_nc_go {α : Type u_1} [Semiring α] (ctx : Context α) (p₁ p₂ acc : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → acc.NonnegCoeffs → denoteS ctx (mul_nc.go p₂ p₁ acc) = denoteS ctx acc + denoteS ctx p₁ * denoteS ctx p₂

theorem Lean.Grind.CommRing.Poly.denoteS_mul_nc {α : Type u_1} [Semiring α] (ctx : Context α) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteS ctx (p₁.mul_nc p₂) = denoteS ctx p₁ * denoteS ctx p₂

theorem Lean.Grind.CommRing.Poly.denoteS_pow {α : Type u_1} [CommSemiring α] (ctx : Context α) (p : Poly) (k : Nat) : p.NonnegCoeffs → denoteS ctx (p.pow k) = denoteS ctx p ^ k

theorem Lean.Grind.CommRing.Poly.denoteS_pow_nc {α : Type u_1} [Semiring α] (ctx : Context α) (p : Poly) (k : Nat) : p.NonnegCoeffs → denoteS ctx (p.pow_nc k) = denoteS ctx p ^ k

theorem Lean.Grind.CommRing.Expr.toPolyS_NonnegCoeffs {e : Expr} : e.toPolyS.NonnegCoeffs

theorem Lean.Grind.CommRing.Expr.toPolyS_nc_NonnegCoeffs {e : Expr} : e.toPolyS_nc.NonnegCoeffs

theorem Lean.Grind.CommRing.Expr.denoteS_toPolyS {α : Type u_1} [CommSemiring α] (ctx : Context α) (e : Expr) : Poly.denoteS ctx e.toPolyS = denoteS ctx e

theorem Lean.Grind.CommRing.Expr.denoteS_toPolyS_nc {α : Type u_1} [Semiring α] (ctx : Context α) (e : Expr) : Poly.denoteS ctx e.toPolyS_nc = denoteS ctx e

def Lean.Grind.CommRing.eq_normS_cert (lhs rhs : Expr) : Bool

theorem Lean.Grind.CommRing.eq_normS {α : Type u_1} [CommSemiring α] (ctx : Context α) (lhs rhs : Expr) : eq_normS_cert lhs rhs = true → Expr.denoteS ctx lhs = Expr.denoteS ctx rhs

def Lean.Grind.CommRing.eq_normS_nc_cert (lhs rhs : Expr) : Bool

theorem Lean.Grind.CommRing.eq_normS_nc {α : Type u_1} [Semiring α] (ctx : Context α) (lhs rhs : Expr) : eq_normS_nc_cert lhs rhs = true → Expr.denoteS ctx lhs = Expr.denoteS ctx rhs

theorem Lean.Grind.Ring.OfSemiring.of_eq {α : Type u_1} [Semiring α] (ctx : CommRing.Context α) (lhs rhs : CommRing.Expr) : CommRing.Expr.denoteS ctx lhs = CommRing.Expr.denoteS ctx rhs → CommRing.Expr.denoteSAsRing ctx lhs = CommRing.Expr.denoteSAsRing ctx rhs

theorem Lean.Grind.Ring.OfSemiring.of_diseq {α : Type u_1} [Semiring α] [AddRightCancel α] (ctx : CommRing.Context α) (lhs rhs : CommRing.Expr) : CommRing.Expr.denoteS ctx lhs ≠ CommRing.Expr.denoteS ctx rhs → CommRing.Expr.denoteSAsRing ctx lhs ≠ CommRing.Expr.denoteSAsRing ctx rhs