In my Introduction to Proofs course, I discussed the proof the following: The cube of an integer is of the form 9k, 9k+1, or 9k+8, for some integer k. The problem is from the text I use, How to Think Like a Mathematician: A Companion to Undergraduate Mathematics
The big idea here is to to note that any integer can be written as 9q+r, q some integer, r=0,1,2,..,8. Then simply find (9q+r)^3 and examine the form of the expression of the nine different cases for r. The algebra is a bit tedious – and so Wolfram Alpha comes to the rescue in the form of the command
expand((9q+r)^3) for r from 0 to 8
The output is here:
Note that the proof itself consists of the big idea of writing an integer as a multiple of 9 with a remainder. W|A simply did the grunge work for us of expanding the polynomials and substituting the values of r. In a course such as this, W|A can be a great timesaver in doing these types of calculations and students see the value of such software as efficient helpers in solving larger problems.