chore(data/int/basic): split file (#17342)
This splits `data.int.basic` into seven files, organised mostly by import requirements.
* `data.int.basic` only requires `algebra.ring.basic` and `data.nat.basic`
* `data.int.order` requires `data.int.basic` and also `algebra.order.ring`
* `data.int.bitwise` requires `data.int.basic` and also `data.nat.pow`
* `data.int.units` requires `data.int.order` and `algebra.group_power.order`
* `data.int.dvd` requires `data.int.order`, `data.nat.cast` and `data.nat.pow`
* `data.int.div` requires `data.int.dvd` and `algebra.ring.regular`
* `data.int.lemmas` contains the remainder, both `data.int.order` and `data.int.bitwise`, and also `data.nat.cast`.
To accommodate this I've moved the existing (but unused in mathlib) `data.int.order` to `data.int.conditionally_complete_order`.
This results in a moderate reduction of import requirements downstream, but I'm hoping to do much better in separate PRs. For now I just want to get this file organised.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
