[Agda] [BUG] builtins strike again -- Nat is a ring?

[James Deikun]

I know this one isn't currently used in the standard library, but I was
poking around the defined builtins and primitives in my FastNat work and
I discovered this short proof of false:

module Test where
  open import Data.Nat
  open import Data.Empty
  open import Relation.Binary.PropositionalEquality

  0≢1+n : ∀ {n} -> 0 ≢ suc n
  0≢1+n ()

  divSucAux : (k m n j : ℕ) -> ℕ
  divSucAux k m zero j = k
  divSucAux k m (suc n) zero = divSucAux (suc k) m n m
  divSucAux k m (suc n) (suc j) = divSucAux k m n j
  {-# BUILTIN NATDIVSUCAUX divSucAux #-}

  oh-noes : ⊥
  oh-noes = 0≢1+n {divSucAux 0 0 0 1} refl

Probably an easy fix, just a retool of the fast path for NATDIVSUCAUX to
never return anything less than k.