chore(data/nat/basic): drop some `nat`-specific lemmas (#17400)
* Drop `nat.mul_left_inj`, `nat.mul_right_inj`, `nat.mul_left_injective`, and `nat.mul_right_injective`. Use general `cancel_monoid_with_zero` lemmas instead.
* Fix proofs broken by this API change.
* Assume `≠ 0` instead of `0 <` in `nat.div_div_self`.
