feat(measure_theory): `int.floor` etc are measurable (#10265)
## API changes
### `algebra/order/archimedean`
* rename `rat.cast_floor` to `rat.floor_cast` to reflect the order of operations;
* same for `rat.cast_ceil` and `rat.cast_round`;
* add `rat.cast_fract`.
### `algebra/order/floor`
* add `@[simp]` to `nat.floor_eq_zero`;
* add `nat.floor_eq_iff'`, `nat.preimage_floor_zero`, and `nat.preimage_floor_of_ne_zero`;
* add `nat.ceil_eq_iff`, `nat.preimage_ceil_zero`, and `nat.preimage_ceil_of_ne_zero`;
* add `int.preimage_floor_singleton`;
* add `int.self_sub_floor`, `int.fract_int_add`, `int.preimage_fract`, `int.image_fract`;
* add `int.preimage_ceil_singleton`.
### `measure_theory/function/floor`
New file. Prove that the functions defined in `algebra.order.floor` are measurable.
