Theoremsabs_ceil_sub_le, abs_floor_sub_le, abs_sub_ceil_le, abs_sub_floor_le, add_one_le_ceil_iff, cast_mul_floor_div_cancel, ceil_add_le, ceil_add_natCast, ceil_add_ofNat, ceil_add_one, ceil_congr, ceil_eq_iff, ceil_eq_zero, ceil_intCast, ceil_le_ceil, ceil_le_floor_add_one, ceil_lt_add_one, ceil_mono, ceil_natCast, ceil_ofNat, ceil_one, ceil_sub_natCast, ceil_sub_ofNat, ceil_sub_one, ceil_zero, floor_add_natCast, floor_add_ofNat, floor_add_one, floor_congr, floor_eq_iff, floor_eq_iff', floor_eq_on_Ico, floor_eq_on_Ico', floor_eq_zero, floor_le, floor_le_ceil, floor_le_floor, floor_le_of_le, floor_le_one_of_le_one, floor_lt, floor_lt', floor_lt_ceil_of_lt_of_pos, floor_lt_one, floor_mono, floor_natCast, floor_ofNat, floor_of_nonpos, floor_one, floor_pos, floor_sub_natCast, floor_sub_ofNat, floor_sub_one, floor_zero, le_ceil, le_floor_iff', le_of_ceil_le, lt_floor_add_one, lt_of_ceil_lt, lt_of_floor_lt, lt_of_lt_floor, lt_one_of_floor_lt_one, lt_succ_floor, map_ceil, map_floor, mul_cast_floor_div_cancel, one_le_ceil_iff, one_le_floor_iff, pos_of_floor_pos, preimage_Icc, preimage_Ici, preimage_Ico, preimage_Iic, preimage_Iio, preimage_Ioc, preimage_Ioi, preimage_Ioo, preimage_ceil_of_ne_zero, preimage_ceil_zero, preimage_floor_of_ne_zero, preimage_floor_zero, sub_one_lt_floor, subsingleton_floorSemiring | 82 |