```module Stdlib.Data.Int.Base;

import Stdlib.Data.Fixity open;

import Stdlib.Data.Nat.Base as Nat;
open Nat using {Nat; zero; suc; sub};

import Stdlib.Data.Bool.Base open;

--- Inductive integers. I.e. whole numbers that can be positive, zero, or negative.
builtin int
type Int :=
| --- ofNat n represents the integer n
ofNat Nat
| --- negSuc n represents the integer -(n + 1)
negSuc Nat;

--- Converts an ;Int; to a ;Nat;. If the ;Int; is negative, it returns ;zero;.
toNat : Int -> Nat
| (ofNat n) := n
| (negSuc _) := zero;

--- Non-negative predicate for ;Int;s.
builtin int-nonneg
nonNeg : Int -> Bool
| (ofNat n) := true
| (negSuc _) := false;

--- Subtraction for ;Nat;s.
builtin int-sub-nat
intSubNat (n m : Nat) : Int :=
case sub n m of {
| zero := ofNat (Nat.sub m n)
| suc k := negSuc k
};

builtin int-plus
+ : Int -> Int -> Int
| (ofNat m) (ofNat n) := ofNat (m Nat.+ n)
| (ofNat m) (negSuc n) := intSubNat m (suc n)
| (negSuc m) (ofNat n) := intSubNat n (suc m)
| (negSuc m) (negSuc n) := negSuc (suc (m Nat.+ n));

--- Negation for ;Nat;s.
builtin int-neg-nat
negNat : Nat -> Int
| zero := ofNat zero
| (suc n) := negSuc n;

--- Negation for ;Int;s.
builtin int-neg
neg : Int -> Int
| (ofNat n) := negNat n
| (negSuc n) := ofNat (suc n);

syntax operator * multiplicative;

--- Multiplication for ;Int;s.
builtin int-mul
* : Int -> Int -> Int
| (ofNat m) (ofNat n) := ofNat (m Nat.* n)
| (ofNat m) (negSuc n) := negNat (m Nat.* suc n)
| (negSuc m) (ofNat n) := negNat (suc m Nat.* n)
| (negSuc m) (negSuc n) := ofNat (suc m Nat.* suc n);

--- Subtraction for ;Int;s.
builtin int-sub
- (n m : Int) : Int := m + neg n;

--- Division for ;Int;s.
builtin int-div
div : Int -> Int -> Int
| (ofNat m) (ofNat n) := ofNat (Nat.div m n)
| (ofNat m) (negSuc n) := negNat (Nat.div m (suc n))
| (negSuc m) (ofNat n) := negNat (Nat.div (suc m) n)
| (negSuc m) (negSuc n) := ofNat (Nat.div (suc m) (suc n));

--- Modulo for ;Int;s.
builtin int-mod
mod : Int -> Int -> Int
| (ofNat m) (ofNat n) := ofNat (Nat.mod m n)
| (ofNat m) (negSuc n) := ofNat (Nat.mod m (suc n))
| (negSuc m) (ofNat n) := negNat (Nat.mod (suc m) n)
| (negSuc m) (negSuc n) := negNat (Nat.mod (suc m) (suc n));

--- Absolute value
abs : Int -> Nat
| (ofNat n) := n
| (negSuc n) := suc n;
```