have : i.succ < k.succ ↔ i < k :=
  ⟨λ h => Nat.lt_of_succ_lt_succ h, λ h => Nat.succ_lt_succ h⟩
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (succ i < succ k) && getBit (n / 2) i)
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n % 2 ^ succ k / 2) i = (decide (succ i < succ k) && getBit (n / 2) i)