Theorem: FinInt.mod2_ge (MLIR/Util/FinInt.lean)

State before:
a : ℤ
n : ℕ
⊢ mod2 a n ≥ 0
Tactic:
simp [mod2]
State after:
a : ℤ
n : ℕ
⊢ 0 ≤ a % 2 ^ n

State before:
a : ℤ
n : ℕ
⊢ 0 ≤ a % 2 ^ n
Tactic:
apply Int.mod_ge
State after:
case a
a : ℤ
n : ℕ
⊢ a ≥ 0

State before:
case a
a : ℤ
n : ℕ
⊢ a ≥ 0
Tactic:
have h := Int.ge_add_ge_right (2^n) (@Int.mod_ge_neg a (2^n))
State after:
case a
a : ℤ
n : ℕ
h : a % 2 ^ n + 2 ^ n ≥ -2 ^ n + 2 ^ n
⊢ a ≥ 0

State before:
case a
a : ℤ
n : ℕ
h : a % 2 ^ n + 2 ^ n ≥ -2 ^ n + 2 ^ n
⊢ a ≥ 0
Tactic:
rw [Int.add_left_neg] at h
State after:
case a
a : ℤ
n : ℕ
h : a % 2 ^ n + 2 ^ n ≥ 0
⊢ a ≥ 0

State before:
case a
a : ℤ
n : ℕ
h : a % 2 ^ n + 2 ^ n ≥ 0
⊢ a ≥ 0
Tactic:
sorry
State after:
no goals