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
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
⊢ (2 ^ succ k - 1) % 2 = 1 ↔ 0 < succ k
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
this : (2 ^ succ k - 1) % 2 = 1
⊢ (2 ^ succ k - 1) % 2 = 1 ↔ 0 < succ k