[eperdew]

I wrote out quite a bit for this, but I think that the main point is that by falling back to the formalism, we see the the LHS of the implication affects our inductive hypothesis. I think this is something that is not clear if you just do "base case starting at n" style proofs."

As far as drudgery, Coq will solve the trivial cases automatically, so you'd never have to prove the n = 0 case by hand. That said, there's a reason most math is done on paper and not in Coq - there's usually an order of magnitude more detail and drudgery in a formal proof, even with automation.