[Agda] record with proof

[Serge D. Mechveliani]

People,
can you, please, answer my questions on the following simple program? 
I am trying to understand usage of Agda by programming the  division 
remainder  for natural numbers (of Nat -- Б└∙).
(This is under  Agda-2.3.0.1 + Standard library lib-0.6).
So far, I ignore  Data.Nat.DivMod,  because it is rather difficult to
understand, and I try to begin with a simpler, home-made approach.

remainder n m,  m > 0,   is found by repeated subtraction of m from the 
                                              current remainder.
1. remNat  finds the remainder all right.
   It uses an auxiliary function  rem  which processes an additional 
argument for the  counter  - the number of subtractions applied.
The counter is used in order to make a termination proof trivial.

2. remNatP  is a variant of  remNat  with producing a proof for  
                                                      "remainder < m".
Its idea is to provide a recursive proof together with a recursive 
evaluation of the remainder. As there are the two result values, I
introduce the  record  Rem m  with the two fields. The second field is
for a proof, its type depends on  m  and on the value of the remainder 
field  r. 
And  remNatP  is not compiled. I wonder, what is wrong there?

-------------------------------------------------------------------
module MyLib where
open import Foreign.Haskell
open import IO.Primitive
open import Relation.Nullary.Core
open import Data.Bool as Bool
open import Data.String as String
open import Data.Nat as Nat
open import Data.Nat.Show  
open import Prelude using (toCostring) 

lessNat? : Б└∙ -> Б└∙ -> Bool       
lessNat? 0       0       = false
lessNat? 0       (suc _) = true
lessNat? (suc _) 0       = false
lessNat? (suc n) (suc m) = lessNat? n m

LessNat? : Б└∙ -> Б└∙ -> Set
LessNat? n m = T (lessNat? n m)

PositiveNat? : Б└∙ -> Set
PositiveNat? 0 = T false
PositiveNat? _ = T true

remNat : Б└∙ -> (m : Б└∙) -> PositiveNat? m -> Б└∙
remNat _ 0 ()   -- unaccessible
remNat n m _ =  rem n n            -- below  m  is a constant subtrahend
  where
  rem : Б└∙ -> Б└∙ -> Б└∙                -- н╩ n counter -> r,  counter  is the
                                   -- number of subtractions applied
  rem 0 _         = 0
  rem n 0         = 0                -- accessible only for  m = 1
  rem n (suc cnt) = if lessNat? n m then  n  
                    else                  rem (n Б┬╦ m) cnt 

record Rem (m : Б└∙) : Set where   
       field
         r          : Б└∙
         boundProof : LessNat? r m

remNatP : Б└∙ -> (m : Б└∙) -> PositiveNat? m -> Rem m
remNatP _ 0       ()    -- unaccessible
remNatP n (suc k) _  =  rem n n  
  where                           -- below  m'  is a constant subtrahend
  m' = suc k
  rem : Б└∙ -> Б└∙ -> Rem m'               -- н╩ n counter -> remainder by m'
  rem 0 _         = record{ r = 0;  boundProof = _ }
  rem _ 0         = record{ r = 0;  boundProof = _ }
                                          -- accessible only for  m' = 1
  rem n (suc cnt) =  
        -- (1)
        if lessNat? n m' then  record{ r = n;  boundProof = _ } 
        else                   rem (n Б┬╦ m') cnt 

{- (3)
        if not (lessNat? n m') then  rem (n Б┬╦ m') cnt 
        else
        record{ r = n;  boundProof = p } 
                                     where
                                     p : LessNat? n m'
                                     p = _
                -- Unsolved metas at the following locations:  `p = _' 
-}

{- (4)
          if lessNat? n m' then ( record{ r = n;  boundProof = p } 
                                  where
                                  p : LessNat? n m'
                                  p = _
                                )
          else  rem (n Б┬╦ m') cnt 
                           -- Parse error   where<ERROR> ...
-}

main : IO Unit
main = putStrLn (toCostring "done")
-------------------------------------------------------------------

3. About
   record Rem (m : Б└∙) : Set where   
          field
            r          : Б└∙
            boundProof : LessNat? r m
:
I thought that a function cannot return a value of this type other than 
providing a proof for  LessNat? r m
(?)
I do not know, may be, I am missing something about dependent records. 

4. The variant (1) in  rem  yields
   "Unsolved metas at the following locations:" 
for the line of  `record ...'.
Why?
In the branch of   lessNat? n m',  the condition for  boundProof  is 
trivially satisfied, so, I put  record{ r = n;  boundProof = _ }
-- ?

5. Setting here  `r = 0'  instead of  `r = n'  makes it compiled.
   But this function expresses the constant of  0,  not the remainder.

6. The variant (3) uses the construct of  
       record{ r = n;  boundProof = p } 
                                     where
                                     p : LessNat? n m'
                                     p = _
It yields, again,
   "Unsolved metas at the following locations:"  for  `p = _'.

7. The variant (4) only transposes the branches of (3) in  if-then-else
   into a more natural order.
   But the report is different:
                                "Parse error   where<ERROR> ..."

Can you comment, please? How to fix the program?
Thank you in advance for explanation,

------
Sergei