module cmp where

open import Data.Nat
open import Data.Nat.Properties as NatProp -- <-cmp
open import Relation.Binary

compare_test : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$!
compare_test x y with <-cmp x y
... | tri< a !$\neg$!b !$\neg$!c = y
... | tri!$\approx$! !$\neg$!a b !$\neg$!c = x
... | tri> !$\neg$!a !$\neg$!b c = x

-- test = compare_test 7 2
-- 7