rw [cmp]
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
⊢ (compare x x).swap = Ordering.lt
α : Type
inst✝ : Order α
x : α
cmp : compare x x = Ordering.gt
⊢ Ordering.gt.swap = Ordering.lt