Axiom. rmul_comm
a ∈ ℝ → b ∈ ℝ → a⋅b = b⋅a