Theory "real"

Signature

Definitions

real_of_num

⊢ 0 = real_0 ∧ ∀n. &SUC n = &n + real_1

real_sub

⊢ ∀x y. x − y = x + -y

real_lte

⊢ ∀x y. x ≤ y ⇔ ¬(y < x)

real_gt

⊢ ∀x y. x > y ⇔ y < x

real_ge

⊢ ∀x y. x ≥ y ⇔ y ≤ x

real_div

⊢ ∀x y. x / y = x * y⁻¹

abs

⊢ ∀x. abs x = if 0 ≤ x then x else -x

pow

⊢ (∀x. x pow 0 = 1) ∧ ∀x n. x pow SUC n = x * x pow n

sup

⊢ ∀P. sup P = @s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s

pos_def

⊢ ∀x. pos x = if 0 ≤ x then x else 0

min_def

⊢ ∀x y. min x y = if x ≤ y then x else y

max_def

⊢ ∀x y. max x y = if x ≤ y then y else x

inf_def

⊢ ∀p. inf p = -sup (λr. p (-r))

NUM_FLOOR_def

⊢ ∀x. flr x = LEAST n. &(n + 1) > x

NUM_CEILING_def

⊢ ∀x. clg x = LEAST n. x ≤ &n

Theorems

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 ⇒ x⁻¹ * x = 1

REAL_LT_MUL

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x * y

REAL_INV_0

⊢ 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 * 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 ⇒ x⁻¹ ≠ 0

REAL_INVINV

⊢ ∀x. x ≠ 0 ⇒ x⁻¹ ⁻¹ = x

REAL_LT_IMP_NE

⊢ ∀x y. x < y ⇒ x ≠ y

REAL_INV_POS

⊢ ∀x. 0 < x ⇒ 0 < 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 = y⁻¹

REAL_RINV_UNIQ

⊢ ∀x y. x * y = 1 ⇒ y = x⁻¹

REAL_INV_INV

⊢ ∀x. x⁻¹ ⁻¹ = x

REAL_INV_EQ_0

⊢ ∀x. x⁻¹ = 0 ⇔ x = 0

REAL_NEG_INV

⊢ ∀x. x ≠ 0 ⇒ -x⁻¹ = (-x)⁻¹

REAL_INV_1OVER

⊢ ∀x. x⁻¹ = 1 / x

REAL_LT_INV_EQ

⊢ ∀x. 0 < x⁻¹ ⇔ 0 < x

REAL_LE_INV_EQ

⊢ ∀x. 0 ≤ x⁻¹ ⇔ 0 ≤ x

REAL_LE_INV

⊢ ∀x. 0 ≤ x ⇒ 0 ≤ 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

⊢ 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 ⇒ y⁻¹ < 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 ⇒ (x * y)⁻¹ = x⁻¹ * 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 ⇒ x⁻¹ − 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 < 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 x⁻¹ = (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. (c pow n)⁻¹ = 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. x⁻¹ pow n = (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 ⇒ (x⁻¹ < y⁻¹ ⇔ y < x)

REAL_INV_INJ

⊢ ∀x y. x⁻¹ = 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_BASE

⊢ ∀r. r < 1 ⇒ flr r = 0

NUM_FLOOR_EQNS

⊢ flr (&n) = n ∧ flr (-&n) = 0 ∧ (0 < m ⇒ flr (&n / &m) = n DIV m) ∧
  (0 < m ⇒ flr (-&n / &m) = 0)

NUM_FLOOR_LOWER_BOUND

⊢ x < &n ⇔ flr (x + 1) ≤ n

NUM_FLOOR_upper_bound

⊢ &n ≤ x ⇔ n < flr (x + 1)

NUM_CEILING_NUM_FLOOR

⊢ ∀r. clg r = (let n = flr r in if r ≤ 0 ∨ r = &n then n else n + 1)

LE_NUM_CEILING

⊢ ∀x. x ≤ &clg x

NUM_CEILING_LE

⊢ ∀x n. x ≤ &n ⇒ clg x ≤ n