Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

(0)! = 1

Applied Tactic: RecCaseSplit `factorial` THEN Auto
Generated subgoals:

None