import UInt

import Base

import IntDefs

abs_neg: (all n:Int. abs(- n) = abs(n))

neg_zero: - +0 = +0

neg_involutive: (all n:Int. - (- n) = n)

int_zero_add: (all n:Int. +0 + n = n)

int_add_zero: (all n:Int. n + +0 = n)

int_add_commute: (all x:Int, y:Int. x + y = y + x)

suc_uint_monuso: (all x:UInt, y:UInt. (1 + x) ⊝ (1 + y) = x ⊝ y)

add_commute_uint_int: (all x:UInt, y:Int. x + y = y + x)

int_add_assoc: (all x:Int, y:Int, z:Int. (x + y) + z = x + (y + z))

int_add_inverse: (all x:Int. x + - x = +0)

neg_distr_add: (all x:Int, y:Int. - (x + y) = - x + - y)

int_sub_cancel: (all x:Int. x - x = +0)