module lessnat2 where


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


data ⊤ : Set where
  true : ⊤ 

data ⊥ : Set where


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