have : ∀ (l : Nat), l > 0 → (2*l - 1) % 2 = 1 := by
  intro l hl
  cases l
  case zero => cases hl
  case succ l =>
    conv =>
      lhs; rw [Nat.mul_succ]; change (2*l+1+1-1)%2
      rw [Nat.add_sub_cancel, Nat.add_comm, Nat.add_mul_mod_self_left]
case hmod
k : Nat
h_ind : ∀ (n : Nat), n &&& 2 ^ k - 1 = n % 2 ^ k
n : Nat
⊢ (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 ∧ (2 * 2 ^ k - 1) % 2 = 1 then 1 else 0) = n % (2 * 2 ^ k) % 2