rw [bitwise_mod_two and (by decide)]
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
⊢ (if (decide (n % 2 = 1) && decide ((2 * 2 ^ k - 1) % 2 = 1)) = true then 1 else 0) = n % (2 * 2 ^ k) % 2