factorials and binomials simplification - nusum less verbose

Thankyou Richard and Robert, you answered completely to my questions.

>matchdeclare([a,b],true);
>defrule(h,binomial(a,b),(a+b)!/a!/b!);
>apply1(?, h);
>minfactorial(%);
    >will simplify the example you give, 

Just for the sake of understanding:

matchdeclare([a,b],true);

This command makes Maxima able to apply the following rule

defrule(h,binomial(a,b),(a+b)!/a!/b!);

wherever it finds something like "binomial(n,k)", whatever the domain of n and k is, isn't it?

>> I'd like to avoid the string "Dependent equations eliminated:  (1)".
>From looking at the code from which that message originates >(src/solve.lisp),
>it appears that linsolvewarn : false; should disable that message.
>I didn't try that.

Yes, the command 
linsolvewarn:false
makes the linear solver silent, and it's what I want.

>> I'm using Maxima within the theorem prover Hol Light, through an >>interface
>> written by John Harrison.

>Hmm, that sounds interesting. Maybe you can tell us more about this.

A theorem prover, like Hol Light, is (roughly speaking) a programming language in wich the code you write is a mathematical proof. If the code runs, the proof was correct and you get a theorem (if you agree with the Hol axioms!).
But it cannot find any result by itself, it can only check if a result is correct (producing a formal proof of it).
So it's very different from a Computer Algebra System, wich can find the answers, but without giving the proofs.
A very interesting mix is ask Maxima for the answers, and then check them by Hol to get formal theorems.
I was encouraged to this approach by the last chapter of the Hol Tutorial (page 206), http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf , were I found the interface I'm using.

Thankyou again.

Giovanni Gherdovich