Theorem radd_cancel_rr

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 4 ⊢ a + c = b + c, hypo.
05. 4 ⊢ a + c - c = b + c - c, eq_cong 4, f t = t - c.
06. 1, 3 ⊢ a + c - c = a, radd_cancel 1 3.
07. 2, 3 ⊢ b + c - c = b, radd_cancel 2 3.
08. 1, 3, 4 ⊢ a = b + c - c, eq_trans_ll 6 5.
09. 1, 2, 3, 4 ⊢ a = b, eq_trans 8 7.
radd_cancel_rr. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a + c = b + c → a = b, subj_intro_iv 9.

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