. sorry_arith
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)
case inr
a : ℤ
n : ℕ
h✝ : ¬2 ^ n ≤ mod2 a (n + 1)
⊢ -2 ^ n ≤ mod2 a (n + 1)