Theorem: Int.le_succ (MLIR/Util/Arith.lean)

State before:
n : ℤ
⊢ n ≤ n + 1
Tactic:
suffices NonNeg 1 by simp [LE.le, Int.le, add_sub_assoc, add_sub]; trivial
State after:
n : ℤ
⊢ NonNeg 1

State before:
n : ℤ
⊢ NonNeg 1
Tactic:
constructor
State after:
no goals

State before:
n : ℤ
this : NonNeg 1
⊢ n ≤ n + 1
Tactic:
simp [LE.le, Int.le, add_sub_assoc, add_sub]
State after:
n : ℤ
this : NonNeg 1
⊢ NonNeg 1

State before:
n : ℤ
this : NonNeg 1
⊢ NonNeg 1
Tactic:
trivial
State after:
no goals