Symbolic `+` and `-` on `Z n` reduce mod `n` when arguments are concrete.
Symbolic `+` and `-` on `Z n` reduce mod `n` when arguments are concrete.

Fixes #554.

GaloisInc/cryptol,GaloisInc/cryptol,GaloisInc/cryptol