Axiom. radd_comm
a ∈ ℝ → b ∈ ℝ → a + b = b + a