Axiom. rmul_neutr
a ∈ ℝ → a⋅1 = a