Commit 2023-01-06 07:14 0411b857

View on Github →

feat: a.nat_mod b < b (#1340) Match https://github.com/leanprover-community/mathlib/pull/17896

Estimated changes

added theorem Int.natMod_lt
added theorem Int.toNat_lt'
added def Int.natMod