Theorem rlt_compat_sub

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

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.