Fixed natToMod and implemented group-action-based modular arithmetic.

natToMod was not defined correctly in the previous commit. It would
produce the wrong result in cases where the argument wrapped the modulus
like `the (Mod 3) (natToMod 4)`. Now it works.

Implemented rotate which is equivalent to (+ (mS mZ)). Then defined
`modplus` in terms of successive rotations, recursive in the first argument,
to mimic Nat's first-argument recursion.
Merge branch 'master' of github.com:esmooov/idris-crypto