Theorem rle_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,
  rle_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.
rle_compat_sub. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a ≤ b → a - c ≤ b - c, subj_intro_iv 10.

Dependencies
The given proof depends on four axioms:
eq_refl, eq_subst, rle_compat_add, rneg_closed.