[Agda] interactive Bin arith performance

[Sergei Meshveliani]

On Thu, 2019-01-31 at 12:13 +0100, Ulf Norell wrote:
> Without looking at the code my guess would be that you are strict in
> the proof objects. At runtime (after compilation) the proof objects
> are erased and not evaluated, but at compile time you evaluate the
> generated proofs, causing the terrible performance.
> 

This is about a certain divMod for a certain representation for Bin.

The result data  DivMod  includes two proofs, and is evaluated
recursively.
And this probably gives a great overhead of proof objects in evaluation
in the interpreter.

Probably, I can reorganize  divMod  to  divMod'  to return only a pair  
(quotient , remainder),
and then add an Agda proof for the two properties of the result:
a = quotient * b + remainder,   remainder < b.

May be this will not be a good style, but this will remove evaluating
proof objects in interpreting of
                                divMod' a b b/=0. 
Right?

Thanks,

------
Sergei