Basic operations on bounded natural numbers.

This file should not depend on anything defined in Mathlib (except for notation), so that it can be upstreamed to Batteries or the Lean standard library easily.

theorem Fin.xor_assoc {n k : ℕ} (h : k = 2 ^ n) (a b c : Fin k) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c)

theorem Fin.xor_comm {k : ℕ} (a b : Fin k) : a ^^^ b = b ^^^ a

@[simp]

theorem Fin.xor_self {k : ℕ} [NeZero k] (a : Fin k) : a ^^^ a = 0

@[simp]

theorem Fin.xor_zero {k : ℕ} [NeZero k] (a : Fin k) : a ^^^ 0 = a