Theorem rmul_compatr_neg

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. ⊢ 0 ∈ ℝ, calc.
04. 1 ⊢ a⋅0 = 0, rmul_rzero 1.
05. 2 ⊢ b + -b = 0, radd_inv 2.
06. 2 ⊢ a⋅(b + -b) = a⋅0, eq_cong 5, f t = a⋅t.
07. 1, 2 ⊢ a⋅(b + -b) = 0, eq_trans 6 4.
08. 2 ⊢ -b ∈ ℝ, rneg_closed 2.
09. 1, 2 ⊢ a⋅(b + -b) = a⋅b + a⋅(-b), rmul_distl_add 1 2 8.
10. 1, 2 ⊢ 0 = a⋅b + a⋅(-b), eq_trans_ll 7 9.
11. 1, 2 ⊢ 0 + -(a⋅b) = a⋅b + a⋅(-b) + -(a⋅b),
  eq_cong 10, f t = t + -(a⋅b).
12. 1, 2 ⊢ a⋅b ∈ ℝ, rmul_closed 1 2.
13. 1, 2 ⊢ -(a⋅b) ∈ ℝ, rneg_closed 12.
14. 1, 2 ⊢ 0 + -(a⋅b) = -(a⋅b), radd_neutl 13.
15. 1, 2 ⊢ -(a⋅b) = a⋅b  + a⋅(-b) + -(a⋅b),
  eq_trans_ll 14 11.
16. 1, 2 ⊢ a⋅(-b) ∈ ℝ, rmul_closed 1 8.
17. 1, 2 ⊢ a⋅b + a⋅(-b) = a⋅(-b) + a⋅b, radd_comm 12 16.
18. 1, 2 ⊢ -(a⋅b) = a⋅(-b) + a⋅b + -(a⋅b),
  eq_subst 17 15, P t ↔ -(a⋅b) = t + -(a⋅b).
19. 1, 2 ⊢ a⋅(-b) + a⋅b + -(a⋅b) = a⋅(-b) + (a⋅b + -(a⋅b)),
  radd_assoc 16 12 13.
20. 1, 2 ⊢ -(a⋅b) = a⋅(-b) + (a⋅b + -(a⋅b)), eq_trans 18 19.
21. 1, 2 ⊢ a⋅b + -(a⋅b) = 0, radd_inv 12.
22. 1, 2 ⊢ -(a⋅b) = a⋅(-b) + 0,
  eq_subst 21 20, P t ↔ -(a⋅b) = a⋅(-b) + t.
23. 1, 2 ⊢ a⋅(-b) + 0 = a⋅(-b), radd_neutr 16.
24. 1, 2 ⊢ -(a⋅b) = a⋅(-b), eq_trans 22 23.
rmul_compatr_neg. ⊢ a ∈ ℝ → b ∈ ℝ → -(a⋅b) = a⋅(-b),
  subj_intro_ii 24.

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