I feel the need to be inflamatory:
I believe n+k should go.
There are lots of good reasons why they should go, of course. The question
is: are there any good reasons why they should stay? My understanding is
that the only reason they are advocated is that they make teaching
induction easier. I don't believe it. I teach an introductory FP course
including induction. I introduce structural induction directly, and the
students have no problem with it. When I have tried to talk to individuals
about natural number induction using (n+k) patterns, then the problems
start. Because they are so unlike the form of patterns they have become
used to they find all sorts of difficulties. What if n is negative. Ah yes,
well it can't be. Why not. It just can't. etc.
Let's throw them out.
John.