rat_dist_mult_add: (all x:Rat, y:Rat, z:Rat. x * (y + z) = x * y + x * z)

rat_dist_mult_add_right: (all x:Rat, y:Rat, z:Rat. (y + z) * x = y * x + z * x)

rat_dist_mult_sub: (all x:Rat, y:Rat, z:Rat. x * (y - z) = x * y - x * z)

rat_dist_mult_sub_right: (all x:Rat, y:Rat, z:Rat. (y - z) * x = y * x - z * x)

rat_div_def: (all x:Rat, y:Rat. x / y = x * inv(y))

rat_div_mult_cancel: (all x:Rat, y:Rat. (if y ≠ rat(+0) then (x / y) * y = x))

auto rat_div_one

rat_div_one: (all x:Rat. x / rat(+1) = x)

rat_div_self: (all x:Rat. (if x ≠ rat(+0) then x / x = rat(+1)))

auto rat_div_zero

rat_div_zero: (all x:Rat. x / rat(+0) = rat(+0))

rat_frac_self: (all k:UInt. (if 0 < k then frac(pos(k), k) = rat(+1)))

rat_inv_frac: (all a:UInt, d:UInt. (if ((0 < a) and (0 < d)) then inv(frac(pos(a), d)) = frac(pos(d), a)))

rat_inv_frac_neg: (all a:UInt, d:UInt. (if ((0 < a) and (0 < d)) then inv(frac(- pos(a), d)) = frac(- pos(d), a)))

rat_inv_inv: (all x:Rat. inv(inv(x)) = x)

rat_inv_mult: (all x:Rat. (if x ≠ rat(+0) then inv(x) * x = rat(+1)))

rat_inv_mult_distr: (all x:Rat, y:Rat. inv(x * y) = inv(x) * inv(y))

rat_inv_neg: (all x:Rat. inv(- x) = - inv(x))

rat_inv_one: inv(rat(+1)) = rat(+1)

rat_inv_unique: (all x:Rat, y:Rat. (if x * y = rat(+1) then inv(x) = y))

auto rat_inv_zero

rat_inv_zero: inv(rat(+0)) = rat(+0)

rat_mult_assoc: (all x:Rat, y:Rat, z:Rat. (x * y) * z = x * (y * z))

rat_mult_commute: (all x:Rat, y:Rat. x * y = y * x)

rat_mult_div_cancel: (all x:Rat, y:Rat. (if y ≠ rat(+0) then (x * y) / y = x))

rat_mult_inv: (all x:Rat. (if x ≠ rat(+0) then x * inv(x) = rat(+1)))

rat_mult_left_cancel: (all x:Rat, y:Rat, z:Rat. (if (x ≠ rat(+0) and (x * y = x * z)) then y = z))

rat_mult_neg: (all x:Rat, y:Rat. x * - y = - (x * y))

auto rat_mult_one

rat_mult_one: (all x:Rat. x * rat(+1) = x)

rat_mult_right_cancel: (all x:Rat, y:Rat, z:Rat. (if (x ≠ rat(+0) and (y * x = z * x)) then y = z))

rat_mult_to_zero: (all x:Rat, y:Rat. (if x * y = rat(+0) then ((x = rat(+0)) or (y = rat(+0)))))

auto rat_mult_zero

rat_mult_zero: (all x:Rat. x * rat(+0) = rat(+0))

rat_neg_mult: (all x:Rat, y:Rat. - x * y = - (x * y))

rat_neg_mult_neg: (all x:Rat, y:Rat. - x * - y = x * y)

rat_neg_one_mult: (all x:Rat. - rat(+1) * x = - x)

auto rat_one_mult

rat_one_mult: (all x:Rat. rat(+1) * x = x)

rat_one_not_zero: rat(+1) ≠ rat(+0)

auto rat_zero_div

rat_zero_div: (all x:Rat. rat(+0) / x = rat(+0))

auto rat_zero_mult

rat_zero_mult: (all x:Rat. rat(+0) * x = rat(+0))