conv => lhs; change decide (n%(2^k*2)%2=1); rw [Nat.mod_mul_mod_right]
n k : Nat
⊢ getBit (n % 2 ^ succ k) zero = (decide (zero < succ k) && getBit n zero)
n k : Nat
⊢ decide (n % 2 = 1) = (decide (zero < succ k) && getBit n zero)