Theorem rlt_compat_add

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 4 ⊢ a < b, hypo.
05. 4 ⊢ a ≤ b, le_from_lt 4.
06. 1, 2, 3, 4 ⊢ a + c ≤ b + c, rle_compat_add 1 2 3 5.
07. 7 ⊢ a + c = b + c, hypo.
08. 1, 2, 3, 7 ⊢ a = b, radd_cancel_rr 1 2 3 7.
09. 4 ⊢ ¬a = b, neq_from_lt 4.
10. 1, 2, 3, 4, 7 ⊢ ⊥, neg_elim 9 8.
11. 1, 2, 3, 4 ⊢ ¬a + c = b + c, neg_intro 10.
12. 1, 2, 3, 4 ⊢ a + c < b + c, lt_intro 6 11.
rlt_compat_add. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a < b → a + c < b + c, subj_intro_iv 12.

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.