[Agda] simple example

[Serge D. Mechveliani]

People,
can you, please, answer a couple of beginner questions?

The function  rem  needs to evaluate the remainder of division of 
natural numbers  n by m  by repeatedly subtracting  m  from the current 
remainder.
The restriction  IsPositive m  is also processed.
The cost optimizations are ignored.
It uses Standard Library 0.6.
Math symbols used:  \bn, \.-

---------------------------------------------------------
module MyLib where
open import Foreign.Haskell
open import IO.Primitive
open import Data.Bool as Bool
open import Data.Nat as Nat hiding (less)
open import Prelude using (toCostring)

less : Б└∙ -> Б└∙ -> Bool              -- \bn for Nat
less zero    zero    = false
less zero    (suc _) = true
less (suc _) zero    = false
less (suc n) (suc m) = less n m

IsPositive : Б└∙ -> Set
IsPositive zero    = T false
IsPositive (suc _) = T true

rem : Б└∙ -> (m : Б└∙) -> IsPositive m -> Б└∙
rem zero    _       _ =  zero
rem (suc n) (suc k) p =  if less n k then  suc n  
                         else              rem (n Б┬╦ k) (suc k) p 
                                           -- \.-  for subtraction on Nat
rem _       zero  ()  -- unaccessible

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


1. If I skip the last sentence in  rem,  the compiler reports

  ... Missing cases:  rem (suc _) zero _  ...

Why cannot it derive from  `IsPositive m'  the fact that  m = zero  
is not possible?

2. For the initial program, the compiler reports

  Termination checking failed for the following functions:  rem
  Problematic calls:          rem (n Б┬╦ k) (suc k) p    
  -- \.-  for subtraction
 
How to fix this? 
May be, one needs to provide a proof for   n Б┬╦ k < n  ? 
                                           (\.-  for subtraction)
(if so, in what form can it be provided?).
May be, Standard library already has such a proof, and it can be 
somehow imported? 

3. It is natural to rely on the library.
   What and how need I to use here from Standard Library 0.6 instead 
   of the above definitions for  less  and  IsPositive ?

Thank you in advance for explanation,

------
Sergei