case succ k h_ind =>
  have : n/2 < 2^k := (Nat.div_lt_iff_lt_mul (Nat.zero_lt_succ 1)).mpr hn
  cases hi
  case refl =>
    dsimp [getBit]
    exact h_ind ‹n/2 < 2^k› k Nat.le.refl
  case step i hstep =>
    dsimp [getBit]
    exact h_ind ‹n/2 < 2^k› i (Nat.le_of_succ_le hstep)
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
no goals