add_both_sides_of_less: (all x:Nat, y:Nat, z:Nat. ((x + y < x + z) ⇔ (y < z)))

add_both_sides_of_less_equal: (all x:Nat. (all y:Nat, z:Nat. ((x + y ≤ x + z) ⇔ (y ≤ z))))

add_mono_less: (all a:Nat, b:Nat, c:Nat, d:Nat. (if ((a < c) and (b < d)) then a + b < c + d))

add_mono_less_equal: (all a:Nat, b:Nat, c:Nat, d:Nat. (if ((a ≤ c) and (b ≤ d)) then a + b ≤ c + d))

dichotomy: (all x:Nat, y:Nat. ((x ≤ y) or (y < x)))

dist_mult_monus: (all x:Nat. (all y:Nat, z:Nat. x * (y ∸ z) = x * y ∸ x * z))

dist_mult_monus_one: (all x:Nat, y:Nat. x * (y ∸ suc(zero)) = x * y ∸ x)

equal_implies_less_equal: (all x:Nat, y:Nat. (if x = y then x ≤ y))

greater_implies_not_equal: (all x:Nat, y:Nat. (if x > y then x ≠ y))

le_exists_monus: (all n:Nat, m:Nat. (if n ≤ m then some x:Nat. m = n + x))

le_less_trans: (all m:Nat, n:Nat, o:Nat. (if ((m ≤ n) and (n < o)) then m < o))

less_equal_add: (all x:Nat. (all y:Nat. x ≤ x + y))

less_equal_add_left: (all x:Nat, y:Nat. y ≤ x + y)

less_equal_add_monus: (all m:Nat. (all n:Nat, o:Nat. (if ((n ≤ m) and (m ≤ n + o)) then m ∸ n ≤ o)))

less_equal_antisymmetric: (all x:Nat. (all y:Nat. (if ((x ≤ y) and (y ≤ x)) then x = y)))

less_equal_implies_less_or_equal: (all x:Nat. (all y:Nat. (if x ≤ y then ((x < y) or (x = y)))))

less_equal_not_equal_implies_less: (all x:Nat, y:Nat. (if ((x ≤ y) and x ≠ y) then x < y))

less_equal_refl: (all n:Nat. n ≤ n)

less_equal_trans: (all m:Nat. (all n:Nat, o:Nat. (if ((m ≤ n) and (n ≤ o)) then m ≤ o)))

less_implies_less_equal: (all x:Nat. (all y:Nat. (if x < y then x ≤ y)))

less_implies_not_equal: (all x:Nat, y:Nat. (if x < y then x ≠ y))

less_implies_not_greater: (all x:Nat. (all y:Nat. (if x < y then not (y < x))))

less_irreflexive: (all x:Nat. not (x < x))

less_le_trans: (all m:Nat, n:Nat, o:Nat. (if ((m < n) and (n ≤ o)) then m < o))

less_suc_iff_suc_less: (all x:Nat, y:Nat. ((x < y) ⇔ (suc(x) < suc(y))))

less_trans: (all m:Nat, n:Nat, o:Nat. (if ((m < n) and (n < o)) then m < o))

max_assoc: (all x:Nat, y:Nat, z:Nat. max(max(x, y), z) = max(x, max(y, z)))

max_equal_greater_left: (all x:Nat, y:Nat. (if y ≤ x then max(x, y) = x))

max_equal_greater_right: (all x:Nat, y:Nat. (if x ≤ y then max(x, y) = y))

max_greater_left: (all x:Nat, y:Nat. x ≤ max(x, y))

max_greater_right: (all y:Nat, x:Nat. y ≤ max(x, y))

max_is_left_or_right: (all x:Nat, y:Nat. ((max(x, y) = x) or (max(x, y) = y)))

max_less_equal: (all x:Nat, y:Nat, z:Nat. (if ((x ≤ z) and (y ≤ z)) then max(x, y) ≤ z))

max_symmetric: (all x:Nat, y:Nat. max(x, y) = max(y, x))

monus_add_assoc: (all n:Nat. (all l:Nat, m:Nat. (if m ≤ n then l + (n ∸ m) = (l + n) ∸ m)))

monus_add_identity: (all n:Nat. (all m:Nat. (if m ≤ n then m + (n ∸ m) = n)))

monus_right_cancel: (all x:Nat, y:Nat, a:Nat. (if ((x ∸ a = y ∸ a) and (a ≤ x) and (a ≤ y)) then x = y))

mult_cancel_left_less: (all x:Nat, y:Nat, z:Nat. (if x * y < x * z then y < z))

mult_cancel_right_less: (all x:Nat, y:Nat, z:Nat. (if y * x < z * x then y < z))

mult_mono_le: (all n:Nat. (all x:Nat, y:Nat. (if x ≤ y then n * x ≤ n * y)))

mult_mono_le2: (all n:Nat, x:Nat, m:Nat, y:Nat. (if ((n ≤ m) and (x ≤ y)) then n * x ≤ m * y))

mult_mono_le_r: (all n:Nat. (all x:Nat, y:Nat. (if x ≤ y then x * n ≤ y * n)))

n_le_nn: (all n:Nat. n ≤ n * n)

not_less_equal_iff_greater: (all x:Nat, y:Nat. ((not (x ≤ y)) ⇔ (y < x)))

not_less_equal_less_equal: (all x:Nat, y:Nat. (if not (x ≤ y) then y ≤ x))

not_less_implies_less_equal: (all x:Nat. (all y:Nat. (if not (x < y) then y ≤ x)))

trichotomy: (all x:Nat. (all y:Nat. ((x < y) or (x = y) or (y < x))))

trichotomy2: (all y:Nat, x:Nat. (if (x ≠ y and not (x < y)) then y < x))

zero_or_positive: (all x:Nat. ((x = zero) or (zero < x)))