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