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

State before:
a : ℤ
n : ℕ
⊢ smod2 a n ≥ -2 ^ n
Tactic:
simp [smod2]
State after:
a : ℤ
n : ℕ
⊢ -2 ^ n ≤ if 2 ^ n ≤ mod2 a (n + 1) then mod2 a (n + 1) - 2 ^ (n + 1) else mod2 a (n + 1)

State before:
a : ℤ
n : ℕ
⊢ -2 ^ n ≤ if 2 ^ n ≤ mod2 a (n + 1) then mod2 a (n + 1) - 2 ^ (n + 1) else mod2 a (n + 1)
Tactic:
split
State after:
case inl
a : ℤ
n : ℕ
h✝ : 2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1) - 2 ^ (n + 1)

case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1)

State before:
case inl
a : ℤ
n : ℕ
h✝ : 2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1) - 2 ^ (n + 1)

case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1)
Tactic:
. sorry_arith
State after:
case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1)

State before:
case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1)
Tactic:
. apply Int.ge_trans 0 mod2_ge (Int.zero_ge_neg Int.two_pow_ge)
State after:
no goals