n+k not ``considered harmful''

You have a basic type of natural numbers.
data Nat = Zero | Succ Nat
You can pattern match on them.
f (Succ (Succ (Succ n))) = n `times` (Succ (Succ (Succ Zero)))
That pattern ensures that the parameter is >= 3.
You have syntactic sugar for natural numbers.
data Nat = 0 | 1 | 2 | ...
How would you write f more simply?
f (n+3) = n * 3
Thus n+k is just pattern matching on pure naturals, proving that n+k is not harmful.

succ my dicc

Wrong. Haskell does not and can not have a basic type of natural numbers. All the types are pointed and hence no inductive reasoning is possible.