mathlib3
194bde8f - feat(order/monotone): add `monotone_int_of_le_succ` etc (#10895)

Commit

4 years ago

feat(order/monotone): add `monotone_int_of_le_succ` etc (#10895) Also use new lemmas to golf `zpow_strict_mono` and prove `zpow_strict_anti`.

Author

urkud

Parents