English
Bitwise XOR on natural numbers corresponds to nimber addition: for all a,b ∈ ℕ, ∗a + ∗b = ∗(a ⊕ b).
Русский
Побитовое XOR для натуральных чисел соответствует сложению Nimber: для любых a,b ∈ ℕ выполняется ∗a + ∗b = ∗(a ⊕ b).
LaTeX
$$$ \forall a,b \in \mathbb{N},\ *a + \ *b = \ *(a \oplus b)$$$
Lean4
/-- Nimber addition of naturals corresponds to the bitwise XOR operation. -/
theorem add_nat (a b : ℕ) : ∗a + ∗b = ∗(a ^^^ b) :=
by
apply le_antisymm
· apply add_le_of_forall_ne
all_goals
intro c hc
obtain ⟨c, rfl⟩ := eq_nat_of_le_nat hc.le
rw [OrderIso.lt_iff_lt] at hc
replace hc := Nat.cast_lt.1 hc
rw [add_nat]
simpa using hc.ne
· apply le_of_not_gt
intro hc
obtain ⟨c, hc'⟩ := eq_nat_of_le_nat hc.le
rw [hc', OrderIso.lt_iff_lt, Nat.cast_lt] at hc
obtain h | h := Nat.lt_xor_cases hc
· apply h.ne
simpa [Nat.xor_comm, Nat.xor_cancel_left, ← hc'] using add_nat (c ^^^ b) b
· apply h.ne
simpa [Nat.xor_comm, Nat.xor_cancel_left, ← hc'] using add_nat a (c ^^^ a)
