Theorem rsub_cancel

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. ⊢ a - b = a + (-b), rsub_eq.
04. ⊢ a - b + b = a + (-b) + b, eq_cong 3, f t = t + b.
05. 2 ⊢ -b ∈ ℝ, rneg_closed 2.
06. 1, 2 ⊢ a + (-b) + b = a + (-b + b), radd_assoc 1 5 2.
07. 2 ⊢ -b + b = b + -b, radd_comm 5 2.
08. 2 ⊢ b + -b = 0, radd_inv 2.
09. 2 ⊢ -b + b = 0, eq_trans 7 8.
10. 2 ⊢ a + (-b + b) = a + 0, eq_cong 9, f t = a + t.
11. 1 ⊢ a + 0 = a, radd_neutr 1.
12. 1, 2 ⊢ a + (-b + b) = a, eq_trans 10 11.
13. 1, 2 ⊢ a + (-b) + b = a, eq_trans 6 12.
14. 1, 2 ⊢ a - b + b = a, eq_trans 4 13.
rsub_cancel. ⊢ a ∈ ℝ → b ∈ ℝ → a - b + b = a,
  subj_intro_ii 14.

Dependencies
The given proof depends on seven axioms:
eq_refl, eq_subst, radd_assoc, radd_comm, radd_inv, radd_neutr, rneg_closed.