feat(*): use `ordered_sub` instead of `nat.sub` lemmas (#9855)
* For all `nat.sub` lemmas in core, prefer to use the `has_ordered_sub` version.
* Most lemmas have an identical version for `has_ordered_sub`. In some cases we only have the symmetric version.
* Make arguments to `tsub_add_eq_tsub_tsub` and `tsub_add_eq_tsub_tsub_swap` explicit
* Rename `add_tsub_add_right_eq_tsub -> add_tsub_add_eq_tsub_right` (for consistency with the `_left` version)
* Rename `sub_mul' -> tsub_mul` and `mul_sub' -> mul_tsub` (these were forgotten in #9793)
* Many of the fixes are to fix the identification of `n < m` and `n.succ \le m`.
* Add projection notation `h.nat_succ_le` for `nat.succ_le_of_lt h`.
