[Agda] Int/(m) test

[Sergei Meshveliani]

Agda is great!

It
1) understands mathematical notions (things can be written adequately), 
2) checks proofs,
3) performs fast algorithms which also carry proofs.

I have tested it on arithmetic of  Integer/(m)  (including partial
division), with all proofs provided.

It is by defining a general Euclidean ring E, its residue E/(base)
(and all the previous class hierarchy), 
and then, by taking the instance for  E = Integer.

For  1 < m < 20  it did all possible divisions  x / y  in  Integer/(m),
and also checked  x^m  (binary method).

The test is practical. It consists of many operations involving only
small integers (|x| < m < 20). So that the unary representation does not
bring much cost overhead.

(For any occasion:  
Agda of February 5, 2014  checks my examples much faster than 
Agda of January 26).

Regards,

------
Sergei