int_add_both_sides_of_less: (all x:Int, y:Int, z:Int. ((x + y < x + z) ⇔ (y < z)))

int_add_both_sides_of_less_equal: (all x:Int, y:Int, z:Int. ((x + y ≤ x + z) ⇔ (y ≤ z)))

int_add_both_sides_of_less_equal_right: (all x:Int, y:Int, z:Int. ((y + x ≤ z + x) ⇔ (y ≤ z)))

int_add_both_sides_of_less_right: (all x:Int, y:Int, z:Int. ((y + x < z + x) ⇔ (y < z)))

int_add_le_left_mono: (all x:Int, y:Int, z:Int. (if y ≤ z then x + y ≤ x + z))

int_add_le_right_mono: (all x:Int, y:Int, z:Int. (if y ≤ z then y + x ≤ z + x))

int_add_less_mono_left: (all x:Int, y:Int, z:Int. (if y < z then x + y < x + z))

int_add_less_mono_right: (all x:Int, y:Int, z:Int. (if y < z then y + x < z + x))

int_add_mono_less: (all a:Int, b:Int, c:Int, d:Int. (if ((a < c) and (b < d)) then a + b < c + d))

int_add_mono_less_equal: (all a:Int, b:Int, c:Int, d:Int. (if ((a ≤ c) and (b ≤ d)) then a + b ≤ c + d))

int_dichotomy: (all x:Int, y:Int. ((x ≤ y) or (y < x)))

int_greater_implies_not_equal: (all x:Int, y:Int. (if x > y then x ≠ y))

int_le_iff_diff_nonneg: (all a:Int, b:Int. ((a ≤ b) ⇔ (+0 ≤ b - a)))

int_less_equal_antisymmetric: (all x:Int, y:Int. (if ((x ≤ y) and (y ≤ x)) then x = y))

int_less_equal_iff_less_or_equal: (all x:Int, y:Int. ((x ≤ y) ⇔ ((x < y) or (x = y))))

int_less_equal_iff_not_greater: (all x:Int, y:Int. ((x ≤ y) ⇔ (not (y < x))))

int_less_equal_implies_less_or_equal: (all x:Int, y:Int. (if x ≤ y then ((x < y) or (x = y))))

int_less_equal_refl: (all n:Int. n ≤ n)

int_less_equal_trans: (all m:Int, n:Int, o:Int. (if ((m ≤ n) and (n ≤ o)) then m ≤ o))

int_less_implies_less_equal: (all x:Int, y:Int. (if x < y then x ≤ y))

int_less_implies_not_equal: (all x:Int, y:Int. (if x < y then x ≠ y))

int_less_implies_not_greater: (all x:Int, y:Int. (if x < y then not (y < x)))

int_less_irreflexive: (all x:Int. not (x < x))

int_less_or_equal_implies_less_equal: (all x:Int, y:Int. (if ((x < y) or (x = y)) then x ≤ y))

int_less_trans: (all x:Int, y:Int, z:Int. (if ((x < y) and (y < z)) then x < z))

int_less_trans_less_equal_left: (all x:Int, y:Int, z:Int. (if ((x ≤ y) and (y < z)) then x < z))

int_less_trans_less_equal_right: (all x:Int, y:Int, z:Int. (if ((x < y) and (y ≤ z)) then x < z))

int_max_assoc: (all x:Int, y:Int, z:Int. max(max(x, y), z) = max(x, max(y, z)))

int_max_equal_greater_left: (all x:Int, y:Int. (if y ≤ x then max(x, y) = x))

int_max_equal_greater_right: (all x:Int, y:Int. (if x ≤ y then max(x, y) = y))

int_max_greater_left: (all x:Int, y:Int. x ≤ max(x, y))

int_max_greater_right: (all x:Int, y:Int. y ≤ max(x, y))

int_max_idempotent: (all x:Int. max(x, x) = x)

int_max_is_left_or_right: (all x:Int, y:Int. ((max(x, y) = x) or (max(x, y) = y)))

int_max_less_equal: (all x:Int, y:Int, z:Int. (if ((x ≤ z) and (y ≤ z)) then max(x, y) ≤ z))

int_max_min_absorb_left: (all x:Int, y:Int. max(x, min(x, y)) = x)

int_max_min_absorb_right: (all x:Int, y:Int. max(min(x, y), x) = x)

int_max_symmetric: (all x:Int, y:Int. max(x, y) = max(y, x))

int_min_assoc: (all x:Int, y:Int, z:Int. min(min(x, y), z) = min(x, min(y, z)))

int_min_equal_less_left: (all x:Int, y:Int. (if x ≤ y then min(x, y) = x))

int_min_equal_less_right: (all x:Int, y:Int. (if y ≤ x then min(x, y) = y))

int_min_greatest_less_equal: (all x:Int, y:Int, z:Int. (if ((z ≤ x) and (z ≤ y)) then z ≤ min(x, y)))

int_min_idempotent: (all x:Int. min(x, x) = x)

int_min_is_left_or_right: (all x:Int, y:Int. ((min(x, y) = x) or (min(x, y) = y)))

int_min_less_equal_left: (all x:Int, y:Int. min(x, y) ≤ x)

int_min_less_equal_right: (all x:Int, y:Int. min(x, y) ≤ y)

int_min_max_absorb_left: (all x:Int, y:Int. min(x, max(x, y)) = x)

int_min_max_absorb_right: (all x:Int, y:Int. min(max(x, y), x) = x)

int_min_symmetric: (all x:Int, y:Int. min(x, y) = min(y, x))

int_neg_le_iff: (all x:Int, y:Int. ((x ≤ y) ⇔ (- y ≤ - x)))

int_neg_le_mono: (all x:Int, y:Int. (if x ≤ y then - y ≤ - x))

int_neg_less_iff: (all x:Int, y:Int. ((x < y) ⇔ (- y < - x)))

int_neg_less_mono: (all x:Int, y:Int. (if x < y then - y < - x))

auto int_negsuc_le_negsuc

int_negsuc_le_negsuc: (all au:UInt, bu:UInt. (negsuc(au) ≤ negsuc(bu)) = (bu ≤ au))

auto int_negsuc_le_pos

int_negsuc_le_pos: (all au:UInt, bu:UInt. (negsuc(au) ≤ pos(bu)) = true)

auto int_negsuc_less_negsuc

int_negsuc_less_negsuc: (all au:UInt, bu:UInt. (negsuc(au) < negsuc(bu)) = (bu < au))

auto int_negsuc_less_pos

int_negsuc_less_pos: (all au:UInt, bu:UInt. (negsuc(au) < pos(bu)) = true)

int_not_less_equal_iff_greater: (all x:Int, y:Int. ((not (x ≤ y)) ⇔ (y < x)))

int_not_less_implies_less_equal: (all x:Int, y:Int. (if not (x < y) then y ≤ x))

auto int_pos_le_negsuc

int_pos_le_negsuc: (all au:UInt, bu:UInt. (pos(au) ≤ negsuc(bu)) = false)

auto int_pos_le_pos

int_pos_le_pos: (all au:UInt, bu:UInt. (pos(au) ≤ pos(bu)) = (au ≤ bu))

auto int_pos_less_negsuc

int_pos_less_negsuc: (all au:UInt, bu:UInt. (pos(au) < negsuc(bu)) = false)

auto int_pos_less_pos

int_pos_less_pos: (all au:UInt, bu:UInt. (pos(au) < pos(bu)) = (au < bu))

int_trichotomy: (all x:Int, y:Int. ((x < y) or (x = y) or (y < x)))