[PostScript]
```Integer (Int): trait
% The usual (unbounded) integers operators
includes
DecimalLiterals (Int for N),
TotalOrder (Int)
introduces
0, 1: -> Int
succ, pred, -__, abs: Int -> Int
__+__, __-__, __*__: Int, Int -> Int
div, mod, min, max: Int, Int -> Int
asserts
Int generated by 0, succ, pred
forall x, y: Int
succ(pred(x)) == x;
pred(succ(x)) == x;
-0 == 0;
-succ(x) == pred(-x);
-pred(x) == succ(-x);
abs(x) == max(-x, x);
x + 0 == x;
x + succ(y) == succ(x + y);
x + pred(y) == pred(x + y);
x - y == x + (-y);
x * 0 == 0;
x*succ(y) == (x*y) + x;
x*pred(y) == (x*y) - x;
y > 0 => mod(x, y) + (div(x, y) * y) = x;
y > 0 => mod(x, y) >= 0;
y > 0 => mod(x, y) < y;
min(x, y) == if x <= y then x else y;
max(x, y) == if x <= y then y else x;
x < succ(x)
implies
AC (+, Int),
AC (*, Int),
AC (min, Int),
AC (max, Int),
RingWithUnit (Int for T)
Int generated by 1, +, -__:Int->Int
forall x, y: Int
x < y == succ(x) < succ(y);
x <= y == x < succ(y)
converts
1, -__:Int->Int, __-__:Int,Int->Int,
abs, +, *, div, mod, min, max, <=, >=, <, >
```