- can_get_small
-
|- !x y d. 0 < d ==> ?c. 0 < c /\ y - c * d < x
- CONJ_EQ_ELIM
-
|- !P v e. (v = e) /\ P v = (v = e) /\ P e
- elim_eq
-
|- (x = y) = x < y + 1 /\ y < x + 1
- elim_neg_ones
-
|- !x. x + ~1 + 1 = x
- eq_justify_multiplication
-
|- !n x y. 0 < n ==> ((x = y) = (n * x = n * y))
- eq_move_all_left
-
|- !x y. (x = y) = (x + ~y = 0)
- eq_move_all_right
-
|- !x y. (x = y) = (0 = y + ~x)
- eq_move_left_left
-
|- !x y z. (x = y + z) = (x + ~y = z)
- eq_move_left_right
-
|- !x y z. (x + y = z) = (y = z + ~x)
- HO_SUB_ELIM
-
|- !P a b. P (& (a - b)) = & b <= & a /\ P (& a + ~& b) \/ & a < & b /\ P 0
- in_additive_range
-
|- !low d x. low < x /\ x <= low + d = ?j. (x = low + j) /\ 0 < j /\ j <= d
- INT_LT_ADD_NUMERAL
-
|- !x y.
x < x + & (NUMERAL (NUMERAL_BIT1 y)) /\
x < x + & (NUMERAL (NUMERAL_BIT2 y)) /\ ~(x < x + ~& (NUMERAL y))
- INT_NUM_COND
-
|- !b n m. & (if b then n else m) = (if b then & n else & m)
- INT_NUM_EVEN
-
|- !n. EVEN n = 2 int_divides & n
- INT_NUM_EXISTS
-
|- (?n. P (& n)) = ?x. 0 <= x /\ P x
- INT_NUM_FORALL
-
|- (!n. P (& n)) = !x. 0 <= x ==> P x
- INT_NUM_ODD
-
|- !n. ODD n = ~(2 int_divides & n)
- INT_NUM_SUB
-
|- !n m. & (n - m) = (if & n < & m then 0 else & n - & m)
- INT_NUM_UEXISTS
-
|- (?!n. P (& n)) = ?!x. 0 <= x /\ P x
- INT_SUB_SUB3
-
|- !x y z. x - (y - z) = x + z - y
- justify_divides
-
|- !n x y. 0 < n ==> (x int_divides y = n * x int_divides n * y)
- lcm_eliminate
-
|- !P c. (?x. P (c * x)) = ?x. P x /\ c int_divides x
- lt_justify_multiplication
-
|- !n x y. 0 < n ==> (x < y = n * x < n * y)
- lt_move_all_left
-
|- !x y. x < y = x + ~y < 0
- lt_move_all_right
-
|- !x y. x < y = 0 < y + ~x
- lt_move_left_left
-
|- !x y z. x < y + z = x + ~y < z
- lt_move_left_right
-
|- !x y z. x + y < z = y < z + ~x
- MEM_base
-
|- !e l. MEM e (e::l)
- MEM_build
-
|- !l1 e1 e2. MEM e1 l1 ==> MEM e1 (e2::l1)
- move_sub
-
|- !b c a. a - c + b = a + b - c
- not_less
-
|- ~(x < y) = y < x + 1
- positive_product_implication
-
|- !c d. 0 < c /\ 0 < d ==> 0 < c * d
- restricted_quantification_simp
-
|- !low high x.
low < x /\ x <= high =
low < high /\ ((x = high) \/ low < x /\ x <= high - 1)
- subtract_to_small
-
|- !x d. 0 < d ==> ?k. 0 < x - k * d /\ x - k * d <= d
- top_and_lessers
-
|- !P d x0. (!x. P x ==> P (x - d)) /\ P x0 ==> !c. 0 < c ==> P (x0 - c * d)