feat(nat): add minus, prove theorems about it
minus is needed to define addition for integers
feat(nat) remove redundant comment
feat(int): start on integers file
define integers, addition. int.lean is an old version, int2.lean is a new try which works better
int2.lean fails to compile when L169 is uncommented