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