The Coq mailing list

[satrajit AT attbi.com]

Say I have proved theorems a and b and have to prove theorem c using a and b, 
something like:

Section mySection.

Theorem a:...
Proof.
.
.
Qed.

Theorem b:...
Proof.
.
.
Qed.

Theorem c:....
Proof.
.
.
Need to use theorems a and b here so that at the appropriate stage in the  
proof, Auto would simply make use of theorems a and b that have been proved 
already.
.
.
Qed.

End mySection.

Is this possible in Coq?
If yes, what is the general procedure to accomplish this in Coq 7.3?

Thanks in anticipation.