α : Type ?u.484320
m n : Num
⊢ Ordering.swap (cmp m n) = Ordering.lt ↔ cmp m n = Ordering.gt
α : Type ?u.484320
m n : Num
⊢ cmp n m = Ordering.lt ↔ cmp m n = Ordering.gt
rw [← cmp_swap]
no goals
α : Type ?u.484320
m n : Num
⊢ Ordering.swap (cmp m n) = Ordering.lt ↔ cmp m n = Ordering.gt
cases cmp m n <;> exact by decide
no goals
α : Type ?u.484320
m n : Num
⊢ Ordering.swap Ordering.gt = Ordering.lt ↔ Ordering.gt = Ordering.gt
decide