case succ k h_ind =>
  conv =>
    lhs; rw [Nat.succ_eq_add_one, Nat.add_comm, ←Nat.shiftRight_shiftRight]
    rw [h_ind]
k : Nat
h_ind : ∀ (n i : Nat), getBit (n >>> k) i = getBit n (i + k)
n i : Nat
⊢ getBit (n >>> succ k) i = getBit n (i + succ k)
no goals