Commit 2024-09-05 00:27 2d7e178e

View on Github →

feat: Register more @[bound] lemmas for floor, ceil, and log (#16039) Int.ceil_lt_add_one and Real.log_pos came up in https://github.com/girving/ray, and I've registered a variety of nearby lemmas.

Estimated changes

modified theorem Int.ceil_le_ceil
modified theorem Int.floor_le_floor
modified theorem Nat.ceil_le_ceil
modified theorem Nat.floor_le_floor