An example of proving summation identities with computer

I am trying to learn how to use computers to prove identities like this one