Theorem rle_compat_addl

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 4 ⊢ a ≤ b, hypo.
05. 1, 2, 3, 4 ⊢ a + c ≤ b + c, rle_compat_add 1 2 3 4.
06. 1, 3 ⊢ a + c = c + a, radd_comm 1 3.
07. 2, 3 ⊢ b + c = c + b, radd_comm 2 3.
08. 1, 2, 3, 4 ⊢ c + a ≤ b + c, eq_subst 6 5, P t ↔ t ≤ b + c.
09. 1, 2, 3, 4 ⊢ c + a ≤ c + b, eq_subst 7 8, P t ↔ c + a ≤ t.
rle_compat_addl. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a ≤ b → c + a ≤ c + b, subj_intro_iv 9.

Dependencies
The given proof depends on three axioms:
eq_subst, radd_comm, rle_compat_add.