feat(nat/int/kernel/subtype): Give definition of int based on quotients and make other minor changes

Minor changes in other files: Add some more theorems about tprod in kernel (and some cleanup of long lines); move some code from nat2 to nat; add thm to subtype and changed (Type U) to Type.