module monotoneless1 where

data ℕ : Set where
  Z : ℕ 
  S : ℕ -> ℕ 

data ⊤ : Set where
  true : ⊤

data ⊥ : Set where

_<_ : ℕ -> ℕ -> Set
_   < Z   = ⊥ 
Z   < S _ = ⊤ 
S n < S m = n < m

infixl 10 _<_ 


_+_ : ℕ -> ℕ ->  ℕ
n + Z   = n
n + S m = S (n + m)

infixl 20 _+_ 


mono : (n m k : ℕ) -> n < m -> n + k < m + k
mono n     m      Z      nm   = nm
mono n     m      (S k)  nm   = mono n m k nm