case succ i h_ind =>
  have : k.pred.succ = k := Nat.succ_pred_eq_of_pos (trans i.zero_lt_succ h)
  rw [←this, Nat.shiftLeft_succ]
  conv =>
    lhs; change getBit ((2 * n <<< k.pred) / 2) i
    rw [Nat.mul_div_cancel_left _ (Nat.zero_lt_succ 1)]
  apply h_ind
  exact Nat.lt_of_succ_lt_succ (trans h this.symm)
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
⊢ getBit (n <<< k) (succ i) = false
no goals