Theorem rlt_add_cancel_rr

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 4 ⊢ a + c < b + c, hypo.
05. 1, 3 ⊢ a + c ∈ ℝ, radd_closed 1 3.
06. 2, 3 ⊢ b + c ∈ ℝ, radd_closed 2 3.
07. 1, 2, 3, 4 ⊢ a + c - c < b + c - c, rlt_compat_sub 5 6 3 4.
08. 1, 3 ⊢ a + c - c = a, radd_cancel 1 3.
09. 2, 3 ⊢ b + c - c = b, radd_cancel 2 3.
10. 1, 2, 3, 4 ⊢ a < b + c - c, eq_subst 8 7, P t ↔ t < b + c - c.
11. 1, 2, 3, 4 ⊢ a < b, eq_subst 9 10, P t ↔ a < t.
rlt_add_cancel_rr. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a + c < b + c → a < b, subj_intro_iv 11.

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