| Metric | Count |
|---|
DefinitionsevalIntCeil, evalIntFloor, evalNatCeil | 3 |
Theoremsabs_fract, abs_one_sub_fract, abs_sub_lt_one_of_floor_eq_floor, add_one_le_ceil_iff, cast_mul_floor_div_cancel_of_pos, ceil_add_ceil_le, ceil_add_intCast, ceil_add_le, ceil_add_natCast, ceil_add_ofNat, ceil_add_one, ceil_congr, ceil_div_ceil_inv_sub_one, ceil_eq_add_one_sub_fract, ceil_eq_floor_add_one_iff_notMem, ceil_eq_iff, ceil_eq_on_Ioc, ceil_eq_on_Ioc', ceil_eq_self_iff_mem, ceil_eq_zero_iff, ceil_intCast, ceil_intCast_add, ceil_le_ceil, ceil_le_floor_add_one, ceil_le_mul, ceil_le_two_mul, ceil_lt_add_one, ceil_lt_iff, ceil_lt_mul, ceil_lt_two_mul, ceil_mono, ceil_natCast, ceil_natCast_add, ceil_neg, ceil_nonneg_of_neg_one_lt, ceil_ofNat, ceil_ofNat_add, ceil_one, ceil_one_add, ceil_sub_intCast, ceil_sub_natCast, ceil_sub_ofNat, ceil_sub_one, ceil_sub_self_eq, ceil_zero, div_two_lt_floor, floor_add_fract, floor_add_intCast, floor_add_natCast, floor_add_ofNat, floor_add_one, floor_congr, floor_div_cast_of_nonneg, floor_div_natCast, floor_eq_iff, floor_eq_on_Ico, floor_eq_on_Ico', floor_eq_self_iff_mem, floor_eq_zero_iff, floor_fract, floor_intCast, floor_intCast_add, floor_le_ceil, floor_le_floor, floor_le_iff, floor_le_neg_one_iff, floor_le_sub_one_iff, floor_lt_ceil_of_lt, floor_lt_self_iff, floor_mono, floor_natCast, floor_natCast_add, floor_neg, floor_ofNat, floor_ofNat_add, floor_one, floor_pos, floor_sub_intCast, floor_sub_natCast, floor_sub_ofNat, floor_sub_one, floor_zero, fract_add, fract_add_floor, fract_add_fract_le, fract_add_intCast, fract_add_le, fract_add_natCast, fract_add_ofNat, fract_add_one, fract_div_intCast_eq_div_intCast_mod, fract_div_mul_self_add_zsmul_eq, fract_div_mul_self_mem_Ico, fract_div_natCast_eq_div_natCast_mod, fract_eq_fract, fract_eq_iff, fract_eq_self, fract_eq_zero_iff, fract_eq_zero_or_add_one_sub_ceil, fract_floor, fract_fract, fract_intCast, fract_intCast_add, fract_lt_one, fract_mul_natCast, fract_natCast, fract_natCast_add, fract_ne_zero_iff, fract_neg, fract_neg_eq_zero, fract_nonneg, fract_ofNat, fract_ofNat_add, fract_one, fract_one_add, fract_pos, fract_sub_intCast, fract_sub_natCast, fract_sub_ofNat, fract_sub_one, fract_sub_self, fract_zero, image_fract, le_ceil_iff, le_floor_add, le_floor_add_floor, lt_floor_add_one, lt_floor_iff, lt_succ_floor, map_ceil, map_floor, map_fract, mul_cast_floor_div_cancel_of_pos, mul_fract_eq_one_iff_exists_int, mul_lt_floor, mul_natCast_floor_div_cancel, natCast_ceil_eq_ceil, natCast_ceil_eq_ceil_of_neg_one_lt, natCast_floor_eq_floor, natCast_mul_floor_div_cancel, one_le_ceil_iff, preimage_Icc, preimage_Ici, preimage_Ico, preimage_Iic, preimage_Iio, preimage_Ioc, preimage_Ioi, preimage_Ioo, preimage_ceil_singleton, preimage_floor_singleton, preimage_fract, self_sub_floor, self_sub_fract, sub_floor_div_mul_lt, sub_floor_div_mul_nonneg, sub_one_lt_floor, int_ceil_pos, int_floor_nonneg, int_floor_nonneg_of_pos, nat_ceil_pos, ceil_lt_add_one_of_gt_neg_one, natCast_ceil_eq_intCast_ceil, natCast_ceil_eq_intCast_ceil_of_neg_one_lt, natCast_floor_eq_intCast_floor, subsingleton_floorRing | 166 |
| Total | 169 |