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