real_dist_mult_add_right: (all x:Real, y:Real, z:Real. (y + z) * x = y * x + z * x)

real_dist_mult_sub: (all x:Real, y:Real, z:Real. x * (y - z) = x * y - x * z)

real_dist_mult_sub_right: (all x:Real, y:Real, z:Real. (y - z) * x = y * x - z * x)

real_div_mult_cancel: (all x:Real, y:Real. (if y ≠ real(+0) then (x / y) * y = x))

auto real_div_one

real_div_one: (all x:Real. x / real(+1) = x)

real_div_self: (all x:Real. (if x ≠ real(+0) then x / x = real(+1)))

auto real_div_zero

real_div_zero: (all x:Real. x / real(+0) = real(+0))

real_inv_inv: (all x:Real. inv(inv(x)) = x)

real_inv_mult: (all x:Real. (if x ≠ real(+0) then inv(x) * x = real(+1)))

real_inv_mult_distr: (all x:Real, y:Real. inv(x * y) = inv(x) * inv(y))

real_inv_neg: (all x:Real. inv(- x) = - inv(x))

real_inv_not_zero: (all x:Real. (if x ≠ real(+0) then inv(x) ≠ real(+0)))

auto real_inv_one

real_inv_one: inv(real(+1)) = real(+1)

real_inv_unique: (all x:Real, y:Real. (if x * y = real(+1) then inv(x) = y))

auto real_inv_zero

real_mult_div_cancel: (all x:Real, y:Real. (if y ≠ real(+0) then (x * y) / y = x))

real_mult_inv_cross: (all a:Real, b:Real, c:Real, d:Real. (if (b ≠ real(+0) and d ≠ real(+0) and (a * d = c * b)) then a * inv(b) = c * inv(d)))

real_mult_left_cancel: (all x:Real, y:Real, z:Real. (if (x ≠ real(+0) and (x * y = x * z)) then y = z))

real_mult_neg: (all x:Real, y:Real. x * - y = - (x * y))

auto real_mult_one

real_mult_right_cancel: (all x:Real, y:Real, z:Real. (if (x ≠ real(+0) and (y * x = z * x)) then y = z))

real_mult_to_zero: (all x:Real, y:Real. (if x * y = real(+0) then ((x = real(+0)) or (y = real(+0)))))

auto real_mult_zero

real_mult_zero: (all x:Real. x * real(+0) = real(+0))

real_neg_mult: (all x:Real, y:Real. - x * y = - (x * y))

real_neg_mult_neg: (all x:Real, y:Real. - x * - y = x * y)

real_neg_one_mult: (all x:Real. - real(+1) * x = - x)

auto real_one_mult

real_one_mult: (all x:Real. real(+1) * x = x)

auto real_zero_div

real_zero_div: (all x:Real. real(+0) / x = real(+0))

auto real_zero_mult

real_zero_mult: (all x:Real. real(+0) * x = real(+0))