int_abs_add: (all x:Int, y:Int. abs(x + y) ≤ abs(x) + abs(y))

int_abs_div: (all x:Int, y:Int. abs(x / y) = abs(x) / abs(y))

int_abs_eq_iff_eq_or_neg: (all x:Int, y:Int. ((abs(x) = abs(y)) ⇔ ((x = y) or (x = - y))))

int_abs_eq_zero_iff_zero: (all x:Int. ((abs(x) = 0) ⇔ (x = +0)))

int_abs_eq_zero_implies_zero: (all x:Int. (if abs(x) = 0 then x = +0))

int_abs_le_iff: (all x:Int, y:UInt. ((abs(x) ≤ y) ⇔ ((- pos(y) ≤ x) and (x ≤ pos(y)))))

int_abs_mult: (all x:Int, y:Int. abs(x * y) = abs(x) * abs(y))

auto int_abs_negsuc

int_abs_negsuc: (all n:UInt. abs(negsuc(n)) = 1 + n)

auto int_abs_pos

int_abs_pos: (all n:UInt. abs(pos(n)) = n)

int_abs_sub_symm: (all x:Int, y:Int. abs(x - y) = abs(y - x))

auto int_abs_zero

int_abs_zero: abs(+0) = 0

int_le_abs: (all x:Int. x ≤ pos(abs(x)))

int_mult_left_cancel: (all n:Int, x:Int, y:Int. (if (n ≠ +0 and (n * x = n * y)) then x = y))

int_mult_right_cancel: (all n:Int, x:Int, y:Int. (if (n ≠ +0 and (x * n = y * n)) then x = y))

int_mult_to_zero: (all x:Int, y:Int. (if x * y = +0 then ((x = +0) or (y = +0))))

int_neg_abs_le: (all x:Int. - pos(abs(x)) ≤ x)

int_pos_abs_eq_iff_nonneg: (all x:Int. ((pos(abs(x)) = x) ⇔ (+0 ≤ x)))

int_rev_triangle: (all x:Int, y:Int. abs(x) ∸ abs(y) ≤ abs(x - y))

int_rev_triangle_right: (all x:Int, y:Int. abs(y) ∸ abs(x) ≤ abs(x - y))

int_zero_implies_abs_eq_zero: (all x:Int. (if x = +0 then abs(x) = 0))