rw [←mod2_idem ha, ←mod2_idem hb]
a b : ℤ
n : ℕ
h : a ≡ b [2^n]
ha : a ≥ 0 ∧ a < 2 ^ n
hb : b ≥ 0 ∧ b < 2 ^ n
⊢ a = b
a b : ℤ
n : ℕ
h : a ≡ b [2^n]
ha : a ≥ 0 ∧ a < 2 ^ n
hb : b ≥ 0 ∧ b < 2 ^ n
⊢ mod2 a n = mod2 b n