Theorem: Int.le_or_gt (GMLInit/Data/Int.lean)

State before:
i j : Int
⊢ i ≤ j ∨ j < i
Tactic:
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
State after:
no goals

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

State before:
case mk.mk
mi ni mj nj : Nat
⊢ mi ⊖ ni ≤ mj ⊖ nj ∨ mj ⊖ nj < mi ⊖ ni
Tactic:
rw [mk_le_mk, mk_lt_mk]
State after:
case mk.mk
mi ni mj nj : Nat
⊢ nj + mi ≤ mj + ni ∨ ni + mj < mi + nj

State before:
case mk.mk
mi ni mj nj : Nat
⊢ nj + mi ≤ mj + ni ∨ ni + mj < mi + nj
Tactic:
rw [Nat.add_comm mi, Nat.add_comm mj]
State after:
case mk.mk
mi ni mj nj : Nat
⊢ nj + mi ≤ ni + mj ∨ ni + mj < nj + mi

State before:
case mk.mk
mi ni mj nj : Nat
⊢ nj + mi ≤ ni + mj ∨ ni + mj < nj + mi
Tactic:
exact (Nat.lt_or_ge ..).symm
State after:
no goals