case pos.pos
α : Type ?u.468320
a✝¹ a✝ : PosNum
⊢ Ordering.swap (cmp (pos a✝¹) (pos a✝)) = cmp (pos a✝) (pos a✝¹)
α : Type ?u.468320
m n : Num
⊢ Ordering.swap (cmp m n) = cmp n m
cases m <;> cases n <;> try { unfold cmp } <;> try { rfl }
no goals
case pos.pos
α : Type ?u.468320
a✝¹ a✝ : PosNum
⊢ Ordering.swap (cmp (pos a✝¹) (pos a✝)) = cmp (pos a✝) (pos a✝¹)
apply PosNum.cmp_swap