_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)