Add inductive integers

This is inspired by Agda's integers. An integer is defined as a positive Nat
or the negative successor of a Nat, yielding unique 0 and fairly convenient
definitions of operations.