induction k generalizing n i
n k i : Nat
h : i ≥ k
⊢ getBit (n <<< k) i = getBit n (i - k)
case zero
n i : Nat
h : i ≥ zero
⊢ getBit (n <<< zero) i = getBit n (i - zero)

case succ
n✝ : Nat
n_ih✝ : ∀ (n : Nat) {i : Nat}, i ≥ n✝ → getBit (n <<< n✝) i = getBit n (i - n✝)
n i : Nat
h : i ≥ succ n✝
⊢ getBit (n <<< succ n✝) i = getBit n (i - succ n✝)