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

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_both_sides_of_equal: (all x:Int, y:Int, z:Int. (if x + y = x + z then y = z))

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

int_add_both_sides_of_equal_right: (all x:Int, y:Int, z:Int. (if y + x = z + x then y = z))

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

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

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

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

auto int_add_zero

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

int_neg_injective: (all x:Int, y:Int. (if - x = - y then x = y))

int_negsuc_eq_pos_false: (all x:UInt, y:UInt. not (negsuc(x) = pos(y)))

int_negsuc_injective: (all x:UInt, y:UInt. (if negsuc(x) = negsuc(y) then x = y))

int_pos_eq_negsuc_false: (all x:UInt, y:UInt. not (pos(x) = negsuc(y)))

int_pos_injective: (all x:UInt, y:UInt. (if pos(x) = pos(y) then x = y))

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

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

auto int_zero_add

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

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

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

neg_zero: - +0 = +0

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