case succ k =>
  unfold getBit
  have : i.succ < k.succ ↔ i < k :=
    ⟨λ h => Nat.lt_of_succ_lt_succ h, λ h => Nat.succ_lt_succ h⟩
  rw [decide_eq_decide.mpr this]
  conv => lhs; arg 1; change n%(2^k*2)/2; rw [Nat.mul_comm, Nat.mod_mul_div_left]
  exact h_ind (n/2) k
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) (succ i) = (decide (succ i < succ k) && getBit n (succ i))
no goals