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
case mk
j : Int
mi ni : Nat
⊢ mi ⊖ ni ≤ j ∨ j < mi ⊖ ni
no goals