have : n/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hn
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
⊢ getBit n i = false
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