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
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)
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
this : i - k = succ (i - succ k)
⊢ getBit (n <<< succ k) i = getBit n (i - succ k)