I am trying to write an integer division function from scratch in agda2 (as of 2.6.3):

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_∸_ : ℕ → ℕ → ℕ
_∸_ m n = {}0

div : ℕ → ℕ → ℕ
div m n with m ∸ n 
...     | 0  = 0
...     | x = suc (div x n)

The basic idea is to use the monus function ∸ (integer minus) to subtract n from m until the difference is zero. But when loading the file, there is an error:

Termination checking failed for the following functions:
  div
Problematic calls:
  div m n | m ∸ n
  div x n

I can see that the error happens because agda has no way to tell if the monus function is decreasing until it reaches zero (i.e. m ∸ n < m unless m is 0).

My questions are:

1. How do I provide a proof to agda that m ∸ n is less than m, and the recursion is decreasing on the first argument?

2. Is it OK if the argument is decreasing only before reaching the base case (zero here)?

Note: I looked at the documentation, which only says that one can use the following pragmas to basically ignore the termination check.

TERMINATING and NON_TERMINATING

But I'd like to provide a proof rather than dictate to agda that monus is decreasing (since what the human asserts could be wrong).