_-_ :@$\mathbb{N}$@ @$\rightarrow$@@$\mathbb{N}$@ @$\rightarrow$@@$\mathbb{N}$@
x - zero  = x
zero - _  = zero
(suc x) - (suc y)  = x - y