Entry	Value
Package Name	natural-add-sub-thm
Count	16
Theorems	ADD_SUB2 : !m n. (m + n) - m = n SUB1 : !n. ~(n = 0) ==> PRE n = n - 1 SUB_0 : !m. m - 0 = m SUB_ADD : !m n. n <= m ==> m - n + n = m SUB_ADD2 : !m n. n <= m ==> n + m - n = m SUB_ADD_LCANCEL : !m n p. p <= n ==> (m + n) - (m + p) = n - p SUB_ADD_RCANCEL : !m n p. n <= m ==> (m + p) - (n + p) = m - n SUB_EQ_0 : !m n. n <= m ==> (m - n = 0 <=> m = n) SUB_PRESUC : !m n. n <= m ==> PRE (SUC m - n) = m - n SUB_REFL : !n. n - n = 0 SUB_SUB : !m n p. n + p <= m ==> m - (n + p) = m - n - p SUB_SUC : !m n. n <= m ==> SUC m - SUC n = m - n SUB_SUC_CANCEL : !m n. n < m ==> SUC (m - SUC n) = m - n SUB_SUC_PRE : !m n. n < m ==> m - SUC n = PRE (m - n) SUC_SUB : !m n. n <= m ==> SUC (m - n) = SUC m - n SUC_SUB1 : !n. SUC n - 1 = n

Back to main package page