Commit 2022-01-31 14:14 bb2b58ed
View on Github →feat(data/{nat,int}/parity): add division lemmas (#11570)
Add lemmas of the form even n → n / 2 * 2 = n and odd n → n / 2 * 2 + 1 = n
feat(data/{nat,int}/parity): add division lemmas (#11570)
Add lemmas of the form even n → n / 2 * 2 = n and odd n → n / 2 * 2 + 1 = n