case zero =>
  dsimp [Nat.getBit]; apply decide_eq_decide.mpr
  have := calc
    (2^k.succ - 1) % 2
      = (2^k*2 - 1) % 2 := by rw [Nat.pow_succ]
    _ = (2-1)%2 :=
      Nat.mul_sub_mod_right (Nat.pos_pow_of_pos (n:=2) _ (by decide)) (.step .refl)
    _ = 1 := rfl
  rw [this]
  constructor <;> intros; exact k.zero_lt_succ; rfl
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ getBit (2 ^ succ k - 1) zero = decide (zero < succ k)
no goals