_-_ :ℕ →ℕ →ℕ
x - zero  = x
zero - _  = zero
(suc x) - (suc y)  = x - y