Entry	Value
Package Name	natural-order-thm
Count	33
Theorems	EQ_IMP_LE : !m n. m = n ==> m <= n LET_ANTISYM : !m n. ~(m <= n /\ n < m) LET_CASES : !m n. m <= n \/ n < m LET_TRANS : !m n p. m <= n /\ n < p ==> m < p LE_0 : !n. 0 <= n LE_ANTISYM : !m n. m <= n /\ n <= m <=> m = n LE_CASES : !m n. m <= n \/ n <= m LE_LT : !m n. m <= n <=> m < n \/ m = n LE_REFL : !n. n <= n LE_SUC : !m n. SUC m <= SUC n <=> m <= n LE_SUC_LT : !m n. SUC m <= n <=> m < n LE_TRANS : !m n p. m <= n /\ n <= p ==> m <= p LTE_ANTISYM : !m n. ~(m < n /\ n <= m) LTE_CASES : !m n. m < n \/ n <= m LTE_TRANS : !m n p. m < n /\ n <= p ==> m < p LT_0 : !n. 0 < SUC n LT_ANTISYM : !m n. ~(m < n /\ n < m) LT_CASES : !m n. m < n \/ n < m \/ m = n LT_IMP_LE : !m n. m < n ==> m <= n LT_IMP_NEQ : !m n. m < n ==> ~(m = n) LT_LE : !m n. m < n <=> m <= n /\ ~(m = n) LT_NZ : !n. 0 < n <=> ~(n = 0) LT_REFL : !n. ~(n < n) LT_SUC : !m n. SUC m < SUC n <=> m < n LT_SUC_LE : !m n. m < SUC n <=> m <= n LT_TRANS : !m n p. m < n /\ n < p ==> m < p NOT_LE : !m n. ~(m <= n) <=> n < m NOT_LT : !m n. ~(m < n) <=> n <= m SUC_LE : !n. n <= SUC n SUC_LT : !n. n < SUC n num_MAX : !p. (?n. p n) /\ (?m. !n. p n ==> n <= m) <=> (?m. p m /\ (!n. p n ==> n <= m)) num_WF : !p. (!n. (!m. m < n ==> p m) ==> p n) ==> (!n. p n) num_WOP : !p. (?n. p n) <=> (?n. p n /\ (!m. m < n ==> ~p m))

Back to main package page