Entry	Value
Package Name	natural-factorial-thm
Count	2
Theorems	FACT_MONO : !m n. m <= n ==> FACT m <= FACT n FACT_NZ : !n. ~(FACT n = 0)

Back to main package page