- REAL_0
-
|- real_0 = 0
- REAL_1
-
|- real_1 = 1
- REAL_10
-
|- 1 ≠ 0
- REAL_ADD_SYM
-
|- ∀x y. x + y = y + x
- REAL_ADD_COMM
-
|- ∀x y. x + y = y + x
- REAL_ADD_ASSOC
-
|- ∀x y z. x + (y + z) = x + y + z
- REAL_ADD_LID
-
|- ∀x. 0 + x = x
- REAL_ADD_LINV
-
|- ∀x. -x + x = 0
- REAL_LDISTRIB
-
|- ∀x y z. x * (y + z) = x * y + x * z
- REAL_LT_TOTAL
-
|- ∀x y. (x = y) ∨ x < y ∨ y < x
- REAL_LT_REFL
-
|- ∀x. ¬(x < x)
- REAL_LT_TRANS
-
|- ∀x y z. x < y ∧ y < z ⇒ x < z
- REAL_LT_IADD
-
|- ∀x y z. y < z ⇒ x + y < x + z
- REAL_SUP_ALLPOS
-
|- ∀P.
(∀x. P x ⇒ 0 < x) ∧ (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
- REAL_MUL_SYM
-
|- ∀x y. x * y = y * x
- REAL_MUL_COMM
-
|- ∀x y. x * y = y * x
- REAL_MUL_ASSOC
-
|- ∀x y z. x * (y * z) = x * y * z
- REAL_MUL_LID
-
|- ∀x. 1 * x = x
- REAL_MUL_LINV
-
|- ∀x. x ≠ 0 ⇒ (inv x * x = 1)
- REAL_LT_MUL
-
|- ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x * y
- REAL_INV_0
-
|- inv 0 = 0
- REAL_ADD_RID
-
|- ∀x. x + 0 = x
- REAL_ADD_RINV
-
|- ∀x. x + -x = 0
- REAL_MUL_RID
-
|- ∀x. x * 1 = x
- REAL_MUL_RINV
-
|- ∀x. x ≠ 0 ⇒ (x * inv x = 1)
- REAL_RDISTRIB
-
|- ∀x y z. (x + y) * z = x * z + y * z
- REAL_EQ_LADD
-
|- ∀x y z. (x + y = x + z) ⇔ (y = z)
- REAL_EQ_RADD
-
|- ∀x y z. (x + z = y + z) ⇔ (x = y)
- REAL_ADD_LID_UNIQ
-
|- ∀x y. (x + y = y) ⇔ (x = 0)
- REAL_ADD_RID_UNIQ
-
|- ∀x y. (x + y = x) ⇔ (y = 0)
- REAL_LNEG_UNIQ
-
|- ∀x y. (x + y = 0) ⇔ (x = -y)
- REAL_RNEG_UNIQ
-
|- ∀x y. (x + y = 0) ⇔ (y = -x)
- REAL_NEG_ADD
-
|- ∀x y. -(x + y) = -x + -y
- REAL_MUL_LZERO
-
|- ∀x. 0 * x = 0
- REAL_MUL_RZERO
-
|- ∀x. x * 0 = 0
- REAL_NEG_LMUL
-
|- ∀x y. -(x * y) = -x * y
- REAL_NEG_RMUL
-
|- ∀x y. -(x * y) = x * -y
- REAL_NEGNEG
-
|- ∀x. - -x = x
- REAL_NEG_MUL2
-
|- ∀x y. -x * -y = x * y
- REAL_ENTIRE
-
|- ∀x y. (x * y = 0) ⇔ (x = 0) ∨ (y = 0)
- REAL_LT_LADD
-
|- ∀x y z. x + y < x + z ⇔ y < z
- REAL_LT_RADD
-
|- ∀x y z. x + z < y + z ⇔ x < y
- REAL_NOT_LT
-
|- ∀x y. ¬(x < y) ⇔ y ≤ x
- REAL_LT_ANTISYM
-
|- ∀x y. ¬(x < y ∧ y < x)
- REAL_LT_GT
-
|- ∀x y. x < y ⇒ ¬(y < x)
- REAL_NOT_LE
-
|- ∀x y. ¬(x ≤ y) ⇔ y < x
- REAL_LE_TOTAL
-
|- ∀x y. x ≤ y ∨ y ≤ x
- REAL_LET_TOTAL
-
|- ∀x y. x ≤ y ∨ y < x
- REAL_LTE_TOTAL
-
|- ∀x y. x < y ∨ y ≤ x
- REAL_LE_REFL
-
|- ∀x. x ≤ x
- REAL_LE_LT
-
|- ∀x y. x ≤ y ⇔ x < y ∨ (x = y)
- REAL_LT_LE
-
|- ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y
- REAL_LT_IMP_LE
-
|- ∀x y. x < y ⇒ x ≤ y
- REAL_LTE_TRANS
-
|- ∀x y z. x < y ∧ y ≤ z ⇒ x < z
- REAL_LET_TRANS
-
|- ∀x y z. x ≤ y ∧ y < z ⇒ x < z
- REAL_LE_TRANS
-
|- ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z
- REAL_LE_ANTISYM
-
|- ∀x y. x ≤ y ∧ y ≤ x ⇔ (x = y)
- REAL_LET_ANTISYM
-
|- ∀x y. ¬(x < y ∧ y ≤ x)
- REAL_LTE_ANTSYM
-
|- ∀x y. ¬(x ≤ y ∧ y < x)
- REAL_NEG_LT0
-
|- ∀x. -x < 0 ⇔ 0 < x
- REAL_NEG_GT0
-
|- ∀x. 0 < -x ⇔ x < 0
- REAL_NEG_LE0
-
|- ∀x. -x ≤ 0 ⇔ 0 ≤ x
- REAL_NEG_GE0
-
|- ∀x. 0 ≤ -x ⇔ x ≤ 0
- REAL_LT_NEGTOTAL
-
|- ∀x. (x = 0) ∨ 0 < x ∨ 0 < -x
- REAL_LE_NEGTOTAL
-
|- ∀x. 0 ≤ x ∨ 0 ≤ -x
- REAL_LE_MUL
-
|- ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y
- REAL_LE_SQUARE
-
|- ∀x. 0 ≤ x * x
- REAL_LE_01
-
|- 0 ≤ 1
- REAL_LT_01
-
|- 0 < 1
- REAL_LE_LADD
-
|- ∀x y z. x + y ≤ x + z ⇔ y ≤ z
- REAL_LE_RADD
-
|- ∀x y z. x + z ≤ y + z ⇔ x ≤ y
- REAL_LT_ADD2
-
|- ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z
- REAL_LE_ADD2
-
|- ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z
- REAL_LE_ADD
-
|- ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y
- REAL_LT_ADD
-
|- ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y
- REAL_LT_ADDNEG
-
|- ∀x y z. y < x + -z ⇔ y + z < x
- REAL_LT_ADDNEG2
-
|- ∀x y z. x + -y < z ⇔ x < z + y
- REAL_LT_ADD1
-
|- ∀x y. x ≤ y ⇒ x < y + 1
- REAL_SUB_ADD
-
|- ∀x y. x − y + y = x
- REAL_SUB_ADD2
-
|- ∀x y. y + (x − y) = x
- REAL_SUB_REFL
-
|- ∀x. x − x = 0
- REAL_SUB_0
-
|- ∀x y. (x − y = 0) ⇔ (x = y)
- REAL_LE_DOUBLE
-
|- ∀x. 0 ≤ x + x ⇔ 0 ≤ x
- REAL_LE_NEGL
-
|- ∀x. -x ≤ x ⇔ 0 ≤ x
- REAL_LE_NEGR
-
|- ∀x. x ≤ -x ⇔ x ≤ 0
- REAL_NEG_EQ0
-
|- ∀x. (-x = 0) ⇔ (x = 0)
- REAL_NEG_0
-
|- -0 = 0
- REAL_NEG_SUB
-
|- ∀x y. -(x − y) = y − x
- REAL_SUB_LT
-
|- ∀x y. 0 < x − y ⇔ y < x
- REAL_SUB_LE
-
|- ∀x y. 0 ≤ x − y ⇔ y ≤ x
- REAL_ADD_SUB
-
|- ∀x y. x + y − x = y
- REAL_EQ_LMUL
-
|- ∀x y z. (x * y = x * z) ⇔ (x = 0) ∨ (y = z)
- REAL_EQ_RMUL
-
|- ∀x y z. (x * z = y * z) ⇔ (z = 0) ∨ (x = y)
- REAL_SUB_LDISTRIB
-
|- ∀x y z. x * (y − z) = x * y − x * z
- REAL_SUB_RDISTRIB
-
|- ∀x y z. (x − y) * z = x * z − y * z
- REAL_NEG_EQ
-
|- ∀x y. (-x = y) ⇔ (x = -y)
- REAL_NEG_MINUS1
-
|- ∀x. -x = -1 * x
- REAL_INV_NZ
-
|- ∀x. x ≠ 0 ⇒ inv x ≠ 0
- REAL_INVINV
-
|- ∀x. x ≠ 0 ⇒ (inv (inv x) = x)
- REAL_LT_IMP_NE
-
|- ∀x y. x < y ⇒ x ≠ y
- REAL_INV_POS
-
|- ∀x. 0 < x ⇒ 0 < inv x
- REAL_LT_LMUL_0
-
|- ∀x y. 0 < x ⇒ (0 < x * y ⇔ 0 < y)
- REAL_LT_RMUL_0
-
|- ∀x y. 0 < y ⇒ (0 < x * y ⇔ 0 < x)
- REAL_LT_LMUL
-
|- ∀x y z. 0 < x ⇒ (x * y < x * z ⇔ y < z)
- REAL_LT_RMUL
-
|- ∀x y z. 0 < z ⇒ (x * z < y * z ⇔ x < y)
- REAL_LT_RMUL_IMP
-
|- ∀x y z. x < y ∧ 0 < z ⇒ x * z < y * z
- REAL_LT_LMUL_IMP
-
|- ∀x y z. y < z ∧ 0 < x ⇒ x * y < x * z
- REAL_LINV_UNIQ
-
|- ∀x y. (x * y = 1) ⇒ (x = inv y)
- REAL_RINV_UNIQ
-
|- ∀x y. (x * y = 1) ⇒ (y = inv x)
- REAL_INV_INV
-
|- ∀x. inv (inv x) = x
- REAL_INV_EQ_0
-
|- ∀x. (inv x = 0) ⇔ (x = 0)
- REAL_NEG_INV
-
|- ∀x. x ≠ 0 ⇒ (-inv x = inv (-x))
- REAL_INV_1OVER
-
|- ∀x. inv x = 1 / x
- REAL_LT_INV_EQ
-
|- ∀x. 0 < inv x ⇔ 0 < x
- REAL_LE_INV_EQ
-
|- ∀x. 0 ≤ inv x ⇔ 0 ≤ x
- REAL_LE_INV
-
|- ∀x. 0 ≤ x ⇒ 0 ≤ inv x
- REAL_LE_ADDR
-
|- ∀x y. x ≤ x + y ⇔ 0 ≤ y
- REAL_LE_ADDL
-
|- ∀x y. y ≤ x + y ⇔ 0 ≤ x
- REAL_LT_ADDR
-
|- ∀x y. x < x + y ⇔ 0 < y
- REAL_LT_ADDL
-
|- ∀x y. y < x + y ⇔ 0 < x
- REAL
-
|- ∀n. &SUC n = &n + 1
- REAL_POS
-
|- ∀n. 0 ≤ &n
- REAL_LE
-
|- ∀m n. &m ≤ &n ⇔ m ≤ n
- REAL_LT
-
|- ∀m n. &m < &n ⇔ m < n
- REAL_INJ
-
|- ∀m n. (&m = &n) ⇔ (m = n)
- REAL_ADD
-
|- ∀m n. &m + &n = &(m + n)
- REAL_MUL
-
|- ∀m n. &m * &n = &(m * n)
- REAL_INV1
-
|- inv 1 = 1
- REAL_OVER1
-
|- ∀x. x / 1 = x
- REAL_DIV_REFL
-
|- ∀x. x ≠ 0 ⇒ (x / x = 1)
- REAL_DIV_LZERO
-
|- ∀x. 0 / x = 0
- REAL_LT_NZ
-
|- ∀n. &n ≠ 0 ⇔ 0 < &n
- REAL_NZ_IMP_LT
-
|- ∀n. n ≠ 0 ⇒ 0 < &n
- REAL_LT_RDIV_0
-
|- ∀y z. 0 < z ⇒ (0 < y / z ⇔ 0 < y)
- REAL_LT_RDIV
-
|- ∀x y z. 0 < z ⇒ (x / z < y / z ⇔ x < y)
- REAL_LT_FRACTION_0
-
|- ∀n d. n ≠ 0 ⇒ (0 < d / &n ⇔ 0 < d)
- REAL_LT_MULTIPLE
-
|- ∀n d. 1 < n ⇒ (d < &n * d ⇔ 0 < d)
- REAL_LT_FRACTION
-
|- ∀n d. 1 < n ⇒ (d / &n < d ⇔ 0 < d)
- REAL_LT_HALF1
-
|- ∀d. 0 < d / 2 ⇔ 0 < d
- REAL_LT_HALF2
-
|- ∀d. d / 2 < d ⇔ 0 < d
- REAL_DOUBLE
-
|- ∀x. x + x = 2 * x
- REAL_DIV_LMUL
-
|- ∀x y. y ≠ 0 ⇒ (y * (x / y) = x)
- REAL_DIV_RMUL
-
|- ∀x y. y ≠ 0 ⇒ (x / y * y = x)
- REAL_HALF_DOUBLE
-
|- ∀x. x / 2 + x / 2 = x
- REAL_DOWN
-
|- ∀x. 0 < x ⇒ ∃y. 0 < y ∧ y < x
- REAL_DOWN2
-
|- ∀x y. 0 < x ∧ 0 < y ⇒ ∃z. 0 < z ∧ z < x ∧ z < y
- REAL_SUB_SUB
-
|- ∀x y. x − y − x = -y
- REAL_LT_ADD_SUB
-
|- ∀x y z. x + y < z ⇔ x < z − y
- REAL_LT_SUB_RADD
-
|- ∀x y z. x − y < z ⇔ x < z + y
- REAL_LT_SUB_LADD
-
|- ∀x y z. x < y − z ⇔ x + z < y
- REAL_LE_SUB_LADD
-
|- ∀x y z. x ≤ y − z ⇔ x + z ≤ y
- REAL_LE_SUB_RADD
-
|- ∀x y z. x − y ≤ z ⇔ x ≤ z + y
- REAL_LT_NEG
-
|- ∀x y. -x < -y ⇔ y < x
- REAL_LE_NEG
-
|- ∀x y. -x ≤ -y ⇔ y ≤ x
- REAL_ADD2_SUB2
-
|- ∀a b c d. a + b − (c + d) = a − c + (b − d)
- REAL_SUB_LZERO
-
|- ∀x. 0 − x = -x
- REAL_SUB_RZERO
-
|- ∀x. x − 0 = x
- REAL_LET_ADD2
-
|- ∀w x y z. w ≤ x ∧ y < z ⇒ w + y < x + z
- REAL_LTE_ADD2
-
|- ∀w x y z. w < x ∧ y ≤ z ⇒ w + y < x + z
- REAL_LET_ADD
-
|- ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y
- REAL_LTE_ADD
-
|- ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y
- REAL_LT_MUL2
-
|- ∀x1 x2 y1 y2. 0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 < x2 ∧ y1 < y2 ⇒ x1 * y1 < x2 * y2
- REAL_LT_INV
-
|- ∀x y. 0 < x ∧ x < y ⇒ inv y < inv x
- REAL_SUB_LNEG
-
|- ∀x y. -x − y = -(x + y)
- REAL_SUB_RNEG
-
|- ∀x y. x − -y = x + y
- REAL_SUB_NEG2
-
|- ∀x y. -x − -y = y − x
- REAL_SUB_TRIANGLE
-
|- ∀a b c. a − b + (b − c) = a − c
- REAL_EQ_SUB_LADD
-
|- ∀x y z. (x = y − z) ⇔ (x + z = y)
- REAL_EQ_SUB_RADD
-
|- ∀x y z. (x − y = z) ⇔ (x = z + y)
- REAL_INV_MUL
-
|- ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ (inv (x * y) = inv x * inv y)
- REAL_LE_LMUL
-
|- ∀x y z. 0 < x ⇒ (x * y ≤ x * z ⇔ y ≤ z)
- REAL_LE_RMUL
-
|- ∀x y z. 0 < z ⇒ (x * z ≤ y * z ⇔ x ≤ y)
- REAL_SUB_INV2
-
|- ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ (inv x − inv y = (y − x) / (x * y))
- REAL_SUB_SUB2
-
|- ∀x y. x − (x − y) = y
- REAL_ADD_SUB2
-
|- ∀x y. x − (x + y) = -y
- REAL_MEAN
-
|- ∀x y. x < y ⇒ ∃z. x < z ∧ z < y
- REAL_EQ_LMUL2
-
|- ∀x y z. x ≠ 0 ⇒ ((y = z) ⇔ (x * y = x * z))
- REAL_LE_MUL2
-
|- ∀x1 x2 y1 y2. 0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≤ x2 ∧ y1 ≤ y2 ⇒ x1 * y1 ≤ x2 * y2
- REAL_LE_LDIV
-
|- ∀x y z. 0 < x ∧ y ≤ z * x ⇒ y / x ≤ z
- REAL_LE_RDIV
-
|- ∀x y z. 0 < x ∧ y * x ≤ z ⇒ y ≤ z / x
- REAL_LT_DIV
-
|- ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x / y
- REAL_LE_DIV
-
|- ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x / y
- REAL_LT_1
-
|- ∀x y. 0 ≤ x ∧ x < y ⇒ x / y < 1
- REAL_LE_LMUL_IMP
-
|- ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ x * y ≤ x * z
- REAL_LE_RMUL_IMP
-
|- ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ y * x ≤ z * x
- REAL_EQ_IMP_LE
-
|- ∀x y. (x = y) ⇒ x ≤ y
- REAL_INV_LT1
-
|- ∀x. 0 < x ∧ x < 1 ⇒ 1 < inv x
- REAL_POS_NZ
-
|- ∀x. 0 < x ⇒ x ≠ 0
- REAL_EQ_RMUL_IMP
-
|- ∀x y z. z ≠ 0 ∧ (x * z = y * z) ⇒ (x = y)
- REAL_EQ_LMUL_IMP
-
|- ∀x y z. x ≠ 0 ∧ (x * y = x * z) ⇒ (y = z)
- REAL_FACT_NZ
-
|- ∀n. &FACT n ≠ 0
- REAL_DIFFSQ
-
|- ∀x y. (x + y) * (x − y) = x * x − y * y
- REAL_POASQ
-
|- ∀x. 0 < x * x ⇔ x ≠ 0
- REAL_SUMSQ
-
|- ∀x y. (x * x + y * y = 0) ⇔ (x = 0) ∧ (y = 0)
- REAL_EQ_NEG
-
|- ∀x y. (-x = -y) ⇔ (x = y)
- REAL_DIV_MUL2
-
|- ∀x z. x ≠ 0 ∧ z ≠ 0 ⇒ ∀y. y / z = x * y / (x * z)
- REAL_MIDDLE1
-
|- ∀a b. a ≤ b ⇒ a ≤ (a + b) / 2
- REAL_MIDDLE2
-
|- ∀a b. a ≤ b ⇒ (a + b) / 2 ≤ b
- ABS_ZERO
-
|- ∀x. (abs x = 0) ⇔ (x = 0)
- ABS_0
-
|- abs 0 = 0
- ABS_1
-
|- abs 1 = 1
- ABS_NEG
-
|- ∀x. abs (-x) = abs x
- ABS_TRIANGLE
-
|- ∀x y. abs (x + y) ≤ abs x + abs y
- ABS_POS
-
|- ∀x. 0 ≤ abs x
- ABS_MUL
-
|- ∀x y. abs (x * y) = abs x * abs y
- ABS_LT_MUL2
-
|- ∀w x y z. abs w < y ∧ abs x < z ⇒ abs (w * x) < y * z
- ABS_SUB
-
|- ∀x y. abs (x − y) = abs (y − x)
- ABS_NZ
-
|- ∀x. x ≠ 0 ⇔ 0 < abs x
- ABS_INV
-
|- ∀x. x ≠ 0 ⇒ (abs (inv x) = inv (abs x))
- ABS_ABS
-
|- ∀x. abs (abs x) = abs x
- ABS_LE
-
|- ∀x. x ≤ abs x
- ABS_REFL
-
|- ∀x. (abs x = x) ⇔ 0 ≤ x
- ABS_N
-
|- ∀n. abs (&n) = &n
- ABS_BETWEEN
-
|- ∀x y d. 0 < d ∧ x − d < y ∧ y < x + d ⇔ abs (y − x) < d
- ABS_BOUND
-
|- ∀x y d. abs (x − y) < d ⇒ y < x + d
- ABS_STILLNZ
-
|- ∀x y. abs (x − y) < abs y ⇒ x ≠ 0
- ABS_CASES
-
|- ∀x. (x = 0) ∨ 0 < abs x
- ABS_BETWEEN1
-
|- ∀x y z. x < z ∧ abs (y − x) < z − x ⇒ y < z
- ABS_SIGN
-
|- ∀x y. abs (x − y) < y ⇒ 0 < x
- ABS_SIGN2
-
|- ∀x y. abs (x − y) < -y ⇒ x < 0
- ABS_DIV
-
|- ∀y. y ≠ 0 ⇒ ∀x. abs (x / y) = abs x / abs y
- ABS_CIRCLE
-
|- ∀x y h. abs h < abs y − abs x ⇒ abs (x + h) < abs y
- REAL_SUB_ABS
-
|- ∀x y. abs x − abs y ≤ abs (x − y)
- ABS_SUB_ABS
-
|- ∀x y. abs (abs x − abs y) ≤ abs (x − y)
- ABS_BETWEEN2
-
|- ∀x0 x y0 y.
x0 < y0 ∧ abs (x − x0) < (y0 − x0) / 2 ∧ abs (y − y0) < (y0 − x0) / 2 ⇒
x < y
- ABS_BOUNDS
-
|- ∀x k. abs x ≤ k ⇔ -k ≤ x ∧ x ≤ k
- POW_0
-
|- ∀n. 0 pow SUC n = 0
- POW_NZ
-
|- ∀c n. c ≠ 0 ⇒ c pow n ≠ 0
- POW_INV
-
|- ∀c. c ≠ 0 ⇒ ∀n. inv (c pow n) = inv c pow n
- POW_ABS
-
|- ∀c n. abs c pow n = abs (c pow n)
- POW_PLUS1
-
|- ∀e. 0 < e ⇒ ∀n. 1 + &n * e ≤ (1 + e) pow n
- POW_ADD
-
|- ∀c m n. c pow (m + n) = c pow m * c pow n
- POW_1
-
|- ∀x. x pow 1 = x
- POW_2
-
|- ∀x. x pow 2 = x * x
- POW_ONE
-
|- ∀n. 1 pow n = 1
- POW_POS
-
|- ∀x. 0 ≤ x ⇒ ∀n. 0 ≤ x pow n
- POW_LE
-
|- ∀n x y. 0 ≤ x ∧ x ≤ y ⇒ x pow n ≤ y pow n
- POW_M1
-
|- ∀n. abs (-1 pow n) = 1
- POW_MUL
-
|- ∀n x y. (x * y) pow n = x pow n * y pow n
- REAL_LE_POW2
-
|- ∀x. 0 ≤ x pow 2
- ABS_POW2
-
|- ∀x. abs (x pow 2) = x pow 2
- REAL_POW2_ABS
-
|- ∀x. abs x pow 2 = x pow 2
- REAL_LE1_POW2
-
|- ∀x. 1 ≤ x ⇒ 1 ≤ x pow 2
- REAL_LT1_POW2
-
|- ∀x. 1 < x ⇒ 1 < x pow 2
- POW_POS_LT
-
|- ∀x n. 0 < x ⇒ 0 < x pow SUC n
- POW_2_LE1
-
|- ∀n. 1 ≤ 2 pow n
- POW_2_LT
-
|- ∀n. &n < 2 pow n
- POW_MINUS1
-
|- ∀n. -1 pow (2 * n) = 1
- POW_LT
-
|- ∀n x y. 0 ≤ x ∧ x < y ⇒ x pow SUC n < y pow SUC n
- REAL_POW_LT
-
|- ∀x n. 0 < x ⇒ 0 < x pow n
- POW_EQ
-
|- ∀n x y. 0 ≤ x ∧ 0 ≤ y ∧ (x pow SUC n = y pow SUC n) ⇒ (x = y)
- POW_ZERO
-
|- ∀n x. (x pow n = 0) ⇒ (x = 0)
- POW_ZERO_EQ
-
|- ∀n x. (x pow SUC n = 0) ⇔ (x = 0)
- REAL_POW_LT2
-
|- ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ x < y ⇒ x pow n < y pow n
- REAL_POW_MONO_LT
-
|- ∀m n x. 1 < x ∧ m < n ⇒ x pow m < x pow n
- REAL_POW_POW
-
|- ∀x m n. (x pow m) pow n = x pow (m * n)
- REAL_SUP_SOMEPOS
-
|- ∀P.
(∃x. P x ∧ 0 < x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
- SUP_LEMMA1
-
|- ∀P s d.
(∀y. (∃x. (λx. P (x + d)) x ∧ y < x) ⇔ y < s) ⇒
∀y. (∃x. P x ∧ y < x) ⇔ y < s + d
- SUP_LEMMA2
-
|- ∀P. (∃x. P x) ⇒ ∃d x. (λx. P (x + d)) x ∧ 0 < x
- SUP_LEMMA3
-
|- ∀d. (∃z. ∀x. P x ⇒ x < z) ⇒ ∃z. ∀x. (λx. P (x + d)) x ⇒ x < z
- REAL_SUP_EXISTS
-
|- ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒ ∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s
- REAL_SUP
-
|- ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒ ∀y. (∃x. P x ∧ y < x) ⇔ y < sup P
- REAL_SUP_UBOUND
-
|- ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒ ∀y. P y ⇒ y ≤ sup P
- SETOK_LE_LT
-
|- ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇔ (∃x. P x) ∧ ∃z. ∀x. P x ⇒ x < z
- REAL_SUP_LE
-
|- ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇒ ∀y. (∃x. P x ∧ y < x) ⇔ y < sup P
- REAL_SUP_UBOUND_LE
-
|- ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇒ ∀y. P y ⇒ y ≤ sup P
- REAL_ARCH
-
|- ∀x. 0 < x ⇒ ∀y. ∃n. y < &n * x
- REAL_ARCH_LEAST
-
|- ∀y. 0 < y ⇒ ∀x. 0 ≤ x ⇒ ∃n. &n * y ≤ x ∧ x < &SUC n * y
- sum_ind
-
|- ∀P.
(∀n f. P (n,0) f) ∧ (∀n m f. P (n,m) f ⇒ P (n,SUC m) f) ⇒
∀v v1 v2. P (v,v1) v2
- sum
-
|- (∀n f. sum (n,0) f = 0) ∧ ∀n m f. sum (n,SUC m) f = sum (n,m) f + f (n + m)
- sum_compute
-
|- (∀n f. sum (n,0) f = 0) ∧
(∀n m f.
sum (n,NUMERAL (BIT1 m)) f =
sum (n,NUMERAL (BIT1 m) − 1) f + f (n + (NUMERAL (BIT1 m) − 1))) ∧
∀n m f.
sum (n,NUMERAL (BIT2 m)) f =
sum (n,NUMERAL (BIT1 m)) f + f (n + NUMERAL (BIT1 m))
- SUM_TWO
-
|- ∀f n p. sum (0,n) f + sum (n,p) f = sum (0,n + p) f
- SUM_DIFF
-
|- ∀f m n. sum (m,n) f = sum (0,m + n) f − sum (0,m) f
- ABS_SUM
-
|- ∀f m n. abs (sum (m,n) f) ≤ sum (m,n) (λn. abs (f n))
- SUM_LE
-
|- ∀f g m n. (∀r. m ≤ r ∧ r < n + m ⇒ f r ≤ g r) ⇒ sum (m,n) f ≤ sum (m,n) g
- SUM_EQ
-
|- ∀f g m n.
(∀r. m ≤ r ∧ r < n + m ⇒ (f r = g r)) ⇒ (sum (m,n) f = sum (m,n) g)
- SUM_POS
-
|- ∀f. (∀n. 0 ≤ f n) ⇒ ∀m n. 0 ≤ sum (m,n) f
- SUM_POS_GEN
-
|- ∀f m. (∀n. m ≤ n ⇒ 0 ≤ f n) ⇒ ∀n. 0 ≤ sum (m,n) f
- SUM_ABS
-
|- ∀f m n. abs (sum (m,n) (λm. abs (f m))) = sum (m,n) (λm. abs (f m))
- SUM_ABS_LE
-
|- ∀f m n. abs (sum (m,n) f) ≤ sum (m,n) (λn. abs (f n))
- SUM_ZERO
-
|- ∀f N. (∀n. n ≥ N ⇒ (f n = 0)) ⇒ ∀m n. m ≥ N ⇒ (sum (m,n) f = 0)
- SUM_ADD
-
|- ∀f g m n. sum (m,n) (λn. f n + g n) = sum (m,n) f + sum (m,n) g
- SUM_CMUL
-
|- ∀f c m n. sum (m,n) (λn. c * f n) = c * sum (m,n) f
- SUM_NEG
-
|- ∀f n d. sum (n,d) (λn. -f n) = -sum (n,d) f
- SUM_SUB
-
|- ∀f g m n. sum (m,n) (λn. f n − g n) = sum (m,n) f − sum (m,n) g
- SUM_SUBST
-
|- ∀f g m n.
(∀p. m ≤ p ∧ p < m + n ⇒ (f p = g p)) ⇒ (sum (m,n) f = sum (m,n) g)
- SUM_NSUB
-
|- ∀n f c. sum (0,n) f − &n * c = sum (0,n) (λp. f p − c)
- SUM_BOUND
-
|- ∀f k m n. (∀p. m ≤ p ∧ p < m + n ⇒ f p ≤ k) ⇒ sum (m,n) f ≤ &n * k
- SUM_GROUP
-
|- ∀n k f. sum (0,n) (λm. sum (m * k,k) f) = sum (0,n * k) f
- SUM_1
-
|- ∀f n. sum (n,1) f = f n
- SUM_2
-
|- ∀f n. sum (n,2) f = f n + f (n + 1)
- SUM_OFFSET
-
|- ∀f n k. sum (0,n) (λm. f (m + k)) = sum (0,n + k) f − sum (0,k) f
- SUM_REINDEX
-
|- ∀f m k n. sum (m + k,n) f = sum (m,n) (λr. f (r + k))
- SUM_0
-
|- ∀m n. sum (m,n) (λr. 0) = 0
- SUM_PERMUTE_0
-
|- ∀n p.
(∀y. y < n ⇒ ∃!x. x < n ∧ (p x = y)) ⇒
∀f. sum (0,n) (λn. f (p n)) = sum (0,n) f
- SUM_CANCEL
-
|- ∀f n d. sum (n,d) (λn. f (SUC n) − f n) = f (n + d) − f n
- REAL_MUL_RNEG
-
|- ∀x y. x * -y = -(x * y)
- REAL_MUL_LNEG
-
|- ∀x y. -x * y = -(x * y)
- real_lt
-
|- ∀y x. x < y ⇔ ¬(y ≤ x)
- REAL_LE_LADD_IMP
-
|- ∀x y z. y ≤ z ⇒ x + y ≤ x + z
- REAL_LE_LNEG
-
|- ∀x y. -x ≤ y ⇔ 0 ≤ x + y
- REAL_LE_NEG2
-
|- ∀x y. -x ≤ -y ⇔ y ≤ x
- REAL_NEG_NEG
-
|- ∀x. - -x = x
- REAL_LE_RNEG
-
|- ∀x y. x ≤ -y ⇔ x + y ≤ 0
- REAL_POW_INV
-
|- ∀x n. inv x pow n = inv (x pow n)
- REAL_POW_DIV
-
|- ∀x y n. (x / y) pow n = x pow n / y pow n
- REAL_POW_ADD
-
|- ∀x m n. x pow (m + n) = x pow m * x pow n
- REAL_LE_RDIV_EQ
-
|- ∀x y z. 0 < z ⇒ (x ≤ y / z ⇔ x * z ≤ y)
- REAL_LE_LDIV_EQ
-
|- ∀x y z. 0 < z ⇒ (x / z ≤ y ⇔ x ≤ y * z)
- REAL_LT_RDIV_EQ
-
|- ∀x y z. 0 < z ⇒ (x < y / z ⇔ x * z < y)
- REAL_LT_LDIV_EQ
-
|- ∀x y z. 0 < z ⇒ (x / z < y ⇔ x < y * z)
- REAL_EQ_RDIV_EQ
-
|- ∀x y z. 0 < z ⇒ ((x = y / z) ⇔ (x * z = y))
- REAL_EQ_LDIV_EQ
-
|- ∀x y z. 0 < z ⇒ ((x / z = y) ⇔ (x = y * z))
- REAL_OF_NUM_POW
-
|- ∀x n. &x pow n = &(x ** n)
- REAL_ADD_LDISTRIB
-
|- ∀x y z. x * (y + z) = x * y + x * z
- REAL_ADD_RDISTRIB
-
|- ∀x y z. (x + y) * z = x * z + y * z
- REAL_OF_NUM_ADD
-
|- ∀m n. &m + &n = &(m + n)
- REAL_OF_NUM_LE
-
|- ∀m n. &m ≤ &n ⇔ m ≤ n
- REAL_OF_NUM_MUL
-
|- ∀m n. &m * &n = &(m * n)
- REAL_OF_NUM_SUC
-
|- ∀n. &n + 1 = &SUC n
- REAL_OF_NUM_EQ
-
|- ∀m n. (&m = &n) ⇔ (m = n)
- REAL_EQ_MUL_LCANCEL
-
|- ∀x y z. (x * y = x * z) ⇔ (x = 0) ∨ (y = z)
- REAL_ABS_0
-
|- abs 0 = 0
- REAL_ABS_TRIANGLE
-
|- ∀x y. abs (x + y) ≤ abs x + abs y
- REAL_ABS_MUL
-
|- ∀x y. abs (x * y) = abs x * abs y
- REAL_ABS_POS
-
|- ∀x. 0 ≤ abs x
- REAL_LE_EPSILON
-
|- ∀x y. (∀e. 0 < e ⇒ x ≤ y + e) ⇒ x ≤ y
- REAL_BIGNUM
-
|- ∀r. ∃n. r < &n
- REAL_INV_LT_ANTIMONO
-
|- ∀x y. 0 < x ∧ 0 < y ⇒ (inv x < inv y ⇔ y < x)
- REAL_INV_INJ
-
|- ∀x y. (inv x = inv y) ⇔ (x = y)
- REAL_DIV_RMUL_CANCEL
-
|- ∀c a b. c ≠ 0 ⇒ (a * c / (b * c) = a / b)
- REAL_DIV_LMUL_CANCEL
-
|- ∀c a b. c ≠ 0 ⇒ (c * a / (c * b) = a / b)
- REAL_DIV_ADD
-
|- ∀x y z. y / x + z / x = (y + z) / x
- REAL_ADD_RAT
-
|- ∀a b c d. b ≠ 0 ∧ d ≠ 0 ⇒ (a / b + c / d = (a * d + b * c) / (b * d))
- REAL_SUB_RAT
-
|- ∀a b c d. b ≠ 0 ∧ d ≠ 0 ⇒ (a / b − c / d = (a * d − b * c) / (b * d))
- REAL_SUB
-
|- ∀m n. &m − &n = if m − n = 0 then -&(n − m) else &(m − n)
- REAL_POS_POS
-
|- ∀x. 0 ≤ pos x
- REAL_POS_ID
-
|- ∀x. 0 ≤ x ⇒ (pos x = x)
- REAL_POS_INFLATE
-
|- ∀x. x ≤ pos x
- REAL_POS_MONO
-
|- ∀x y. x ≤ y ⇒ pos x ≤ pos y
- REAL_POS_EQ_ZERO
-
|- ∀x. (pos x = 0) ⇔ x ≤ 0
- REAL_POS_LE_ZERO
-
|- ∀x. pos x ≤ 0 ⇔ x ≤ 0
- REAL_MIN_REFL
-
|- ∀x. min x x = x
- REAL_LE_MIN
-
|- ∀z x y. z ≤ min x y ⇔ z ≤ x ∧ z ≤ y
- REAL_MIN_LE
-
|- ∀z x y. min x y ≤ z ⇔ x ≤ z ∨ y ≤ z
- REAL_MIN_LE1
-
|- ∀x y. min x y ≤ x
- REAL_MIN_LE2
-
|- ∀x y. min x y ≤ y
- REAL_MIN_ALT
-
|- ∀x y. (x ≤ y ⇒ (min x y = x)) ∧ (y ≤ x ⇒ (min x y = y))
- REAL_MIN_LE_LIN
-
|- ∀z x y. 0 ≤ z ∧ z ≤ 1 ⇒ min x y ≤ z * x + (1 − z) * y
- REAL_MIN_ADD
-
|- ∀z x y. min (x + z) (y + z) = min x y + z
- REAL_MIN_SUB
-
|- ∀z x y. min (x − z) (y − z) = min x y − z
- REAL_IMP_MIN_LE2
-
|- ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ min x1 x2 ≤ min y1 y2
- REAL_MAX_REFL
-
|- ∀x. max x x = x
- REAL_LE_MAX
-
|- ∀z x y. z ≤ max x y ⇔ z ≤ x ∨ z ≤ y
- REAL_LE_MAX1
-
|- ∀x y. x ≤ max x y
- REAL_LE_MAX2
-
|- ∀x y. y ≤ max x y
- REAL_MAX_LE
-
|- ∀z x y. max x y ≤ z ⇔ x ≤ z ∧ y ≤ z
- REAL_MAX_ALT
-
|- ∀x y. (x ≤ y ⇒ (max x y = y)) ∧ (y ≤ x ⇒ (max x y = x))
- REAL_MAX_MIN
-
|- ∀x y. max x y = -min (-x) (-y)
- REAL_MIN_MAX
-
|- ∀x y. min x y = -max (-x) (-y)
- REAL_LIN_LE_MAX
-
|- ∀z x y. 0 ≤ z ∧ z ≤ 1 ⇒ z * x + (1 − z) * y ≤ max x y
- REAL_MAX_ADD
-
|- ∀z x y. max (x + z) (y + z) = max x y + z
- REAL_MAX_SUB
-
|- ∀z x y. max (x − z) (y − z) = max x y − z
- REAL_IMP_MAX_LE2
-
|- ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ max x1 x2 ≤ max y1 y2
- REAL_SUP_EXISTS_UNIQUE
-
|- ∀p. (∃x. p x) ∧ (∃z. ∀x. p x ⇒ x ≤ z) ⇒ ∃!s. ∀y. (∃x. p x ∧ y < x) ⇔ y < s
- REAL_SUP_MAX
-
|- ∀p z. p z ∧ (∀x. p x ⇒ x ≤ z) ⇒ (sup p = z)
- REAL_IMP_SUP_LE
-
|- ∀p x. (∃r. p r) ∧ (∀r. p r ⇒ r ≤ x) ⇒ sup p ≤ x
- REAL_IMP_LE_SUP
-
|- ∀p x. (∃r. p r) ∧ (∃z. ∀r. p r ⇒ r ≤ z) ∧ (∃r. p r ∧ x ≤ r) ⇒ x ≤ sup p
- REAL_INF_MIN
-
|- ∀p z. p z ∧ (∀x. p x ⇒ z ≤ x) ⇒ (inf p = z)
- REAL_IMP_LE_INF
-
|- ∀p r. (∃x. p x) ∧ (∀x. p x ⇒ r ≤ x) ⇒ r ≤ inf p
- REAL_IMP_INF_LE
-
|- ∀p r. (∃z. ∀x. p x ⇒ z ≤ x) ∧ (∃x. p x ∧ x ≤ r) ⇒ inf p ≤ r
- REAL_INF_LT
-
|- ∀p z. (∃x. p x) ∧ inf p < z ⇒ ∃x. p x ∧ x < z
- REAL_INF_CLOSE
-
|- ∀p e. (∃x. p x) ∧ 0 < e ⇒ ∃x. p x ∧ x < inf p + e
- SUP_EPSILON
-
|- ∀p e. 0 < e ∧ (∃x. p x) ∧ (∃z. ∀x. p x ⇒ x ≤ z) ⇒ ∃x. p x ∧ sup p ≤ x + e
- REAL_LE_SUP
-
|- ∀p x.
(∃y. p y) ∧ (∃y. ∀z. p z ⇒ z ≤ y) ⇒
(x ≤ sup p ⇔ ∀y. (∀z. p z ⇒ z ≤ y) ⇒ x ≤ y)
- REAL_INF_LE
-
|- ∀p x.
(∃y. p y) ∧ (∃y. ∀z. p z ⇒ y ≤ z) ⇒
(inf p ≤ x ⇔ ∀y. (∀z. p z ⇒ y ≤ z) ⇒ y ≤ x)
- REAL_SUP_CONST
-
|- ∀x. sup (λr. r = x) = x
- REAL_MUL_SUB2_CANCEL
-
|- ∀z x y. x * y + (z − x) * y = z * y
- REAL_MUL_SUB1_CANCEL
-
|- ∀z x y. y * x + y * (z − x) = y * z
- REAL_NEG_HALF
-
|- ∀x. x − x / 2 = x / 2
- REAL_NEG_THIRD
-
|- ∀x. x − x / 3 = 2 * x / 3
- REAL_DIV_DENOM_CANCEL
-
|- ∀x y z. x ≠ 0 ⇒ (y / x / (z / x) = y / z)
- REAL_DIV_DENOM_CANCEL2
-
|- ∀y z. y / 2 / (z / 2) = y / z
- REAL_DIV_DENOM_CANCEL3
-
|- ∀y z. y / 3 / (z / 3) = y / z
- REAL_DIV_INNER_CANCEL
-
|- ∀x y z. x ≠ 0 ⇒ (y / x * (x / z) = y / z)
- REAL_DIV_INNER_CANCEL2
-
|- ∀y z. y / 2 * (2 / z) = y / z
- REAL_DIV_INNER_CANCEL3
-
|- ∀y z. y / 3 * (3 / z) = y / z
- REAL_DIV_OUTER_CANCEL
-
|- ∀x y z. x ≠ 0 ⇒ (x / y * (z / x) = z / y)
- REAL_DIV_OUTER_CANCEL2
-
|- ∀y z. 2 / y * (z / 2) = z / y
- REAL_DIV_OUTER_CANCEL3
-
|- ∀y z. 3 / y * (z / 3) = z / y
- REAL_DIV_REFL2
-
|- 2 / 2 = 1
- REAL_DIV_REFL3
-
|- 3 / 3 = 1
- REAL_HALF_BETWEEN
-
|- (0 < 1 / 2 ∧ 1 / 2 < 1) ∧ 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1
- REAL_THIRDS_BETWEEN
-
|- (0 < 1 / 3 ∧ 1 / 3 < 1 ∧ 0 < 2 / 3 ∧ 2 / 3 < 1) ∧ 0 ≤ 1 / 3 ∧ 1 / 3 ≤ 1 ∧
0 ≤ 2 / 3 ∧ 2 / 3 ≤ 1
- REAL_LE_SUB_CANCEL2
-
|- ∀x y z. x − z ≤ y − z ⇔ x ≤ y
- REAL_ADD_SUB_ALT
-
|- ∀x y. x + y − y = x
- INFINITE_REAL_UNIV
-
|- INFINITE 𝕌(:real)
- add_rat
-
|- x / y + u / v =
if y = 0 then unint (x / y) + u / v
else if v = 0 then x / y + unint (u / v)
else if y = v then (x + u) / v
else (x * v + u * y) / (y * v)
- add_ratl
-
|- x / y + z = if y = 0 then unint (x / y) + z else (x + z * y) / y
- add_ratr
-
|- x + y / z = if z = 0 then x + unint (y / z) else (x * z + y) / z
- add_ints
-
|- (&n + &m = &(n + m)) ∧ (-&n + &m = if n ≤ m then &(m − n) else -&(n − m)) ∧
(&n + -&m = if n < m then -&(m − n) else &(n − m)) ∧
(-&n + -&m = -&(n + m))
- mult_rat
-
|- x / y * (u / v) =
if y = 0 then unint (x / y) * (u / v)
else if v = 0 then x / y * unint (u / v)
else x * u / (y * v)
- mult_ratl
-
|- x / y * z = if y = 0 then unint (x / y) * z else x * z / y
- mult_ratr
-
|- x * (y / z) = if z = 0 then x * unint (y / z) else x * y / z
- mult_ints
-
|- (&a * &b = &(a * b)) ∧ (-&a * &b = -&(a * b)) ∧ (&a * -&b = -&(a * b)) ∧
(-&a * -&b = &(a * b))
- pow_rat
-
|- (x pow 0 = 1) ∧ (0 pow NUMERAL (BIT1 n) = 0) ∧
(0 pow NUMERAL (BIT2 n) = 0) ∧
(&NUMERAL a pow NUMERAL n = &(NUMERAL a ** NUMERAL n)) ∧
(-&NUMERAL a pow NUMERAL n =
(if ODD (NUMERAL n) then numeric_negate else (λx. x))
(&(NUMERAL a ** NUMERAL n))) ∧ ((x / y) pow n = x pow n / y pow n)
- neg_rat
-
|- (-(x / y) = if y = 0 then -unint (x / y) else -x / y) ∧
(x / -y = if y = 0 then unint (x / y) else -x / y)
- eq_rat
-
|- (x / y = u / v) ⇔
if y = 0 then unint (x / y) = u / v
else if v = 0 then x / y = unint (u / v)
else if y = v then x = u
else x * v = y * u
- eq_ratl
-
|- (x / y = z) ⇔ if y = 0 then unint (x / y) = z else x = y * z
- eq_ratr
-
|- (z = x / y) ⇔ if y = 0 then z = unint (x / y) else y * z = x
- eq_ints
-
|- ((&n = &m) ⇔ (n = m)) ∧ ((-&n = &m) ⇔ (n = 0) ∧ (m = 0)) ∧
((&n = -&m) ⇔ (n = 0) ∧ (m = 0)) ∧ ((-&n = -&m) ⇔ (n = m))
- div_ratr
-
|- x / (y / z) = if (y = 0) ∨ (z = 0) then x / unint (y / z) else x * z / y
- div_ratl
-
|- x / y / z =
if y = 0 then unint (x / y) / z
else if z = 0 then unint (x / y / z)
else x / (y * z)
- div_rat
-
|- x / y / (u / v) =
if (u = 0) ∨ (v = 0) then x / y / unint (u / v)
else if y = 0 then unint (x / y) / (u / v)
else x * v / (y * u)
- le_rat
-
|- x / &n ≤ u / &m ⇔
if n = 0 then unint (x / 0) ≤ u / &m
else if m = 0 then x / &n ≤ unint (u / 0)
else &m * x ≤ &n * u
- le_ratl
-
|- x / &n ≤ u ⇔ if n = 0 then unint (x / 0) ≤ u else x ≤ &n * u
- le_ratr
-
|- x ≤ u / &m ⇔ if m = 0 then x ≤ unint (u / 0) else &m * x ≤ u
- le_int
-
|- (&n ≤ &m ⇔ n ≤ m) ∧ (-&n ≤ &m ⇔ T) ∧ (&n ≤ -&m ⇔ (n = 0) ∧ (m = 0)) ∧
(-&n ≤ -&m ⇔ m ≤ n)
- lt_rat
-
|- x / &n < u / &m ⇔
if n = 0 then unint (x / 0) < u / &m
else if m = 0 then x / &n < unint (u / 0)
else &m * x < &n * u
- lt_ratl
-
|- x / &n < u ⇔ if n = 0 then unint (x / 0) < u else x < &n * u
- lt_ratr
-
|- x < u / &m ⇔ if m = 0 then x < unint (u / 0) else &m * x < u
- lt_int
-
|- (&n < &m ⇔ n < m) ∧ (-&n < &m ⇔ n ≠ 0 ∨ m ≠ 0) ∧ (&n < -&m ⇔ F) ∧
(-&n < -&m ⇔ m < n)
- NUM_FLOOR_LE
-
|- 0 ≤ x ⇒ &flr x ≤ x
- NUM_FLOOR_LE2
-
|- 0 ≤ y ⇒ (x ≤ flr y ⇔ &x ≤ y)
- NUM_FLOOR_LET
-
|- flr x ≤ y ⇔ x < &y + 1
- NUM_FLOOR_DIV
-
|- 0 ≤ x ∧ 0 < y ⇒ &flr (x / y) * y ≤ x
- NUM_FLOOR_DIV_LOWERBOUND
-
|- 0 ≤ x ∧ 0 < y ⇒ x < &(flr (x / y) + 1) * y
- NUM_FLOOR_EQNS
-
|- (flr (&n) = n) ∧ (0 < m ⇒ (flr (&n / &m) = n DIV m))
- NUM_FLOOR_LOWER_BOUND
-
|- x < &n ⇔ flr (x + 1) ≤ n
- NUM_FLOOR_upper_bound
-
|- &n ≤ x ⇔ n < flr (x + 1)
- LE_NUM_CEILING
-
|- ∀x. x ≤ &clg x
- NUM_CEILING_LE
-
|- ∀x n. x ≤ &n ⇒ clg x ≤ n