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