- ALL_DIVIDES_0
-
|- !a. divides a 0
- ZERO_DIVIDES
-
|- divides 0 m = (m = 0)
- DIVIDES_REFL
-
|- !a. divides a a
- ONE_DIVIDES_ALL
-
|- !a. divides 1 a
- DIVIDES_ADD_1
-
|- !a b c. divides a b /\ divides a c ==> divides a (b + c)
- DIVIDES_ADD_2
-
|- !a b c. divides a b /\ divides a (b + c) ==> divides a c
- DIVIDES_SUB
-
|- !a b c. divides a b /\ divides a c ==> divides a (b - c)
- DIVIDES_LE
-
|- !a b. 0 < b /\ divides a b ==> a <= b
- NOT_LT_DIV
-
|- !a b. 0 < b /\ b < a ==> ~divides a b
- DIVIDES_ANTISYM
-
|- !a b. divides a b /\ divides b a ==> (a = b)
- DIVIDES_TRANS
-
|- !p q r. divides p q ==> divides q r ==> divides p r
- DIVIDES_MULT
-
|- !a b c. divides a b ==> divides a (b * c)
- DIVIDES_FACT
-
|- !b. 0 < b ==> divides b (FACT b)
- DIVIDES_MULT_LEFT
-
|- !n m. divides (n * m) m = (m = 0) \/ (n = 1)
- NOT_PRIME_0
-
|- ~prime 0
- NOT_PRIME_1
-
|- ~prime 1