Axiom. radd_inv
a ∈ ℝ → a + (-a) = 0