[Agda] Nat.DivMod details in lib-0.7

[Sergei Meshveliani]

People,
I have the following suggestions/questions on  Nat.DivMod._divMod_  of
the lib-0.7 standard library
(minor ones, though).


1. May be it has sense to add this lemma to  record DivMod :

   dividesIff :  (remainder ≡ Fin.zero)  iff  (divisor | dividend)

-- probably, it can be derived from other three fields.
I expect the `->' part to be trivial, and the `<-' part to be not so
trivial.
I think that the latter implication is usable, because it relates the
remainder to divisibility.

2. Why not require  divisor ≢ 0
   instead of       False (divisor ≟ 0)
   ?
The former condition looks simpler to use.
For example, having  n≢0 : n ≢ 0,  I need to write

    n/=0 = Decid.fromWitnessFalse {Q = (n ≟ 0)} n≢0

in order to use                _divMod_ m n {n/=0}.
And this complicates the code.

Regards,

------
Sergei