Theorem rle_neg_swaps

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ a ≤ b, hypo.
04. 1, 2, 3 ⊢ a - a ≤ b - a, rle_compat_sub 1 2 1 3.
05. 1 ⊢ a - a = 0, rsub_self 1.
06. 1, 2, 3 ⊢ 0 ≤ b - a, eq_subst 5 4, P t ↔ t ≤ b - a.
07. ⊢ 0 ∈ ℝ, calc.
08. 1, 2 ⊢ b - a ∈ ℝ, rsub_closed 2 1.
09. 1, 2, 3 ⊢ 0 - b ≤ (b - a) - b, rle_compat_sub 7 8 2 6.
10. ⊢ b - a = b + -a, rsub_eq.
11. 1 ⊢ -a ∈ ℝ, rneg_closed 1.
12. 1, 2 ⊢ b + -a = -a + b, radd_comm 2 11.
13. 1, 2 ⊢ b - a = -a + b, eq_trans 10 12.
14. 1, 2 ⊢ (b - a) - b = (-a + b) - b, eq_cong 13, f t = t - b.
15. 1, 2 ⊢ (-a + b) - b = -a, radd_cancel 11 2.
16. 1, 2 ⊢ (b - a) - b = -a, eq_trans 14 15.
17. 1, 2, 3 ⊢ 0 - b ≤ -a, le_eq_trans 9 16.
18. 2 ⊢ 0 - b = -b, rsub_from_zero 2.
19. 1, 2, 3 ⊢ -b ≤ -a, eq_subst 18 17, P t ↔ t ≤ -a.
rle_neg_swaps. ⊢ a ∈ ℝ → b ∈ ℝ → a ≤ b → -b ≤ -a,
  subj_intro_iii 19.

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.