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

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

real_add_inverse_unique: (all x:Real, y:Real. (if x + y = real(+0) then y = - x))

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

real_add_sub_cancel: (all x:Real, y:Real. (x + y) - y = x)

auto real_add_zero

real_neg_distr_add: (all x:Real, y:Real. - (x + y) = - x + - y)

real_neg_injective: (all x:Real, y:Real. (if - x = - y then x = y))

real_neg_involutive: (all x:Real. - (- x) = x)

real_neg_sub: (all x:Real, y:Real. - (x - y) = y - x)

auto real_neg_zero

real_neg_zero: - real(+0) = real(+0)

real_sub_add_cancel: (all x:Real, y:Real. (x - y) + y = x)

auto real_sub_cancel

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

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

auto real_sub_zero

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

auto real_zero_add

real_zero_add: (all x:Real. real(+0) + x = x)

auto real_zero_sub

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