feat(library/standard): Prove more theorems in nat and int

Prove more theorems in nat about sub and dist, including triangle inequality.
In int, use the simplifier much more, and prove more theorems about mul.

Note: change of theorem name also made an edit in nat2 necessary.