Axiom. rmul_assoc
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → (a⋅b)⋅c = a⋅(b⋅c)