rw [←smod2_idem ha, ←smod2_idem hb]
a b : ℤ
n : ℕ
h : a ≡ b [±2^n]
ha : a ≥ -2 ^ n ∧ a < 2 ^ n
hb : b ≥ -2 ^ n ∧ b < 2 ^ n
⊢ a = b
a b : ℤ
n : ℕ
h : a ≡ b [±2^n]
ha : a ≥ -2 ^ n ∧ a < 2 ^ n
hb : b ≥ -2 ^ n ∧ b < 2 ^ n
⊢ smod2 a n = smod2 b n