Entry	Value
Package Name	natural-order-def
Count	6
Theorems	GE : !m n. m >= n <=> n <= m GT : !m n. m > n <=> n < m LE_ZERO : !m. m <= 0 <=> m = 0 LT_ZERO : !m. ~(m < 0) NO_NAME : !m n. m < SUC n <=> m = n \/ m < n NO_NAME : !m n. m <= SUC n <=> m = SUC n \/ m <= n

Back to main package page