rat_abs_add: (all x:Rat, y:Rat. abs(x + y) ≤ abs(x) + abs(y))

rat_abs_le_iff: (all x:Rat, y:Rat. (abs(x) ≤ y) = ((- y ≤ x) and (x ≤ y)))

rat_abs_mult: (all x:Rat, y:Rat. abs(x * y) = abs(x) * abs(y))

rat_abs_neg: (all x:Rat. abs(- x) = abs(x))

rat_abs_nonneg: (all x:Rat. rat(+0) ≤ abs(x))

rat_abs_nonneg_eq: (all x:Rat. (if rat(+0) ≤ x then abs(x) = x))

rat_abs_nonpos_eq: (all x:Rat. (if x ≤ rat(+0) then abs(x) = - x))

rat_add_both_sides_of_less: (all x:Rat, y:Rat, z:Rat. (x + y < x + z) = (y < z))

rat_add_both_sides_of_less_equal: (all x:Rat, y:Rat, z:Rat. (x + y ≤ x + z) = (y ≤ z))

rat_add_both_sides_of_less_equal_right: (all x:Rat, y:Rat, z:Rat. (y + x ≤ z + x) = (y ≤ z))

rat_add_both_sides_of_less_right: (all x:Rat, y:Rat, z:Rat. (y + x < z + x) = (y < z))

rat_add_mono_less: (all a:Rat, b:Rat, c:Rat, d:Rat. (if ((a < c) and (b < d)) then a + b < c + d))

rat_add_mono_less_equal: (all a:Rat, b:Rat, c:Rat, d:Rat. (if ((a ≤ c) and (b ≤ d)) then a + b ≤ c + d))

rat_den_neg: (all x:Rat. den(- x) = den(x))

rat_dichotomy: (all x:Rat, y:Rat. ((x ≤ y) or (y < x)))

rat_eq_cross: (all x:Rat, y:Rat. (if num(x) * pos(den(y)) = num(y) * pos(den(x)) then x = y))

rat_inv_pos: (all x:Rat. (if rat(+0) < x then rat(+0) < inv(x)))

rat_le_abs: (all x:Rat. x ≤ abs(x))

rat_le_def: (all x:Rat, y:Rat. (x ≤ y) = (num(x) * pos(den(y)) ≤ num(y) * pos(den(x))))

rat_le_iff_sub_nonneg: (all x:Rat, y:Rat. (x ≤ y) = (rat(+0) ≤ y - x))

rat_le_zero_num: (all x:Rat. (x ≤ rat(+0)) = (num(x) ≤ +0))

rat_less_def: (all x:Rat, y:Rat. (x < y) = (num(x) * pos(den(y)) < num(y) * pos(den(x))))

rat_less_equal_antisymmetric: (all x:Rat, y:Rat. (if ((x ≤ y) and (y ≤ x)) then x = y))

rat_less_equal_iff_less_or_equal: (all x:Rat, y:Rat. ((x ≤ y) ⇔ ((x < y) or (x = y))))

rat_less_equal_iff_not_greater: (all x:Rat, y:Rat. ((x ≤ y) ⇔ (not (y < x))))

rat_less_equal_refl: (all x:Rat. x ≤ x)

rat_less_equal_trans: (all x:Rat, y:Rat, z:Rat. (if ((x ≤ y) and (y ≤ z)) then x ≤ z))

rat_less_iff_sub_pos: (all x:Rat, y:Rat. (x < y) = (rat(+0) < y - x))

rat_less_implies_less_equal: (all x:Rat, y:Rat. (if x < y then x ≤ y))

rat_less_implies_not_equal: (all x:Rat, y:Rat. (if x < y then x ≠ y))

rat_less_implies_not_greater: (all x:Rat, y:Rat. (if x < y then not (y < x)))

rat_less_irreflexive: (all x:Rat. not (x < x))

rat_less_trans: (all x:Rat, y:Rat, z:Rat. (if ((x < y) and (y < z)) then x < z))

rat_less_trans_less_equal_left: (all x:Rat, y:Rat, z:Rat. (if ((x ≤ y) and (y < z)) then x < z))

rat_less_trans_less_equal_right: (all x:Rat, y:Rat, z:Rat. (if ((x < y) and (y ≤ z)) then x < z))

rat_less_zero_num: (all x:Rat. (x < rat(+0)) = (num(x) < +0))

rat_max_equal_greater_left: (all x:Rat, y:Rat. (if y ≤ x then max(x, y) = x))

rat_max_equal_greater_right: (all x:Rat, y:Rat. (if x ≤ y then max(x, y) = y))

rat_max_greater_left: (all x:Rat, y:Rat. x ≤ max(x, y))

rat_max_greater_right: (all x:Rat, y:Rat. y ≤ max(x, y))

rat_max_less_equal: (all x:Rat, y:Rat, z:Rat. (if ((x ≤ z) and (y ≤ z)) then max(x, y) ≤ z))

rat_max_symmetric: (all x:Rat, y:Rat. max(x, y) = max(y, x))

rat_min_equal_less_left: (all x:Rat, y:Rat. (if x ≤ y then min(x, y) = x))

rat_min_equal_less_right: (all x:Rat, y:Rat. (if y ≤ x then min(x, y) = y))

rat_min_greatest_less_equal: (all x:Rat, y:Rat, z:Rat. (if ((z ≤ x) and (z ≤ y)) then z ≤ min(x, y)))

rat_min_less_equal_left: (all x:Rat, y:Rat. min(x, y) ≤ x)

rat_min_less_equal_right: (all x:Rat, y:Rat. min(x, y) ≤ y)

rat_min_symmetric: (all x:Rat, y:Rat. min(x, y) = min(y, x))

rat_mult_nonneg: (all x:Rat, y:Rat. (if ((rat(+0) ≤ x) and (rat(+0) ≤ y)) then rat(+0) ≤ x * y))

rat_mult_pos: (all x:Rat, y:Rat. (if ((rat(+0) < x) and (rat(+0) < y)) then rat(+0) < x * y))

rat_neg_abs_le: (all x:Rat. - abs(x) ≤ x)

rat_neg_le_iff: (all x:Rat, y:Rat. (- y ≤ - x) = (x ≤ y))

rat_neg_less_iff: (all x:Rat, y:Rat. (- y < - x) = (x < y))

rat_nonneg_mult_mono_le_left: (all z:Rat, x:Rat, y:Rat. (if ((rat(+0) ≤ z) and (x ≤ y)) then z * x ≤ z * y))

rat_nonneg_mult_mono_le_right: (all z:Rat, x:Rat, y:Rat. (if ((rat(+0) ≤ z) and (x ≤ y)) then x * z ≤ y * z))

rat_not_less_equal_iff_greater: (all x:Rat, y:Rat. ((not (x ≤ y)) ⇔ (y < x)))

rat_not_less_implies_less_equal: (all x:Rat, y:Rat. (if not (x < y) then y ≤ x))

rat_num_neg: (all x:Rat. num(- x) = - num(x))

rat_pos_mult_le_iff: (all z:Rat, x:Rat, y:Rat. (if rat(+0) < z then (x * z ≤ y * z) = (x ≤ y)))

rat_pos_mult_less_iff: (all z:Rat, x:Rat, y:Rat. (if rat(+0) < z then (x * z < y * z) = (x < y)))

rat_pos_mult_mono_less_left: (all z:Rat, x:Rat, y:Rat. (if ((rat(+0) < z) and (x < y)) then z * x < z * y))

rat_pos_mult_mono_less_right: (all z:Rat, x:Rat, y:Rat. (if ((rat(+0) < z) and (x < y)) then x * z < y * z))

rat_square_nonneg: (all x:Rat. rat(+0) ≤ x * x)

rat_trichotomy: (all x:Rat, y:Rat. ((x < y) or (x = y) or (y < x)))

rat_zero_le_frac: (all n:Int, d:UInt. (if 0 < d then (rat(+0) ≤ frac(n, d)) = (+0 ≤ n)))

rat_zero_le_neg: (all x:Rat. (rat(+0) ≤ - x) = (x ≤ rat(+0)))

rat_zero_le_num: (all x:Rat. (rat(+0) ≤ x) = (+0 ≤ num(x)))

rat_zero_less_frac: (all n:Int, d:UInt. (if 0 < d then (rat(+0) < frac(n, d)) = (+0 < n)))

rat_zero_less_neg: (all x:Rat. (rat(+0) < - x) = (x < rat(+0)))

rat_zero_less_num: (all x:Rat. (rat(+0) < x) = (+0 < num(x)))

rat_zero_less_one: rat(+0) < rat(+1)