Entry	Value
Package Name	natural-div-thm
Count	61
Theorems	DIV_0 : !n. ~(n = 0) ==> 0 DIV n = 0 DIV_1 : !n. n DIV 1 = n DIV_ADD_MOD : !a b n. ~(n = 0) ==> ((a + b) MOD n = a MOD n + b MOD n <=> (a + b) DIV n = a DIV n + b DIV n) DIV_DIV : !m n p. ~(n * p = 0) ==> m DIV n DIV p = m DIV (n * p) DIV_EQ_0 : !m n. ~(n = 0) ==> (m DIV n = 0 <=> m < n) DIV_EQ_EXCLUSION : !a b c d. b * c < (a + 1) * d /\ a * d < (c + 1) * b ==> a DIV b = c DIV d DIV_LE : !m n. ~(n = 0) ==> m DIV n <= m DIV_LE_EXCLUSION : !a b c d. ~(b = 0) /\ b * c < (a + 1) * d ==> c DIV d <= a DIV b DIV_LT : !m n. m < n ==> m DIV n = 0 DIV_MOD : !m n p. ~(n * p = 0) ==> (m DIV n) MOD p = (m MOD (n * p)) DIV n DIV_MONO : !m n p. ~(p = 0) /\ m <= n ==> m DIV p <= n DIV p DIV_MONO2 : !m n p. ~(p = 0) /\ p <= m ==> n DIV m <= n DIV p DIV_MONO_LT : !m n p. ~(p = 0) /\ m + p <= n ==> m DIV p < n DIV p DIV_MULT : !m n. ~(m = 0) ==> (m * n) DIV m = n DIV_MULT2 : !m n p. ~(m * p = 0) ==> (m * n) DIV (m * p) = n DIV p DIV_MULT_ADD : !a b n. ~(n = 0) ==> (a * n + b) DIV n = a + b DIV n DIV_MUL_LE : !m n. n * m DIV n <= m DIV_REFL : !n. ~(n = 0) ==> n DIV n = 1 DIV_UNIQ : !m n q r. m = q * n + r /\ r < n ==> m DIV n = q EVEN_ADD : !m n. EVEN (m + n) <=> EVEN m <=> EVEN n EVEN_AND_ODD : !n. ~(EVEN n /\ ODD n) EVEN_DOUBLE : !n. EVEN (2 * n) EVEN_EXISTS : !n. EVEN n <=> (?m. n = 2 * m) EVEN_MOD : !n. EVEN n <=> n MOD 2 = 0 EVEN_MULT : !m n. EVEN (m * n) <=> EVEN m \/ EVEN n EVEN_OR_ODD : !n. EVEN n \/ ODD n EVEN_SUB : !m n. n <= m ==> (EVEN (m - n) <=> EVEN m <=> EVEN n) LE_LDIV : !a b n. ~(a = 0) /\ b <= a * n ==> b DIV a <= n LE_LDIV_EQ : !a b n. ~(a = 0) ==> (b DIV a <= n <=> b < a * (n + 1)) LE_RDIV_EQ : !a b n. ~(a = 0) ==> (n <= b DIV a <=> a * n <= b) LT_LDIV : !a b n. b < a * n ==> b DIV a < n LT_LDIV_EQ : !a b n. ~(a = 0) ==> (b DIV a < n <=> b < a * n) MOD_0 : !n. ~(n = 0) ==> 0 MOD n = 0 MOD_1 : !n. n MOD 1 = 0 MOD_ADD_MOD' : !n a b. ~(n = 0) ==> (a MOD n + b MOD n) MOD n = (a + b) MOD n MOD_EQ : !m n p q. m = n + q * p ==> m MOD p = n MOD p MOD_EQ_0 : !m n. ~(n = 0) ==> (m MOD n = 0 <=> (?q. m = q * n)) MOD_EXISTS : !m n. (?q. m = n * q) <=> (if n = 0 then m = 0 else m MOD n = 0) MOD_LE : !m n. ~(n = 0) ==> m MOD n <= m MOD_LT : !m n. m < n ==> m MOD n = m MOD_MOD : !m n p. ~(n * p = 0) ==> m MOD (n * p) MOD n = m MOD n MOD_MOD_REFL' : !n m. ~(n = 0) ==> m MOD n MOD n = m MOD n MOD_MULT : !m n. ~(m = 0) ==> (m * n) MOD m = 0 MOD_MULT2 : !m n p. ~(m * p = 0) ==> (m * n) MOD (m * p) = m * n MOD p MOD_MULT_ADD : !m n p. (m * n + p) MOD n = p MOD n MOD_MULT_LMOD' : !n m p. ~(n = 0) ==> (m MOD n * p) MOD n = (m * p) MOD n MOD_MULT_MOD2' : !n m p. ~(n = 0) ==> (m MOD n * p MOD n) MOD n = (m * p) MOD n MOD_MULT_RMOD' : !n m p. ~(n = 0) ==> (m * p MOD n) MOD n = (m * p) MOD n MOD_REFL : !n. ~(n = 0) ==> n MOD n = 0 MOD_UNIQ : !m n q r. m = q * n + r /\ r < n ==> m MOD n = r MULT_DIV_LE : !m n p. ~(p = 0) ==> m * n DIV p <= (m * n) DIV p NOT_EVEN : !n. ~EVEN n <=> ODD n NOT_ODD : !n. ~ODD n <=> EVEN n ODD_ADD : !m n. ODD (m + n) <=> ~(ODD m <=> ODD n) ODD_DOUBLE : !n. ODD (SUC (2 * n)) ODD_EXISTS : !n. ODD n <=> (?m. n = SUC (2 * m)) ODD_MOD : !n. ODD n <=> n MOD 2 = 1 ODD_MULT : !m n. ODD (m * n) <=> ODD m /\ ODD n ODD_SUB : !m n. n <= m ==> (ODD (m - n) <=> ~(ODD m <=> ODD n)) SUC_INJ_MOD : !n a b. ~(n = 0) ==> (SUC a MOD n = SUC b MOD n <=> a MOD n = b MOD n) div_induction : !k p. 1 < k /\ p 0 /\ (!n. ~(n = 0) /\ p (n DIV k) ==> p n) ==> (!n. p n)

Back to main package page