dist_neg_mult: (all x:Int, y:Int. - (x * y) = - x * y)

int_dist_mult_add: (all a:Int, x:Int, y:Int. a * (x + y) = a * x + a * y)

int_dist_mult_add_right: (all a:Int, x:Int, y:Int. (x + y) * a = x * a + y * a)

int_dist_mult_sub: (all a:Int, x:Int, y:Int. a * (x - y) = a * x - a * y)

int_less_iff_diff_pos: (all a:Int, b:Int. ((a < b) ⇔ (+0 < b - a)))

int_mult_assoc: (all x:Int, y:Int, z:Int. (x * y) * z = x * (y * z))

int_mult_commute: (all x:Int, y:Int. x * y = y * x)

auto int_mult_one

int_mult_one: (all x:Int. x * +1 = x)

auto int_mult_zero

int_mult_zero: (all x:Int. x * +0 = +0)

int_neg_mult_left_cancel_le: (all n:Int, x:Int, y:Int. (if ((n < +0) and (n * x ≤ n * y)) then y ≤ x))

int_neg_mult_left_cancel_less: (all n:Int, x:Int, y:Int. (if ((n < +0) and (n * x < n * y)) then y < x))

int_neg_mult_mono_less_left: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x < y)) then n * y < n * x))

int_neg_mult_mono_less_right: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x < y)) then y * n < x * n))

int_neg_mult_right_cancel_le: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x * n ≤ y * n)) then y ≤ x))

int_neg_mult_right_cancel_less: (all n:Int, x:Int, y:Int. (if ((n < +0) and (x * n < y * n)) then y < x))

int_nonneg_mult_mono_le_left: (all n:Int, x:Int, y:Int. (if ((+0 ≤ n) and (x ≤ y)) then n * x ≤ n * y))

int_nonneg_mult_mono_le_right: (all n:Int, x:Int, y:Int. (if ((+0 ≤ n) and (x ≤ y)) then x * n ≤ y * n))

int_nonpos_mult_mono_le_left: (all n:Int, x:Int, y:Int. (if ((n ≤ +0) and (x ≤ y)) then n * y ≤ n * x))

int_nonpos_mult_mono_le_right: (all n:Int, x:Int, y:Int. (if ((n ≤ +0) and (x ≤ y)) then y * n ≤ x * n))

auto int_one_mult

int_one_mult: (all x:Int. +1 * x = x)

int_pos_mult_left_cancel_le: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (n * x ≤ n * y)) then x ≤ y))

int_pos_mult_left_cancel_less: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (n * x < n * y)) then x < y))

int_pos_mult_mono_less_left: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x < y)) then n * x < n * y))

int_pos_mult_mono_less_right: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x < y)) then x * n < y * n))

int_pos_mult_right_cancel_le: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x * n ≤ y * n)) then x ≤ y))

int_pos_mult_right_cancel_less: (all n:Int, x:Int, y:Int. (if ((+0 < n) and (x * n < y * n)) then x < y))

auto int_zero_mult

int_zero_mult: (all x:Int. +0 * x = +0)