def Lean.Grind.Linarith.Expr.denoteN {α : Type u_1} [NatModule α] (ctx : Context α) : Expr → α

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

• nil : Poly.nil.NonnegCoeffs
• add (a : Int) (x : Var) (p : Poly) : a ≥ 0 → p.NonnegCoeffs → (Poly.add a x p).NonnegCoeffs

def Lean.Grind.Linarith.Poly.denoteN {α : Type u_1} [NatModule α] (ctx : Context α) (p : Poly) : α

theorem Lean.Grind.Linarith.Poly.denoteN_nil {α : Type u_1} [NatModule α] (ctx : Context α) : denoteN ctx nil = 0

theorem Lean.Grind.Linarith.Poly.denoteN_add {α : Type u_1} [NatModule α] (ctx : Context α) (k : Int) (x : Var) (p : Poly) : k ≥ 0 → denoteN ctx (add k x p) = k.toNat • Var.denote ctx x + denoteN ctx p

theorem Lean.Grind.Linarith.instAssociativeHAdd_1 {α : Type u_1} [NatModule α] : Std.Associative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.Linarith.instCommutativeHAdd_1 {α : Type u_1} [NatModule α] : Std.Commutative fun (x1 x2 : α) => x1 + x2

theorem Lean.Grind.Linarith.Poly.denoteN_insert {α : Type u_1} [NatModule α] (ctx : Context α) (k : Int) (x : Var) (p : Poly) : k ≥ 0 → p.NonnegCoeffs → denoteN ctx (insert k x p) = k.toNat • Var.denote ctx x + denoteN ctx p

theorem Lean.Grind.Linarith.Poly.denoteN_append {α : Type u_1} [NatModule α] (ctx : Context α) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteN ctx (p₁.append p₂) = denoteN ctx p₁ + denoteN ctx p₂

theorem Lean.Grind.Linarith.Poly.denoteN_combine {α : Type u_1} [NatModule α] (ctx : Context α) (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → denoteN ctx (p₁.combine p₂) = denoteN ctx p₁ + denoteN ctx p₂

theorem Lean.Grind.Linarith.Poly.denoteN_mul' {α : Type u_1} [NatModule α] (ctx : Context α) (p : Poly) (k : Nat) : p.NonnegCoeffs → denoteN ctx (p.mul' ↑k) = k • denoteN ctx p

theorem Lean.Grind.Linarith.Poly.denoteN_mul {α : Type u_1} [NatModule α] (ctx : Context α) (p : Poly) (k : Nat) : p.NonnegCoeffs → denoteN ctx (p.mul ↑k) = k • denoteN ctx p

def Lean.Grind.Linarith.Expr.toPolyN : Expr → Poly

theorem Lean.Grind.Linarith.Poly.mul'_Nonneg (p : Poly) (k : Nat) : p.NonnegCoeffs → (p.mul' ↑k).NonnegCoeffs

theorem Lean.Grind.Linarith.Poly.mul_Nonneg (p : Poly) (k : Nat) : p.NonnegCoeffs → (p.mul ↑k).NonnegCoeffs

theorem Lean.Grind.Linarith.Poly.append_Nonneg (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.append p₂).NonnegCoeffs

theorem Lean.Grind.Linarith.Poly.combine_Nonneg (p₁ p₂ : Poly) : p₁.NonnegCoeffs → p₂.NonnegCoeffs → (p₁.combine p₂).NonnegCoeffs

theorem Lean.Grind.Linarith.Expr.toPolyN_Nonneg (e : Expr) : e.toPolyN.NonnegCoeffs

theorem Lean.Grind.Linarith.Expr.denoteN_toPolyN {α : Type u_1} [NatModule α] (ctx : Context α) (e : Expr) : Poly.denoteN ctx e.toPolyN = denoteN ctx e

def Lean.Grind.Linarith.eq_normN_cert (lhs rhs : Expr) : Bool

theorem Lean.Grind.Linarith.eq_normN {α : Type u_1} [NatModule α] (ctx : Context α) (lhs rhs : Expr) : eq_normN_cert lhs rhs = true → Expr.denoteN ctx lhs = Expr.denoteN ctx rhs