Axiom. radd_neutr
a ∈ ℝ → a + 0 = a