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 ⊢ 0 = a - a, eq_symm 5. 07. 1, 2, 3 ⊢ 0 ≤ b - a, eq_le_trans 6 4. rle_as_diff. ⊢ a ∈ ℝ → b ∈ ℝ → a ≤ b → 0 ≤ b - a, subj_intro_iii 7.
Dependencies
The given proof depends on five axioms:
eq_refl, eq_subst, radd_inv, rle_compat_add, rneg_closed.