feat(nat): add minus, prove theorems about it
minus is needed to define addition for integers
feat(nat) remove redundant comment