English
Swapping the arguments of cmp reverses their order: (cmp a b).swap = cmp b a.
Русский
Обмен аргументов компаратора меняет их порядок: (cmp a b).swap = cmp b a.
LaTeX
$$$\\forall a\\ b,\\ (cmp a b).swap = cmp b a$$$
Lean4
@[simp]
theorem cmp_swap [Preorder α] [DecidableLT α] (a b : α) : (cmp a b).swap = cmp b a :=
by
unfold cmp cmpUsing
by_cases h : a < b <;> by_cases h₂ : b < a <;> simp [h, h₂, Ordering.swap]
exact lt_asymm h h₂