apply (Nat.succ_pred_eq_of_pos ?_).symm
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
⊢ i - k = succ (pred (i - 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
⊢ 0 < i - k