Entry	Value
Package Name	natural-factorial-def
Count	2
Theorems	FACT_SUC : !n. FACT (SUC n) = SUC n * FACT n FACT_ZERO : FACT 0 = 1

Back to main package page