_+_ : ℕ → ℕ → ℕ
zero  + m = m
suc n + m = suc (n + m)