Commit 2024-12-21 22:54 e7d8b80a
View on Github →feat(SetTheory/Game/PGame): neg_identical_neg_iff (#20149)
Adds neg_identical_neg_iff: x ≡ y ↔ -x ≡ -y.
This probably has suboptimal golfing! I'm unsure myself of further ways to improve this, but this proof looks very golfable!