def Lean.Meta.Grind.Arith.Cutsat.mkNatVar (e : Expr) : GoalM (Expr × Expr)

Given e, returns (NatCast.natCast e, rfl)

def Lean.Meta.Grind.Arith.Cutsat.natToInt (a : Expr) : GoalM (Expr × Expr)

Given a : Nat, returns (a', h) such that a' : Int, and h : NatCast.natCast a = a'

def Lean.Meta.Grind.Arith.Cutsat.assertNatCast (e : Expr) (x : Var) : GoalM Unit

Given x whose denotation is e, if e is of the form NatCast.natCast a, asserts that it is nonnegative.

def Lean.Meta.Grind.Arith.Cutsat.isNatTerm (e : Expr) : GoalM Bool

def Lean.Meta.Grind.Arith.Cutsat.mkNonnegThm? (e : Expr) : GoalM (Option Expr)

Given e : Int, tries to construct a proof that e ≥ 0

def Lean.Meta.Grind.Arith.Cutsat.assertNonneg (e : Expr) (x : Var) : GoalM Unit

Given x whose denotation is e : Int, tries to assert that e ≥ 0