English
In a total preorder with decidable order, the two comparison notions cmpLE and cmp coincide.
Русский
В полном преддорепорядке с решаемостью порядка совпадают понятия сравнения cmpLE и cmp.
LaTeX
$$$cmpLE x y = cmp x y$$$
Lean4
theorem cmpLE_eq_cmp {α} [Preorder α] [IsTotal α (· ≤ ·)] [DecidableLE α] [DecidableLT α] (x y : α) :
cmpLE x y = cmp x y :=
by
by_cases xy : x ≤ y <;> by_cases yx : y ≤ x <;> simp [cmpLE, lt_iff_le_not_ge, *, cmp, cmpUsing]
cases not_or_intro xy yx (total_of _ _ _)