case succ k h_ind =>
  have : i-k = (i-k.succ).succ := by
    rw [Nat.sub_succ i k]
    apply (Nat.succ_pred_eq_of_pos ?_).symm
    exact Nat.zero_lt_sub_of_lt h
  conv =>
    lhs; change (n <<< (k+1)).getBit i
    rw [Nat.add_comm, ←Nat.shiftLeft_shiftLeft]
    rw [h_ind (n <<< 1) (Nat.le_of_succ_le h), this]
    change ((2*n)/2).getBit (i-k.succ)
    simp
k : Nat
h_ind : ∀ (n : Nat) {i : Nat}, i ≥ k → getBit (n <<< k) i = getBit n (i - k)
n i : Nat
h : i ≥ succ k
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)
no goals