have : ∀ k, 1 &&& 2 * k = 0 := by
  intro k; rw [Nat.land_comm, Nat.land_one, Nat.mul_mod_right]
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1
n : Nat
this✝¹ : n = 2 * (n / 2) + 1
this✝ : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
this : ∀ (k : Nat), 1 &&& 2 * k = 0
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1