Commit 2023-07-31 15:32 b6d0a69c
View on Github →feat: a + a = 0 ↔ a = 0 in ZMod n for n odd (#6086)
This PR proves that a + a = 0 ↔ a = 0, and uses it to golf the proof of ne_neg_self.
feat: a + a = 0 ↔ a = 0 in ZMod n for n odd (#6086)
This PR proves that a + a = 0 ↔ a = 0, and uses it to golf the proof of ne_neg_self.