apply h_ind
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 <<< pred k) i = false
case h
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
⊢ i < pred k