Commit 2022-10-26 21:53 ad7dca6a

View on Github →

feat(algebra/order/floor): some nat.ceil lemmas (#16987) mostly for feature completeness with the int version nat.ceil_coe is renamed to nat.ceil_nat_cast to match the int version

Estimated changes

Modified src/algebra/order/floor.lean

added theorem nat.add_one_le_ceil_iff

deleted theorem nat.ceil_coe

added theorem nat.ceil_int_cast

added theorem nat.ceil_le_floor_add_one

added theorem nat.ceil_nat_cast

modified theorem nat.ceil_one

modified theorem nat.ceil_zero

added theorem nat.one_le_ceil_iff

Modified src/data/int/log.lean