feat(nat/int/kernel): Prove more theorems about sub in nat; prove that int is a quotient

Add pair extensionality to kernel
Add to nat a lot of theorems with interaction between sub and le
Add to int more properties about the defining relations/functions for int