have : 2*(n/2) + 1 = 2*(n/2) ^^^ 1 := by
  apply Nat.add_eq_xor
  rw [Nat.land_one, Nat.mul_mod_right]
n : Nat
this : n = 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