English
In a linear order, compare(a,b) ≠ Ordering.lt iff b ≤ a.
Русский
В линейном порядке compare(a,b) ≠ Ordering.lt тогда и только тогда, когда b ≤ a.
LaTeX
$$$\operatorname{compare}(a,b) \neq \mathrm{Ordering.lt} \iff b \le a$$$
Lean4
theorem compare_ge_iff_ge : compare a b ≠ .lt ↔ b ≤ a :=
by
cases h : compare a b
· simpa using compare_lt_iff_lt.1 h
· simpa using le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h
· simpa using le_of_lt <| compare_gt_iff_gt.1 h