Commit 2023-06-11 22:44 7fdd4f37
View on Github →refactor(data/nat/nth): redefine, review API (#18760)
Redefine nat.nth
in terms of already available definitions, review API, generalize some lemmas.
Also fix some typos in data/set/intervals/monotone
.