Hello,
the standard modules are included in the Toolbox distribution, but since you point to a TLAPS directory, you appear to be interested in the proof system. The prover does not use the definitions from the standard modules for reasoning about integers, but encodes TLA+ integers into the corresponding backend theories, for example by injecting the standard sort int of SMT solvers into the universal sort used to represent TLA+ constants. In this way, we can rely on the built-in automation of backends for reasoning about integers. At this point, we do not have any lemmas about ordinary integer reasoning – although it might be useful to state and prove some theorems about non-linear integer arithmetic. However, the directory that you indicate contains the module NaturalsInduction that contains lemmas about inductive reasoning on integers (which backends do not perform automatically), including principles for defining recursive functions over integers.
Regards,