[Agda] is divMod slow?

[Sergei Meshveliani]

Dear Standard library developers,

I test  
       (suc n) mod (suc (suc n))
       where
       mod = Data.Nat.DivMod.mod

for  n = 123456789.

The result is correct (and trivial), but it takes   ** 6 seconds **   
on a 3 GHz machine.
It is written in  Data.Nat.DivMod that _mod_ is implemented via
Agda.Builtin.Nat.mod-helper.

Probably, this means that it relies on something like `mod' of Haskell
standard library implemented in GHC.
But `mod' of GHC computes this in less than 0.0001 sec
(somewhat one machine command for division of two macrodigits).   

Currently the Nat arithmetic in Agda Standard library is fast because it
is via built-ins. But divMod is also of important arithmetic. 
What about  divMod ?
For example, arithmetic of rational numbers rely on gcd for Nat, and gcd
relies on mod (divMod).

What is happening there?

Regards,

------
Sergei