- HRAT_LT_REFL
-
|- ∀x. ¬hrat_lt x x
- HRAT_LT_TRANS
-
|- ∀x y z. hrat_lt x y ∧ hrat_lt y z ⇒ hrat_lt x z
- HRAT_LT_ANTISYM
-
|- ∀x y. ¬(hrat_lt x y ∧ hrat_lt y x)
- HRAT_LT_TOTAL
-
|- ∀x y. (x = y) ∨ hrat_lt x y ∨ hrat_lt y x
- HRAT_MUL_RID
-
|- ∀x. x hrat_mul hrat_1 = x
- HRAT_MUL_RINV
-
|- ∀x. x hrat_mul hrat_inv x = hrat_1
- HRAT_RDISTRIB
-
|- ∀x y z. (x hrat_add y) hrat_mul z = x hrat_mul z hrat_add y hrat_mul z
- HRAT_LT_ADDL
-
|- ∀x y. hrat_lt x (x hrat_add y)
- HRAT_LT_ADDR
-
|- ∀x y. hrat_lt y (x hrat_add y)
- HRAT_LT_GT
-
|- ∀x y. hrat_lt x y ⇒ ¬hrat_lt y x
- HRAT_LT_NE
-
|- ∀x y. hrat_lt x y ⇒ x ≠ y
- HRAT_EQ_LADD
-
|- ∀x y z. (x hrat_add y = x hrat_add z) ⇔ (y = z)
- HRAT_EQ_LMUL
-
|- ∀x y z. (x hrat_mul y = x hrat_mul z) ⇔ (y = z)
- HRAT_LT_ADD2
-
|- ∀u v x y. hrat_lt u x ∧ hrat_lt v y ⇒ hrat_lt (u hrat_add v) (x hrat_add y)
- HRAT_LT_LADD
-
|- ∀x y z. hrat_lt (z hrat_add x) (z hrat_add y) ⇔ hrat_lt x y
- HRAT_LT_RADD
-
|- ∀x y z. hrat_lt (x hrat_add z) (y hrat_add z) ⇔ hrat_lt x y
- HRAT_LT_MUL2
-
|- ∀u v x y. hrat_lt u x ∧ hrat_lt v y ⇒ hrat_lt (u hrat_mul v) (x hrat_mul y)
- HRAT_LT_LMUL
-
|- ∀x y z. hrat_lt (z hrat_mul x) (z hrat_mul y) ⇔ hrat_lt x y
- HRAT_LT_RMUL
-
|- ∀x y z. hrat_lt (x hrat_mul z) (y hrat_mul z) ⇔ hrat_lt x y
- HRAT_LT_LMUL1
-
|- ∀x y. hrat_lt (x hrat_mul y) y ⇔ hrat_lt x hrat_1
- HRAT_LT_RMUL1
-
|- ∀x y. hrat_lt (x hrat_mul y) x ⇔ hrat_lt y hrat_1
- HRAT_GT_LMUL1
-
|- ∀x y. hrat_lt y (x hrat_mul y) ⇔ hrat_lt hrat_1 x
- HRAT_LT_L1
-
|- ∀x y. hrat_lt (hrat_inv x hrat_mul y) hrat_1 ⇔ hrat_lt y x
- HRAT_LT_R1
-
|- ∀x y. hrat_lt (x hrat_mul hrat_inv y) hrat_1 ⇔ hrat_lt x y
- HRAT_GT_L1
-
|- ∀x y. hrat_lt hrat_1 (hrat_inv x hrat_mul y) ⇔ hrat_lt x y
- HRAT_INV_MUL
-
|- ∀x y. hrat_inv (x hrat_mul y) = hrat_inv x hrat_mul hrat_inv y
- HRAT_UP
-
|- ∀x. ∃y. hrat_lt x y
- HRAT_DOWN
-
|- ∀x. ∃y. hrat_lt y x
- HRAT_DOWN2
-
|- ∀x y. ∃z. hrat_lt z x ∧ hrat_lt z y
- HRAT_MEAN
-
|- ∀x y. hrat_lt x y ⇒ ∃z. hrat_lt x z ∧ hrat_lt z y
- ISACUT_HRAT
-
|- ∀h. isacut (cut_of_hrat h)
- EQUAL_CUTS
-
|- ∀X Y. (cut X = cut Y) ⇒ (X = Y)
- CUT_ISACUT
-
|- ∀X. isacut (cut X)
- CUT_NONEMPTY
-
|- ∀X. ∃x. cut X x
- CUT_BOUNDED
-
|- ∀X. ∃x. ¬cut X x
- CUT_DOWN
-
|- ∀X x y. cut X x ∧ hrat_lt y x ⇒ cut X y
- CUT_UP
-
|- ∀X x. cut X x ⇒ ∃y. cut X y ∧ hrat_lt x y
- CUT_UBOUND
-
|- ∀X x y. ¬cut X x ∧ hrat_lt x y ⇒ ¬cut X y
- CUT_STRADDLE
-
|- ∀X x y. cut X x ∧ ¬cut X y ⇒ hrat_lt x y
- CUT_NEARTOP_ADD
-
|- ∀X e. ∃x. cut X x ∧ ¬cut X (x hrat_add e)
- CUT_NEARTOP_MUL
-
|- ∀X u. hrat_lt hrat_1 u ⇒ ∃x. cut X x ∧ ¬cut X (u hrat_mul x)
- HREAL_INV_ISACUT
-
|- ∀X.
isacut
(λw. ∃d. hrat_lt d hrat_1 ∧ ∀x. cut X x ⇒ hrat_lt (w hrat_mul x) d)
- HREAL_ADD_ISACUT
-
|- ∀X Y. isacut (λw. ∃x y. (w = x hrat_add y) ∧ cut X x ∧ cut Y y)
- HREAL_MUL_ISACUT
-
|- ∀X Y. isacut (λw. ∃x y. (w = x hrat_mul y) ∧ cut X x ∧ cut Y y)
- HREAL_ADD_SYM
-
|- ∀X Y. X hreal_add Y = Y hreal_add X
- HREAL_MUL_SYM
-
|- ∀X Y. X hreal_mul Y = Y hreal_mul X
- HREAL_ADD_ASSOC
-
|- ∀X Y Z. X hreal_add (Y hreal_add Z) = X hreal_add Y hreal_add Z
- HREAL_MUL_ASSOC
-
|- ∀X Y Z. X hreal_mul (Y hreal_mul Z) = X hreal_mul Y hreal_mul Z
- HREAL_LDISTRIB
-
|- ∀X Y Z. X hreal_mul (Y hreal_add Z) = X hreal_mul Y hreal_add X hreal_mul Z
- HREAL_MUL_LID
-
|- ∀X. hreal_1 hreal_mul X = X
- HREAL_MUL_LINV
-
|- ∀X. hreal_inv X hreal_mul X = hreal_1
- HREAL_NOZERO
-
|- ∀X Y. X hreal_add Y ≠ X
- HREAL_LT_LEMMA
-
|- ∀X Y. X hreal_lt Y ⇒ ∃x. ¬cut X x ∧ cut Y x
- HREAL_SUB_ISACUT
-
|- ∀X Y. X hreal_lt Y ⇒ isacut (λw. ∃x. ¬cut X x ∧ cut Y (x hrat_add w))
- HREAL_SUB_ADD
-
|- ∀X Y. X hreal_lt Y ⇒ (Y hreal_sub X hreal_add X = Y)
- HREAL_LT_TOTAL
-
|- ∀X Y. (X = Y) ∨ X hreal_lt Y ∨ Y hreal_lt X
- HREAL_LT
-
|- ∀X Y. X hreal_lt Y ⇔ ∃D. Y = X hreal_add D
- HREAL_ADD_TOTAL
-
|- ∀X Y. (X = Y) ∨ (∃D. Y = X hreal_add D) ∨ ∃D. X = Y hreal_add D
- HREAL_SUP_ISACUT
-
|- ∀P.
(∃X. P X) ∧ (∃Y. ∀X. P X ⇒ X hreal_lt Y) ⇒ isacut (λw. ∃X. P X ∧ cut X w)
- HREAL_SUP
-
|- ∀P.
(∃X. P X) ∧ (∃Y. ∀X. P X ⇒ X hreal_lt Y) ⇒
∀Y. (∃X. P X ∧ Y hreal_lt X) ⇔ Y hreal_lt hreal_sup P