The undercurrent where he's trying to expand the accepted definition of "by trivial algebra" is interesting. Essentially Zeilberger argues that if you can plug something in to Mathematica and it can solve it, then it's true "by trivial algebra" by today's standards, and we should stop bothering to prove such results by hand.