Commit 2024-09-12 08:50 2c64747c

feat(Data/Nat/Bitwise): more symmetric statement of Nat.xor_trichotomy (#16693) We state Nat.xor_trichotomy in a more symmetric form. We golf most of the proof and change most simp to rw. Note that this makes the proof of lt_xor_cases (which is useful in the current form for Sprague-Grundy) slightly longer.