have : k.pred.succ = k := Nat.succ_pred_eq_of_pos (trans i.zero_lt_succ h)
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
i : Nat
h_ind : ∀ (n k : Nat), i < k → getBit (n <<< k) i = false
n k : Nat
h : succ i < k
this : succ (pred k) = k
⊢ getBit (n <<< k) (succ i) = false