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