simp [this (2^k) (Nat.pos_pow_of_pos k (by decide))]
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
this : ∀ (l : Nat), l > 0 → (2 * l - 1) % 2 = 1
⊢ (if n % 2 = 1 ∧ (2 * 2 ^ k - 1) % 2 = 1 then 1 else 0) = n % (2 * 2 ^ k) % 2
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
this : ∀ (l : Nat), l > 0 → (2 * l - 1) % 2 = 1
⊢ (if n % 2 = 1 then 1 else 0) = n % (2 * 2 ^ k) % 2