There have been several good answers to this question, so I'm not trying to compete with them, but rather offer a peculiar angle on this problem as food for thought and potential for a useful library contribution.
I would not prove the lemma by induction. I would simply test that it holds for 0, 1, 2 and 3. The fact that those tests pass is sufficient to show that the lemma holds universally.
But how do I obtain the proof by mere testing? I need to observe that the degree of the formulae on both sides of the equation is three: the left sums over a quadratic, and summation increments degree; the right is the product of three linear forms.
Of course, the proof that degree n formulae agree everywhere if they agree on 0..n requires induction on n. It's a rather amusing exercise. The trick is to ensure that your language of formulae is closed under taking the forward difference, i.e., that given some f, you can always compute df such that for all n, f(n+1) = f(n) + df(n). (The point is that df inverts the summation operator.) Then you prove that when f has nonzero degree, df has degree one less. Now, f agrees with g on 0..n+1 if and only if f(0) = g(0) and df agrees with dg on 0..n.