Commit 2026-05-10 00:45 d8cbbf99

View on Github →

feat(Order/SuccPred/LinearLocallyFinite): StrictMono toZ (#39014) We prove that toZ is strictly monotonic, and golf/deprecate other theorems in this file using this.

Estimated changes

deleted theorem le_of_toZ_le
added theorem toZ_inj
deleted theorem toZ_le_iff
added theorem toZ_le_toZ
added theorem toZ_lt_toZ
deleted theorem toZ_mono
added theorem toZ_strictMono