Theorem rneg_dist_add

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 1, 2 ⊢ a + b ∈ ℝ, radd_closed 1 2.
04. 1 ⊢ (-1)⋅a = -a, rmul_minus_one 1.
05. 2 ⊢ (-1)⋅b = -b, rmul_minus_one 2.
06. 1, 2 ⊢ (-1)⋅(a + b) = -(a + b), rmul_minus_one 3.
07. 1, 2 ⊢ -(a + b) = (-1)⋅(a + b), eq_symm 6.
08. ⊢ -1 ∈ ℝ, calc.
09. 1, 2 ⊢ (-1)⋅(a + b) = (-1)⋅a + (-1)⋅b,
  rmul_distl_add 8 1 2.
10. 1, 2 ⊢ -(a + b) = (-1)⋅a + (-1)⋅b, eq_trans 7 9.
11. 1, 2 ⊢ -(a + b) = -a + (-1)⋅b,
  eq_subst 4 10, P t ↔ -(a + b) = t + (-1)⋅b.
12. 1, 2 ⊢ -(a + b) = -a + -b,
  eq_subst 5 11, P t ↔ -(a + b) = -a + t.
rneg_dist_add. ⊢ a ∈ ℝ → b ∈ ℝ → -(a + b) = -a + -b,
  subj_intro_ii 12.

Dependencies
The given proof depends on 12 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rmul_closed, rmul_comm, rmul_distl_add, rmul_neutr, rneg_closed.