def Int.Linear.Poly.gcdAll : Poly → Nat

def Int.Linear.Poly.gcdCoeffs' : Poly → Nat

def Lean.Meta.Simp.Arith.Int.simpEq? (e : Expr) : MetaM (Option (Expr × Expr))

def Lean.Meta.Simp.Arith.Int.simpLe? (e : Expr) (checkIfModified : Bool) : MetaM (Option (Expr × Expr))

def Lean.Meta.Simp.Arith.Int.simpRel? (e : Expr) : MetaM (Option (Expr × Expr))

def Lean.Meta.Simp.Arith.Int.simpDvd? (e : Expr) : MetaM (Option (Expr × Expr))

def Lean.Meta.Simp.Arith.Int.simpExpr? (lhs : Expr) : MetaM (Option (Expr × Expr))