Axiom. rmul_inv
a ∈ ℝ → ¬a = 0 → a⋅(/a) = 1