. rw [bitwise_div_two]
  rw [Nat.mul_sub_div 0 2 (2^k) (by rw [Nat.mul_comm]; exact Nat.pos_pow_of_pos (n:=2) (k+1) (by decide))]
  rw [Nat.mod_mul_div_left n 2 (2^k)]
  exact h_ind (n/2)
case hdiv
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) / 2 = n % (2 * 2 ^ k) / 2

case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) % 2 = n % (2 * 2 ^ k) % 2
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ bitwise and n (2 * 2 ^ k - 1) % 2 = n % (2 * 2 ^ k) % 2