_-_ : Nat @$\rightarrow$@ Nat @$\rightarrow$@ Nat
n     - zero = n      -- "n - zero" have 2-pattern, "zero - zero" "suc n - zero"
zero  - suc m = zero
suc n - suc m = n - m