feat(data/int): absolute values and integers (#9028)
We prove that an absolute value maps all `units ℤ` to `1`.
I added a new file since there is no neat place in the import hierarchy where this fit (the meet of `algebra.algebra.basic` and `data.int.cast`).
