no goals
α : Type ?u.123313
m : PosNum
⊢ ∀ (n : PosNum), Ordering.swap (cmp m n) = cmp n m
induction' m with m IH m IH <;> intro n <;> cases' n with n n <;> unfold cmp <;>
  try { rfl } <;> rw [← IH] <;> cases cmp m n <;> rfl