apply decide_eq_decide.mpr
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ decide (i < k) = decide (succ i < succ k)
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
this : getBit (2 ^ succ k - 1) (succ i) = getBit (2 ^ k - 1) i
⊢ i < k ↔ succ i < succ k