English
For any a,b, 0 < a - b if and only if b < a or b = ⊤.
Русский
Для любых a,b верно: 0 < a − b тогда и только тогда, когда b < a или b = ⊤.
LaTeX
$$0 < a - b \iff b < a \lor b = \top$$
Lean4
theorem sub_pos (a b : α) : 0 < a - b ↔ b < a ∨ b = ⊤
where
mp
h := by
refine or_iff_not_imp_right.mpr fun h2 ↦ ?_
replace h := strictMono_add_left_of_ne_top _ h2 h
simp only [zero_add] at h
rw [sub_eq_add_neg, add_assoc, add_comm (-b), add_neg_cancel_of_ne_top h2, add_zero] at h
exact h
mpr
h := by
rcases h with h | h
· convert strictMono_add_left_of_ne_top (-b) (by simp [h.ne_top]) h using 1
· simp [add_neg_cancel_of_ne_top h.ne_top]
· simp [sub_eq_add_neg]
· rw [h]
simp only [sub_eq_add_neg, LinearOrderedAddCommGroupWithTop.neg_top, add_top]
apply lt_of_le_of_ne le_top
exact Ne.symm top_ne_zero
