Theorem rle_from_diff

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ 0 ≤ b - a, hypo.
04. 1, 2 ⊢ b - a ∈ ℝ, rsub_closed 2 1.
05. ⊢ 0 ∈ ℝ, calc.
06. 1, 2, 3 ⊢ 0 + a ≤ b - a + a, rle_compat_add 5 4 1 3.
07. 1 ⊢ 0 + a = a, radd_neutl 1.
08. 1 ⊢ a = 0 + a, eq_symm 7.
09. 1, 2, 3 ⊢ a ≤ b - a + a, eq_le_trans 8 6.
10. 1, 2 ⊢ b - a + a = b, rsub_cancel 2 1.
11. 1, 2, 3 ⊢ a ≤ b, le_eq_trans 9 10.
rle_from_diff. ⊢ a ∈ ℝ → b ∈ ℝ → 0 ≤ b - a → a ≤ b,
  subj_intro_iii 11.

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