Entry	Value
Package Name	natural-div-def
Count	6
Theorems	DIVISION_DEF_DIV : !m n. ~(n = 0) ==> m DIV n * n + m MOD n = m DIVISION_DEF_MOD : !m n. ~(n = 0) ==> m MOD n < n EVEN_SUC : !n. EVEN (SUC n) <=> ~EVEN n EVEN_ZERO : EVEN 0 ODD_SUC : !n. ODD (SUC n) <=> ~ODD n ODD_ZERO : ~ODD 0

Back to main package page