[Agda] divMod variant

[Serge D. Mechveliani]

People,
the archive  http://botik.ru/pub/local/Mechveliani/agdaNotes/ddivRem.zip
contains 
* the implementation  DDivRem.agda  for division with remainder for   
  unary coded natural numbers,
* the test module  Main.agd,
* notes  notes.agda  and questions on this program 

-- all this is for  Agda-2.3.0.1 + lib-0.6.  

Instead of
  data DivMod : Nat -> Nat -> Set where
    result : {divisor : Nat} (q : Nat) (r : Fin divisor) ->
             DivMod (toNat r + q * divisor) divisor
of Standard
divRem  has the result type

  record NatDivRem (dividend divisor : Nat) : Set where   
    field
      quot  : Nat   
      rem   : Nat
      proof : (rem < divisor) x (dividend == (quot * divisor + rem)) 

  natDivRem : (dividend : Nat)     -> (divisor : Nat) -> 
              False (divisor =? 0) -> NatDivRem dividend divisor

(For this letter I denote  \bn ->  Nat,  \equiv ->  ==,   \=? ->  =? ). 

It also builds the needed proofs.
In its internal loop, it processes the additional arguments for
* the counter for subtractions, in order to help the termination proof,
* the current proof for   m == (q * n' + r),  in order to provide an
  incremental proof, to save the cost.

I shall be grateful to you if you look into (a quite small code in) 
DDivRem.agda  and give notes.  
The mark  `debug'  in comments points at questionable places.

I tried  divRem m 5   for several values of  m  (see Main.agda).
I understand that
* probably,  Agda-2.3.0.1 + lib-0.6  does not at all aim at performance,
* unary coded naturals  is not an appropriate test for investigating  
  the performance points;
  I think, say, sorting a long character list fits better.

Still consider the following.
1. The time cost in  divRem  looks like  O(m^2).
2. The version "-skipProofs" has the same timing.
   Why does it look as  O(m^2) ?
   A short comment in  notes.agda  argues for that it must be  O(m).

Thanks,

------
Sergei