real_abs_add: (all x:Real, y:Real. abs(x + y) ≤ abs(x) + abs(y))

real_abs_le_iff: (all x:Real, y:Real. (abs(x) ≤ y) = ((- y ≤ x) and (x ≤ y)))

real_abs_mult: (all x:Real, y:Real. abs(x * y) = abs(x) * abs(y))

real_abs_neg: (all x:Real. abs(- x) = abs(x))

real_abs_nonneg: (all x:Real. real(+0) ≤ abs(x))

real_abs_nonneg_eq: (all x:Real. (if real(+0) ≤ x then abs(x) = x))

real_abs_nonpos_eq: (all x:Real. (if x ≤ real(+0) then abs(x) = - x))

real_add_both_sides_of_less: (all x:Real, y:Real, z:Real. (x + y < x + z) = (y < z))

real_add_both_sides_of_less_equal: (all x:Real, y:Real, z:Real. (x + y ≤ x + z) = (y ≤ z))

real_add_both_sides_of_less_equal_right: (all x:Real, y:Real, z:Real. (y + x ≤ z + x) = (y ≤ z))

real_add_both_sides_of_less_right: (all x:Real, y:Real, z:Real. (y + x < z + x) = (y < z))

real_add_le_left_mono: (all x:Real, y:Real, z:Real. (if x ≤ y then z + x ≤ z + y))

real_add_mono_less: (all a:Real, b:Real, c:Real, d:Real. (if ((a < c) and (b < d)) then a + b < c + d))

real_add_mono_less_equal: (all a:Real, b:Real, c:Real, d:Real. (if ((a ≤ c) and (b ≤ d)) then a + b ≤ c + d))

real_dichotomy: (all x:Real, y:Real. ((x ≤ y) or (y < x)))

real_inv_pos: (all x:Real. (if real(+0) < x then real(+0) < inv(x)))

real_le_abs: (all x:Real. x ≤ abs(x))

real_le_iff_sub_nonneg: (all x:Real, y:Real. (x ≤ y) = (real(+0) ≤ y - x))

real_less_equal_iff_less_or_equal: (all x:Real, y:Real. ((x ≤ y) ⇔ ((x < y) or (x = y))))

real_less_equal_iff_not_greater: (all x:Real, y:Real. ((x ≤ y) ⇔ (not (y < x))))

real_less_equal_refl: (all x:Real. x ≤ x)

real_less_iff_sub_pos: (all x:Real, y:Real. (x < y) = (real(+0) < y - x))

real_less_implies_less_equal: (all x:Real, y:Real. (if x < y then x ≤ y))

real_less_implies_not_equal: (all x:Real, y:Real. (if x < y then x ≠ y))

real_less_implies_not_greater: (all x:Real, y:Real. (if x < y then not (y < x)))

real_less_irreflexive: (all x:Real. not (x < x))

real_less_trans: (all x:Real, y:Real, z:Real. (if ((x < y) and (y < z)) then x < z))

real_less_trans_less_equal_left: (all x:Real, y:Real, z:Real. (if ((x ≤ y) and (y < z)) then x < z))

real_less_trans_less_equal_right: (all x:Real, y:Real, z:Real. (if ((x < y) and (y ≤ z)) then x < z))

real_max_equal_greater_left: (all x:Real, y:Real. (if y ≤ x then max(x, y) = x))

real_max_equal_greater_right: (all x:Real, y:Real. (if x ≤ y then max(x, y) = y))

real_max_greater_left: (all x:Real, y:Real. x ≤ max(x, y))

real_max_greater_right: (all x:Real, y:Real. y ≤ max(x, y))

real_max_less_equal: (all x:Real, y:Real, z:Real. (if ((x ≤ z) and (y ≤ z)) then max(x, y) ≤ z))

real_max_symmetric: (all x:Real, y:Real. max(x, y) = max(y, x))

real_min_equal_less_left: (all x:Real, y:Real. (if x ≤ y then min(x, y) = x))

real_min_equal_less_right: (all x:Real, y:Real. (if y ≤ x then min(x, y) = y))

real_min_greatest_less_equal: (all x:Real, y:Real, z:Real. (if ((z ≤ x) and (z ≤ y)) then z ≤ min(x, y)))

real_min_less_equal_left: (all x:Real, y:Real. min(x, y) ≤ x)

real_min_less_equal_right: (all x:Real, y:Real. min(x, y) ≤ y)

real_min_symmetric: (all x:Real, y:Real. min(x, y) = min(y, x))

real_mult_pos: (all x:Real, y:Real. (if ((real(+0) < x) and (real(+0) < y)) then real(+0) < x * y))

real_neg_abs_le: (all x:Real. - abs(x) ≤ x)

real_neg_le_iff: (all x:Real, y:Real. (- y ≤ - x) = (x ≤ y))

real_neg_le_zero: (all x:Real. (- x ≤ real(+0)) = (real(+0) ≤ x))

real_neg_less_iff: (all x:Real, y:Real. (- y < - x) = (x < y))

real_nonneg_mult_mono_le_left: (all z:Real, x:Real, y:Real. (if ((real(+0) ≤ z) and (x ≤ y)) then z * x ≤ z * y))

real_nonneg_mult_mono_le_right: (all z:Real, x:Real, y:Real. (if ((real(+0) ≤ z) and (x ≤ y)) then x * z ≤ y * z))

real_not_less_equal_iff_greater: (all x:Real, y:Real. ((not (x ≤ y)) ⇔ (y < x)))

real_not_less_implies_less_equal: (all x:Real, y:Real. (if not (x < y) then y ≤ x))

real_pos_mult_le_iff: (all z:Real, x:Real, y:Real. (if real(+0) < z then (x * z ≤ y * z) = (x ≤ y)))

real_pos_mult_less_iff: (all z:Real, x:Real, y:Real. (if real(+0) < z then (x * z < y * z) = (x < y)))

real_pos_mult_mono_less_left: (all z:Real, x:Real, y:Real. (if ((real(+0) < z) and (x < y)) then z * x < z * y))

real_pos_mult_mono_less_right: (all z:Real, x:Real, y:Real. (if ((real(+0) < z) and (x < y)) then x * z < y * z))

real_square_nonneg: (all x:Real. real(+0) ≤ x * x)

real_trichotomy: (all x:Real, y:Real. ((x < y) or (x = y) or (y < x)))

real_zero_le_neg: (all x:Real. (real(+0) ≤ - x) = (x ≤ real(+0)))

real_zero_less_neg: (all x:Real. (real(+0) < - x) = (x < real(+0)))

real_zero_less_one: real(+0) < real(+1)