intro k
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ ∀ (k : Nat), 1 &&& 2 * k = 0
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
k : Nat
⊢ 1 &&& 2 * k = 0