rw [Nat.mul_comm, Nat.mul_sub_div 0 2 (2^k) (Nat.mul_pos (by decide) (Nat.pos_pow_of_pos (n:=2) k (by decide)))]
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit ((2 ^ k * 2 - 1) / 2) i = getBit (2 ^ k - 1) i
k : Nat
h_ind : ∀ (i : Nat), getBit (2 ^ k - 1) i = decide (i < k)
i : Nat
⊢ getBit (2 ^ k - succ (0 / 2)) i = getBit (2 ^ k - 1) i