cases hi
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
i : Nat
hi : i ≥ succ k
this : n / 2 < 2 ^ k
⊢ getBit n i = false
case refl
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
⊢ getBit n (succ k) = false

case step
k : Nat
h_ind : ∀ {n : Nat}, n < 2 ^ k → ∀ (i : Nat), i ≥ k → getBit n i = false
n : Nat
hn : n < 2 ^ succ k
this : n / 2 < 2 ^ k
m✝ : Nat
a✝ : Nat.le (succ k) m✝
⊢ getBit n (succ m✝) = false