rw [←Nat.xor_assoc, Nat.xor_comm _ 1, Nat.xor_assoc 1, Nat.xor_self, Nat.xor_zero]
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 2 * (n / 2) ^^^ 1 ^^^ (2 * (n / 2) ^^^ 1 &&& 2 * (n / 2)) = 1
n : Nat
this✝ : n = 2 * (n / 2) + 1
this : 2 * (n / 2) + 1 = 2 * (n / 2) ^^^ 1
⊢ 1 ^^^ 1 &&& 2 * (n / 2) = 1