data INTEGER : Type
add : INTEGER -> INTEGER -> INTEGER
mult : INTEGER -> INTEGER -> INTEGER
plusZeroRightNeutral : (m : INTEGER) -> m + Z = m
plusCommutative : (m : INTEGER) -> (n : INTEGER) -> m + n = n + m
castPlus : (m : Nat) -> (n : Nat) -> the INTEGER (cast (m + n)) = cast m + cast n
unfoldPS : (m : Nat) -> PS m = 1 + cast m
unfoldNS : (m : Nat) -> NS m = -1 - cast m
difference : Nat -> Nat -> INTEGER
differenceZeroRight : (n : Nat) -> difference n 0 = cast n
minusSuccSucc : (m : Nat) -> (n : Nat) -> the INTEGER (cast (S m) - cast (S n)) = cast m - cast n
unfoldDifference : (m : Nat) -> (n : Nat) -> difference m n = cast m - cast n
negateInvolutive : (m : INTEGER) -> negate (negate m) = m
negatePlus : (m : INTEGER) -> (n : INTEGER) -> negate (m + n) = negate m + negate n
negateDifference : (m : Nat) -> (n : Nat) -> negate (difference m n) = difference n m
minusZeroRight : (m : INTEGER) -> m - Z = m
plusInverse : (m : INTEGER) -> m - m = Z
plusAssociative : (m : INTEGER) -> (n : INTEGER) -> (p : INTEGER) -> m + (n + p) = (m + n) + p