Theorem: Nat.xor_comm (Extra/Nat/Bitwise.lean)

State before:
x y : Nat
⊢ x ^^^ y = y ^^^ x
Tactic:
induction x using Nat.recBit generalizing y <;> cases y using Nat.casesBitOn <;> simp [*]
State after:
no goals