rw [Nat.xor_and, Nat.land_self]
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
⊢ 2 * (n / 2) ^^^ 1 ^^^ (2 * (n / 2) ^^^ 1 &&& 2 * (n / 2)) = 1