Commit 2024-09-24 12:27 a6954b37

View on Github →

chore(Order/Group): golf (#17079) ... using lemmas like monotone_int_of_le_succ

Estimated changes

modified theorem zpow_mono_right
modified theorem zpow_right_strictAnti
modified theorem zpow_right_strictMono