@[simp]

theorem Nat.xor_mod_two_eq (a : ℕ) (b : ℕ) : (a ^^^ b) % 2 = (a + b) % 2

@[simp]

theorem Nat.even_xor (a : ℕ) (b : ℕ) : Even (a ^^^ b) ↔ (Even a ↔ Even b)