induction i using Int.casesMkOn with
| mk mi ni =>
  induction j using Int.casesMkOn with
  | mk mj nj =>
    rw [mk_le_mk, mk_lt_mk]
    rw [Nat.add_comm mi, Nat.add_comm mj]
    exact (Nat.lt_or_ge ..).symm
i j : Int
⊢ i ≤ j ∨ j < i
no goals