Commit 2023-10-23 02:56 49b7459e
View on Github →feat: add gcongr lemmas for Nat.floor, Nat.ceil, Int.floor, Int.ceil (#7811)
The lemmas are just restatements of lemmas of the form Monotone Nat.floor etc, but these cannot be tagged directly with the gcongr attribute.