[Agda] built-in divMod

[Sergei Meshveliani]

Dear standard library developers,

As I understand, 
(1) the certified Nat arithmetic is exponentially slow, due to unary 
    representation,
(2) due to this, it is added a non-certified built-in arithmetic for 
    Nat, including the predicates _≡ᵇ_; _<ᵇ_ returning a Boolean result.

But is there a fast built-in  divMod  for Nat ?

For I do not see, how (2) can help with fast GCD, and hence with a fast
_rational_ number arithmetic over Nat and Integer.

In scientific computation rational numbers are used as widely as
Integer, strongly needed. 

On the other hand, a fast divMod will allow us to program in Agda a fast
gcd   and fast rational arithmetic over Nat (Integer) 
(if I am not missing something, for this is difficult to make sure
without trying to write the code).

This (divMod a b b\=0)  can, say, return  (quot , rem) : Nat x Nat,
and the proofs for 
               T (a ≡ᵇ a * quot + rem),   T (rem <ᵇ b)  

can be postulated in the library.
As many non-certified things for Nat are already included, why do not
add built-in  divMod ?  I hope this will be the last one.
Probably it is somewhere in the  gmp  library (used in GHC ?).  

Am I missing something?

------
Sergei