Both "nusum" and "Gosper" do in this case,
but the package "Zeilberger" does much more.
For example:
- It implements Zeilberger's algorithm
(for example: sum_k=0^n binomial(n,k))
- It writes formal proves for the identities found
by itself (and it tests the proof)
------------EXAMPLE--------------------------
%i30) res : parGosper(binomial(n,k),k,n,1);
k
(%o30) [[---------, [2, - 1]]]
n - k + 1
(%i31) zb_prove_detail:PROOF_HIGH;
(%o31) 3
(%i32) zb_prove(binomial(n,k),k,n,res);
The result contains one recurrence for binomial(n, k) :
2 binomial(n, k) - binomial(n + 1, k) =
(k + 1) binomial(n, k + 1) k binomial(n, k)
-------------------------- - ---------------- ;
n - k n - k + 1
which we can prove by dividing both members of the equality by binomial(n, k)
and checking the resulting equality between rational functions.
Namely it is equivalent to test the equality between:
n + 1 k
2 - --------- and 1 - ---------
n - k + 1 n - k + 1
(%o32) true
-------------------------------------------------------------
Regards
Fabrizio