The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 04/05/2013 04:14 PM, Jonas Oberhauser wrote:

The main problem is, as Mr. Chlipala mentioned, hat 10! is just a very large number.

I believe, however, that you don't actually need to fully beta-reduce the term in question.
Probably unfold does what you want:


Goal fact 10 = 10 * fact 9.
unfold fact. reflexivity. Qed.

If you're going to go that route, you can also just write [reflexivity] on its own to prove the goal.  It only takes about a second for me.