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.
feat(library/standard/list): add many basic facts and operations
feat(library/standard): more theorems in int, more clean-up in other files

in int.lean prove more about multiplication (including |a||b|=|ab|) and less than (including totality)

Note: making argument of by_cases in kernel implicit required some changes in nat2.lean
feat(library/standard/list): add sort and other functions