case zero =>
  cases k
  case zero => conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
  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 ^ k) zero = (decide (zero < k) && getBit n zero)
no goals