case zero =>
  have : k.pred.succ = k := Nat.succ_pred_eq_of_pos h
  rw [←this, Nat.shiftLeft_succ]
  conv => lhs; change decide ((2*n <<< k.pred) % 2 = 1); simp
n k : Nat
h : zero < k
⊢ getBit (n <<< k) zero = false
no goals