[Agda] _divMod_

[Serge D. Mechveliani]

People,
I have a question on  Nat.DivMod  of Standard library   
                                     (of Agda-2.3.0.1, lib-0.6):
need to study how to use _divMod_.
Nat.DivMod  has an example of such usage: the function  _mod_. 
I copy the  _mod_  definition from  Nat.DivMod  to my module  Main.agda
with changing the identifiers as
                  _mod_ -> mod2,  \?= -> eq?,  \nequiv 0 -> p 
(see the _mod_ code in  Nat/DivMod.agda):
----------------
mod2 : (dividend divisor : Nat) {p : False (divisor eq? 0)} -> Fin divisor
mod2 m n {p} with _divMod_ m n {p}
.(toNat r + q * n) mod n | result q r = r
----------------

-- for this email, I write  Nat for \bn,  eq? for \?= ,  
in order to avoid problems with math symbols in email. 

The report is:  "Missing with-clauses for function mod2".

(1) Nat.DivMod.agda  is compiled, and  Main.agda  is not: 
    can you explain this effect?

I thought, probably, the last line applies a _view_, similar as the 
User Guide explains in Section `3.1 Views'.
At the moment, I do not understand `views'. But I look into the Guide 
example of Parity and `parity' in this section, and just try to mimic 
it. I change the implementation to  
--------------
mod2 m n {p} with _divMod_ m n {p}
mod2 .(toNat r + q * n) n | result q r = r 
--------------
(the second line has two arguments before `|', instead of the three 
arguments in Nat/DivMod).
I do not know of _what_ this computes, but at least it is compiled.
I wonder what all this story may be about.

(2) Why it is chosen a name  _divMod_  having two underscores? 
    It is not declared as infix.

(3) My beginner's attempt of  divMod  might be like this: 

  record MyDivMod (dividend divisor : Б└∙) : Set
         where
         field
           quot  : Б└∙
           rem   : Fin divisor
           proof : (dividend  Б┴║  quot * divisor + (toБ└∙ rem))

  myDivMod : (n : Б└∙) -> (m : Б└∙) -> False (m Б┴÷ 0) -> MyDivMod n m
  myDivMod n m p = ...

Will this approach work?
May be  _divMod_  is better, this needs studying;
and so far, I only try to  apply _divMod_.

Thank you in advance for explanation,

------
Sergei