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