rle_neg

Theorem rle_neg

Theorem. rle_neg
a ∈ ℝ → b ∈ ℝ → ¬a ≤ b → b ≤ a

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ ¬a ≤ b, hypo.
04. 1, 2 ⊢ a ≤ b ∨ b ≤ a, rle_total 1 2.
05. 1, 2, 3 ⊢ b ≤ a, tollendo_ponens_right 4 3.
rle_neg. ⊢ a ∈ ℝ → b ∈ ℝ → ¬a ≤ b → b ≤ a,
  subj_intro_iii 5.

Dependencies
The given proof depends on two axioms:
efq, rle_total.