Theory extreal_base

⊢ ℚ꙳ = IMAGE Normal ℚ

⊢ ∀x. ceiling (Normal x) = LEAST n. x ≤ &n

⊢ (∀r. contract (Normal r) = r / (1 + abs r)) ∧ contract +∞ = 1 ∧
  contract −∞ = -1

⊢ ∀c. expand c =
      if 1 ≤ c then +∞ else if c ≤ -1 then −∞ else Normal (c / (1 − abs c))

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0.
           ∀ $var$('extreal').
             (∀a0.
                a0 = ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM) ∨
                a0 = ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ∨
                (∃a. a0 =
                     (λa.
                          ind_type$CONSTR (SUC (SUC 0)) a
                            (λn. ind_type$BOTTOM)) a) ⇒
                $var$('extreal') a0) ⇒
             $var$('extreal') a0) rep

⊢ abs =
  WFREC (@R. WF R)
    (λextreal_abs a.
         case a of −∞ => I +∞ | +∞ => I +∞ | Normal x => I (Normal (abs x)))

⊢ -−∞ = +∞ ∧ -+∞ = −∞ ∧ ∀x. -Normal x = Normal (-x)

⊢ (∀v v1 f. extreal_CASE −∞ v v1 f = v) ∧
  (∀v v1 f. extreal_CASE +∞ v v1 f = v1) ∧
  ∀a v v1 f. extreal_CASE (Normal a) v v1 f = f a

⊢ (∀r. Normal r / +∞ = Normal 0) ∧ (∀r. Normal r / −∞ = Normal 0) ∧
  ∀x r. r ≠ 0 ⇒ x / Normal r = x * (Normal r)⁻¹

⊢ −∞ ⁻¹ = Normal 0 ∧ +∞ ⁻¹ = Normal 0 ∧
  ∀r. r ≠ 0 ⇒ (Normal r)⁻¹ = Normal r⁻¹

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

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

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

⊢ ∀n. &n = Normal (&n)

⊢ (∀a n. Normal a pow n = Normal (a pow n)) ∧
  (∀n. +∞ pow n = if n = 0 then Normal 1 else +∞) ∧
  ∀n. −∞ pow n = if n = 0 then Normal 1 else if EVEN n then +∞ else −∞

⊢ extreal_size −∞ = 0 ∧ extreal_size +∞ = 0 ∧
  ∀a. extreal_size (Normal a) = 1

⊢ (∀x. sqrt (Normal x) = Normal (sqrt x)) ∧ sqrt +∞ = +∞

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

⊢ ∀x. real x = if x = −∞ ∨ x = +∞ then 0 else @r. x = Normal r

⊢ ∀s. real_set s = {real x | x ≠ +∞ ∧ x ≠ −∞ ∧ x ∈ s}

⊢ ∀x y. x ∈ ℚ꙳ ∧ y ∈ ℚ꙳ ⇒ x + y ∈ ℚ꙳

⊢ ∀x. Normal x ≤ &ceiling (Normal x)

⊢ ∀x. 0 ≤ x ⇒ &ceiling (Normal x) < Normal x + 1

⊢ ∀z x. x ∈ ℚ꙳ ⇒ &z * x ∈ ℚ꙳ ∧ -&z * x ∈ ℚ꙳

⊢ ∀c. countable c ⇔ c = ∅ ∨ ∃f. c = IMAGE f ℚ꙳

⊢ ∀x y. x ∈ ℚ꙳ ∧ y ∈ ℚ꙳ ∧ y ≠ 0 ⇒ x / y ∈ ℚ꙳

⊢ ∀x. 0 < x ⇒ ∀y. y ≠ +∞ ⇒ ∃n. y < &n * x

⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ < x

⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ ≤ x

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y = x + z ⇔ y = z)

⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ⇒ (x + z = y + z ⇔ x = y)

⊢ ∀x. x ∈ ℚ꙳ ∧ x ≠ 0 ⇒ 1 / x ∈ ℚ꙳

⊢ ∀x y. x ∈ ℚ꙳ ∧ y ∈ ℚ꙳ ⇒ x * y ∈ ℚ꙳

⊢ ∀n. &n ∈ ℚ꙳ ∧ -&n ∈ ℚ꙳

⊢ ∀x. x ∈ ℚ꙳ ⇒ -x ∈ ℚ꙳

⊢ countable ℚ꙳

⊢ ∀x y. x < y ⇒ ∃r. r ∈ ℚ꙳ ∧ x < r ∧ r < y

⊢ ∀x y. x < y ⇒ ∃r. r ∈ ℚ ∧ x < Normal r ∧ Normal r < y

⊢ ∀x y. 0 ≤ x ∧ x < y ⇒ ∃r. r ∈ ℚ꙳ ∧ x < r ∧ r < y

⊢ INFINITE ℚ꙳

⊢ ∀x. x ∈ ℚ꙳ ⇒ ∃y. x = Normal y

⊢ ℚ꙳ =
  {x | ∃a b. x = &a / &b ∧ 0 < &b} ∪ {x | ∃a b. x = -(&a / &b) ∧ 0 < &b}

⊢ ∀x. x ≠ +∞ ⇒ ∃n. x ≤ &n

⊢ ∀x. x ≠ −∞ ⇒ ∃n. -&n ≤ x

⊢ ∀x y. x ∈ ℚ꙳ ∧ y ∈ ℚ꙳ ⇒ x − y ∈ ℚ꙳

⊢ abs 0 = 0

⊢ ∀x. abs (abs x) = abs x

⊢ ∀x k. abs x ≤ k ⇔ -k ≤ x ∧ x ≤ k

⊢ ∀x k. abs x < k ⇔ -k < x ∧ x < k

⊢ ∀x. abs (contract x) ≤ 1

⊢ ∀r. abs (contract (Normal r)) < 1

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ 0 ⇒ abs (x / y) = abs x / abs y

⊢ ∀x y. y ≠ 0 ⇒ abs (x / Normal y) = abs x / Normal (abs y)

⊢ ∀x. abs x = 0 ⇔ x = 0

⊢ ∀x. 0 < abs x ⇔ x ≠ 0

⊢ ∀x. abs x ≤ 0 ⇔ x = 0

⊢ ∀x y. abs (x * y) ≤ Normal (1 / 2) * (x² + y²)

⊢ ∀x. abs x ≤ x² + 1

⊢ ∀x. abs x = max x (-x)

⊢ ∀x y. abs (x * y) = abs x * abs y

⊢ ∀x. x < 0 ⇒ abs x = -x

⊢ ∀x. x ≤ 0 ⇒ abs x = -x

⊢ ∀x. abs (-x) = abs x

⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ abs x ≠ +∞ ∧ abs x ≠ −∞

⊢ ∀x. abs x ≠ 0 ⇔ x ≠ 0

⊢ ∀x. 0 ≤ abs x

⊢ ∀x. (abs x)² = x²

⊢ ∀x n m. n ≤ m ⇒ abs x pow n ≤ 1 + abs x pow m

⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ abs (real x) = real (abs x)

⊢ ∀x. abs x = x ⇔ 0 ≤ x

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x − y) = abs (y − x)

⊢ ∀x y. abs (x − y) = abs (y − x)

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x + y) ≤ abs x + abs y

⊢ ∀x y. abs (x + y) ≤ abs x + abs y

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs (x − y) ≤ abs x + abs y

⊢ ∀x y. abs (x − y) ≤ abs x + abs y

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs x ≤ abs y + abs (x − y)

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ abs x ≤ abs y + abs (y − x)

⊢ ∀x y. abs x ≤ abs y + abs (x − y)

⊢ ∀x y. abs x ≤ abs y + abs (y − x)

⊢ ∀x k. 0 ≤ k ⇒ (k ≤ abs x ⇔ x ≤ -k ∨ k ≤ x)

⊢ ∀a b c d.
    a ≠ −∞ ∧ b ≠ −∞ ∧ c ≠ −∞ ∧ d ≠ −∞ ⇒ a + b + (c + d) = a + c + (b + d)

⊢ ∀a b c d.
    a ≠ −∞ ∧ b ≠ +∞ ∧ c ≠ −∞ ∧ d ≠ +∞ ⇒ a − b + (c − d) = a + c − (b + d)

⊢ ∀x y z.
    x ≠ −∞ ∧ y ≠ −∞ ∧ z ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ∧ z ≠ +∞ ⇒
    x + (y + z) = x + y + z

⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ x + y = y + x

⊢ ∀x y. Normal x + y = y + Normal x

⊢ (∀x. x ≠ −∞ ⇒ x + +∞ = +∞ ∧ +∞ + x = +∞) ∧
  ∀x. x ≠ +∞ ⇒ x + −∞ = −∞ ∧ −∞ + x = −∞

⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ∨ y ≤ 0 ∧ z ≤ 0 ⇒ x * (y + z) = x * y + x * z

⊢ ∀x y z. y ≤ 0 ∧ z ≤ 0 ⇒ x * (y + z) = x * y + x * z

⊢ ∀r y z.
    y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
    Normal r * (y + z) = Normal r * y + Normal r * z

⊢ ∀r y z.
    y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
    Normal r * (y + z) = Normal r * y + Normal r * z

⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ⇒ x * (y + z) = x * y + x * z

⊢ ∀x. 0 + x = x

⊢ ∀x y. (x ≠ −∞ ∧ y ≠ −∞ ⇒ x + y ≠ −∞) ∧ (x ≠ +∞ ∧ y ≠ +∞ ⇒ x + y ≠ +∞)

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ (x + y)² = x² + y² + 2 * x * y

⊢ ∀x y. 0 < x ∧ x ≠ +∞ ∧ 0 ≤ y ⇒ (x + y)² = x² + y² + 2 * x * y

⊢ ∀x y z. 0 ≤ y ∧ 0 ≤ z ∨ y ≤ 0 ∧ z ≤ 0 ⇒ (y + z) * x = y * x + z * x

⊢ ∀x y z.
    y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
    (y + z) * Normal x = y * Normal x + z * Normal x

⊢ ∀x y z.
    y ≠ +∞ ∧ z ≠ +∞ ∨ y ≠ −∞ ∧ z ≠ −∞ ⇒
    (y + z) * Normal x = y * Normal x + z * Normal x

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ real (x + y) = real x + real y

⊢ ∀x. x + 0 = x

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ x + y − y = x

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ y + x − y = x

⊢ ∀x r. x + Normal r − Normal r = x

⊢ ∀x y. contract x = contract y ⇔ x = y

⊢ ∀x y. contract x ≤ contract y ⇔ x ≤ y

⊢ ∀x. contract (-x) = -contract x

⊢ DATATYPE (extreal −∞ +∞ Normal)

⊢ ∀x y z.
    x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ∧ z ≠ 0 ⇒ x / z + y / z = (x + y) / z

⊢ ∀x y z.
    (x ≠ +∞ ∧ y ≠ +∞ ∨ x ≠ −∞ ∧ y ≠ −∞) ∧ z ≠ 0 ∧ z ≠ +∞ ∧ z ≠ −∞ ⇒
    x / z + y / z = (x + y) / z

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ x / y = y⁻¹ * x

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ x / y = x * y⁻¹

⊢ ∀x. x ≠ +∞ ∧ x ≠ −∞ ⇒ x / +∞ = 0 ∧ x / −∞ = 0

⊢ ∀x r. r ≠ 0 ⇒ x = x / Normal r * Normal r

⊢ ∀x y. y ≠ 0 ⇒ Normal x / y ≠ +∞ ∧ Normal x / y ≠ −∞

⊢ ∀x. x / 1 = x

⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x / x = 1

⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ x / x = 1

⊢ ∀x y z.
    x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ∧ z ≠ 0 ⇒ x / z − y / z = (x − y) / z

⊢ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0

⊢ ∀a b c d.
    b ≠ −∞ ∧ b ≠ +∞ ∧ c ≠ −∞ ∧ c ≠ +∞ ⇒ (a + b = c + d ⇔ a − c = d − b)

⊢ ∀x y. -x = -y ⇔ x = y

⊢ ∀x y z. 0 < z ⇒ (x = y / Normal z ⇔ x * Normal z = y)

⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ⇒ (x = y − z ⇔ x + z = y)

⊢ ∀x y z. x = y − Normal z ⇔ x + Normal z = y

⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ⇒ (x − y = z ⇔ x = z + y)

⊢ ∀x y z. x = Normal z − y ⇔ y = Normal z − x

⊢ ∀x. expand (contract x) = x

⊢ ∀a a'. Normal a = Normal a' ⇔ a = a'

⊢ ∀f0 f1 f2. ∃fn. fn −∞ = f0 ∧ fn +∞ = f1 ∧ ∀a. fn (Normal a) = f2 a

⊢ abs (Normal x) = Normal (abs x) ∧ abs −∞ = +∞ ∧ abs +∞ = +∞

⊢ ∀P. (∀x. P (Normal x)) ∧ P −∞ ∧ P +∞ ⇒ ∀v. P v

⊢ Normal x + Normal y = Normal (x + y) ∧ Normal v0 + −∞ = −∞ ∧
  Normal v0 + +∞ = +∞ ∧ −∞ + Normal v1 = −∞ ∧ +∞ + Normal v1 = +∞ ∧
  −∞ + −∞ = −∞ ∧ +∞ + +∞ = +∞

⊢ ∀x y. Normal x + Normal y = Normal (x + y)

⊢ ∀P. (∀x y. P (Normal x) (Normal y)) ∧ (∀v0. P (Normal v0) −∞) ∧
      (∀v0. P (Normal v0) +∞) ∧ (∀v1. P −∞ (Normal v1)) ∧
      (∀v1. P +∞ (Normal v1)) ∧ P −∞ −∞ ∧ P +∞ +∞ ∧ P −∞ +∞ ∧ P +∞ −∞ ⇒
      ∀v v1. P v v1

⊢ ∀M M' v v1 f.
    M = M' ∧ (M' = −∞ ⇒ v = v') ∧ (M' = +∞ ⇒ v1 = v1') ∧
    (∀a. M' = Normal a ⇒ f a = f' a) ⇒
    extreal_CASE M v v1 f = extreal_CASE M' v' v1' f'

⊢ extreal_CASE x v v1 f = v' ⇔
  x = −∞ ∧ v = v' ∨ x = +∞ ∧ v1 = v' ∨ ∃r. x = Normal r ∧ f r = v'

⊢ ∀x. x = −∞ ∨ x = +∞ ∨ ∃r. x = Normal r

⊢ −∞ ≠ +∞ ∧ (∀a. −∞ ≠ Normal a) ∧ ∀a. +∞ ≠ Normal a

⊢ ∀x y. y ≠ 0 ⇒ Normal x / Normal y = Normal (x / y)

⊢ ∀x. x + x = 2 * x

⊢ ∀x. Normal x = 0 ⇔ x = 0

⊢ ∀P. P −∞ ∧ P +∞ ∧ (∀r. P (Normal r)) ⇒ ∀e. P e

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

⊢ (Normal x ≤ Normal y ⇔ x ≤ y) ∧ (−∞ ≤ v0 ⇔ T) ∧ (+∞ ≤ +∞ ⇔ T) ∧
  (Normal v5 ≤ +∞ ⇔ T) ∧ (+∞ ≤ −∞ ⇔ F) ∧ (Normal v6 ≤ −∞ ⇔ F) ∧
  (+∞ ≤ Normal v8 ⇔ F)

⊢ ∀x y. Normal x ≤ Normal y ⇔ x ≤ y

⊢ ∀P. (∀x y. P (Normal x) (Normal y)) ∧ (∀v0. P −∞ v0) ∧ P +∞ +∞ ∧
      (∀v5. P (Normal v5) +∞) ∧ P +∞ −∞ ∧ (∀v6. P (Normal v6) −∞) ∧
      (∀v8. P +∞ (Normal v8)) ⇒
      ∀v v1. P v v1

⊢ ∀x y. Normal x < Normal y ⇔ x < y

⊢ ∀a b. max (Normal a) (Normal b) = Normal (max a b)

⊢ ∀x y. x < y ⇒ ∃z. x < z ∧ z < y

⊢ ∀a b. min (Normal a) (Normal b) = Normal (min a b)

⊢ −∞ * −∞ = +∞ ∧ −∞ * +∞ = −∞ ∧ +∞ * −∞ = −∞ ∧ +∞ * +∞ = +∞ ∧
  Normal x * −∞ = (if x = 0 then Normal 0 else if 0 < x then −∞ else +∞) ∧
  −∞ * Normal y = (if y = 0 then Normal 0 else if 0 < y then −∞ else +∞) ∧
  Normal x * +∞ = (if x = 0 then Normal 0 else if 0 < x then +∞ else −∞) ∧
  +∞ * Normal y = (if y = 0 then Normal 0 else if 0 < y then +∞ else −∞) ∧
  Normal x * Normal y = Normal (x * y)

⊢ ∀x y. Normal x * Normal y = Normal (x * y)

⊢ ∀P. P −∞ −∞ ∧ P −∞ +∞ ∧ P +∞ −∞ ∧ P +∞ +∞ ∧ (∀x. P (Normal x) −∞) ∧
      (∀y. P −∞ (Normal y)) ∧ (∀x. P (Normal x) +∞) ∧
      (∀y. P +∞ (Normal y)) ∧ (∀x y. P (Normal x) (Normal y)) ⇒
      ∀v v1. P v v1

⊢ ∀ee. ee = −∞ ∨ ee = +∞ ∨ ∃r. ee = Normal r

⊢ ∀x. Normal x ≠ −∞ ∧ Normal x ≠ +∞

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

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

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

⊢ ∀a n. Normal a pow n = Normal (a pow n)

⊢ ∀x y. x ≠ −∞ ∧ y ≠ +∞ ∨ x ≠ +∞ ∧ y ≠ −∞ ⇒ x − y = x + -y

⊢ Normal x − Normal y = Normal (x − y) ∧ +∞ − Normal x = +∞ ∧
  −∞ − Normal x = −∞ ∧ Normal x − −∞ = +∞ ∧ Normal x − +∞ = −∞ ∧
  −∞ − +∞ = −∞ ∧ +∞ − −∞ = +∞

⊢ ∀x y. Normal x − Normal y = Normal (x − y)

⊢ 4 * (1 / 4) = 1

⊢ ((0 < 1 / 4 ∧ 1 / 4 < 1) ∧ 0 < 3 / 4 ∧ 3 / 4 < 1) ∧
  (0 ≤ 1 / 4 ∧ 1 / 4 ≤ 1) ∧ 0 ≤ 3 / 4 ∧ 3 / 4 ≤ 1

⊢ (0 < 1 / 2 ∧ 1 / 2 < 1) ∧ 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1

⊢ 2 * (1 / 2) = 1

⊢ ∀x. x / 2 + x / 2 = x

⊢ 1 / 2 ≠ +∞ ∧ 1 / 2 ≠ −∞

⊢ ∀r. 0 < r ⇒ +∞ / Normal r = +∞ ∧ −∞ / Normal r = −∞

⊢ +∞ ² = +∞ ∧ −∞ ² = +∞

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

⊢ +∞ ⁻¹ = 0 ∧ −∞ ⁻¹ = 0

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ = y⁻¹ ⇔ x = y)

⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x⁻¹ ⁻¹ = x

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ ≤ y⁻¹ ⇔ y ≤ x)

⊢ ∀x y. 0 < y ∧ y ≤ x ⇒ x⁻¹ ≤ y⁻¹

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (x⁻¹ < y⁻¹ ⇔ y < x)

⊢ ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ (x * y)⁻¹ = x⁻¹ * y⁻¹

⊢ ∀x. x ≠ 0 ⇒ x⁻¹ ≠ +∞ ∧ x⁻¹ ≠ −∞

⊢ 1⁻¹ = 1

⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ 0 < 1 / x

⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ 0 < x⁻¹

⊢ ∀x. x ≠ 0 ⇒ (0 < x⁻¹ ⇔ x ≠ +∞ ∧ 0 ≤ x)

⊢ ∀x y z. 0 < z ∧ z < +∞ ⇒ (x / z = y ⇔ x = y * z)

⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ∧ x ≤ y ⇒ x / z ≤ y / z

⊢ 0 ≤ 1

⊢ 0 ≤ 2

⊢ ∀x. x ≤ abs x ∧ -x ≤ abs x

⊢ ∀k x. k ≤ abs x ⇔ x ≤ -k ∨ k ≤ x

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y

⊢ ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z

⊢ ∀x y. x ≤ 0 ∧ y ≤ 0 ⇒ x + y ≤ 0

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (y ≤ x + y ⇔ 0 ≤ x)

⊢ ∀x y. 0 ≤ x ⇒ y ≤ x + y

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x ≤ x + y ⇔ 0 ≤ y)

⊢ ∀x y. 0 ≤ y ⇒ x ≤ x + y

⊢ ∀x y. x ≤ y ∧ y ≤ x ⇔ x = y

⊢ ∀y z. 0 ≤ y ∧ 0 < z ⇒ 0 ≤ y / Normal z

⊢ (∀x. −∞ ≤ x ∧ x ≤ +∞) ∧ (∀x. x ≤ −∞ ⇔ x = −∞) ∧ ∀x. +∞ ≤ x ⇔ x = +∞

⊢ ∀x. 0 < x ⇒ 0 ≤ x⁻¹

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y ≤ x + z ⇔ y ≤ z)

⊢ ∀x y z. y ≤ z ⇒ x + y ≤ x + z

⊢ ∀x y z. 0 < x ⇒ (y ≤ z * Normal x ⇔ y / Normal x ≤ z)

⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ⇒ (x * y ≤ x * z ⇔ y ≤ z)

⊢ ∀x y z. 0 ≤ z ∧ x ≤ y ⇒ z * x ≤ z * y

⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ (-x ≤ y ⇔ 0 ≤ x + y)

⊢ ∀x y z. y ≤ z ⇒ x − z ≤ x − y

⊢ ∀x y. x ≤ y ⇔ x < y ∨ x = y

⊢ ∀z x y. z ≤ max x y ⇔ z ≤ x ∨ z ≤ y

⊢ ∀x y. x ≤ max x y

⊢ ∀x y. y ≤ max x y

⊢ ∀z x y. z ≤ min x y ⇔ z ≤ x ∧ z ≤ y

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

⊢ ∀x1 x2 y1 y2. 0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≤ x2 ∧ y1 ≤ y2 ⇒ x1 * y1 ≤ x2 * y2

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

⊢ ∀x y. -x ≤ -y ⇔ y ≤ x

⊢ (∀x. 0 ≤ x ⇒ x ≠ −∞) ∧ ∀x. x ≤ 0 ⇒ x ≠ +∞

⊢ ∀n. 0 ≤ &n

⊢ ∀x. 0 ≤ x²

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y + x ≤ z + x ⇔ y ≤ z)

⊢ ∀x y z. y ≤ z ⇒ y + x ≤ z + x

⊢ ∀x y z. 0 < x ⇒ (y * Normal x ≤ z ⇔ y ≤ z / Normal x)

⊢ ∀x y. 0 ≤ x ∧ x ≤ y ∧ y ≠ +∞ ⇒ real x ≤ real y

⊢ ∀x. x ≤ x

⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ⇒ (x * z ≤ y * z ⇔ x ≤ y)

⊢ ∀x y z. 0 ≤ z ∧ x ≤ y ⇒ x * z ≤ y * z

⊢ ∀x y z. z ≠ +∞ ∧ z ≠ −∞ ⇒ (x − z ≤ y − z ⇔ x ≤ y)

⊢ ∀x y z. x ≤ y ⇒ x − z ≤ y − z

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y ≤ z − x ⇔ y + x ≤ z)

⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ −∞ ⇒ (y ≤ z − x ⇔ y + x ≤ z)

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y + x ≤ z ⇒ y ≤ z − x

⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ y + x ≤ z ⇒ y ≤ z − x

⊢ ∀x y. x ≤ y ∨ y ≤ x

⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z

⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y

⊢ ∀w x y z. w ≠ −∞ ∧ w ≠ +∞ ∧ w ≤ x ∧ y < z ⇒ w + y < x + z

⊢ ∀w x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ w ≤ x ∧ y < z ⇒ w + y < x + z

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

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

⊢ ∀x y. x ≤ y ∨ y < x

⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z

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

⊢ 0 < 1

⊢ 0 < 2

⊢ -1 < 0

⊢ ∀k x. k < abs x ⇔ x < -k ∨ k < x

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

⊢ ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z

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

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (y < x + y ⇔ 0 < x)

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x < x + y ⇔ 0 < y)

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ 0 < y ⇒ x < x + y

⊢ ∀x y. ¬(x < y ∧ y < x)

⊢ ∀y z. 0 < y ∧ 0 < z ⇒ 0 < y / Normal z

⊢ ∀x y. x < y ⇒ x ≤ y

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

⊢ −∞ < +∞ ∧ (∀x. −∞ < Normal x ∧ Normal x < +∞) ∧
  (∀x. ¬(x < −∞) ∧ ¬(+∞ < x)) ∧ (∀x. x ≠ +∞ ⇔ x < +∞) ∧ ∀x. x ≠ −∞ ⇔ −∞ < x

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x + y < x + z ⇔ y < z)

⊢ ∀x y z. 0 < z ⇒ (x / Normal z < y ⇔ x < y * Normal z)

⊢ ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y

⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ⇒ (x * y < x * z ⇔ y < z)

⊢ ∀x y z. 0 < x ∧ x ≠ +∞ ∧ y < z ⇒ x * y < x * z

⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ⇒ (x − z < x − y ⇔ y < z)

⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ∧ y < z ⇒ x − z < x − y

⊢ ∀x y z. x < max y z ⇔ x < y ∨ x < z

⊢ ∀x b d. x < max b d ∧ b ≤ x ⇒ x < d

⊢ ∀x y z. z < min x y ⇔ z < x ∧ z < y

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

⊢ ∀x1 x2 y1 y2.
    0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≠ +∞ ∧ y1 ≠ +∞ ∧ x1 < x2 ∧ y1 < y2 ⇒
    x1 * y1 < x2 * y2

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

⊢ ∀x y. -x < -y ⇔ y < x

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y + x < z + x ⇔ y < z)

⊢ ∀x y z. 0 < z ⇒ (x < y / Normal z ⇔ x * Normal z < y)

⊢ ∀x y z. z < 0 ⇒ (y / Normal z < x ⇔ x * Normal z < y)

⊢ ∀x. ¬(x < x)

⊢ ∀x y z. 0 < z ∧ z ≠ +∞ ⇒ (x * z < y * z ⇔ x < y)

⊢ ∀x y z. x < y ∧ 0 < z ∧ z ≠ +∞ ⇒ x * z < y * z

⊢ ∀x y z. z ≠ +∞ ∧ z ≠ −∞ ⇒ (x − z < y − z ⇔ x < y)

⊢ ∀x y z. z ≠ +∞ ∧ z ≠ −∞ ∧ x < y ⇒ x − z < y − z

⊢ ∀x y z. x ≠ −∞ ∧ y ≠ −∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y + x < z ⇔ y < z − x)

⊢ ∀x y z. x ≠ +∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y + x < z ⇔ y < z − x)

⊢ ∀x y z. x ≠ −∞ ∧ y ≠ −∞ ∧ y + x < z ⇒ y < z − x

⊢ ∀x y z. x ≠ +∞ ∧ y ≠ +∞ ∧ y + x < z ⇒ y < z − x

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y + x < z ⇒ y < z − x

⊢ ∀x y. x = y ∨ x < y ∨ y < x

⊢ ∀x y z. x < y ∧ y < z ⇒ x < z

⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y

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

⊢ ∀x y. x < y ∨ y ≤ x

⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z

⊢ ∀x. 0 ≤ x ⇒ max 0 x = x

⊢ ∀x y. max x y = max y x

⊢ ∀x. max x +∞ = +∞ ∧ max +∞ x = +∞ ∧ max −∞ x = x ∧ max x −∞ = x

⊢ ∀z x y. max x y ≤ z ⇔ x ≤ z ∧ y ≤ z

⊢ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ max x1 x2 ≤ max y1 y2

⊢ ∀x y z. max x y < z ⇔ x < z ∧ y < z

⊢ ∀x y. x ≤ y ∨ x < y ⇒ max x y = y ∧ max y x = y

⊢ ∀x. max x x = x

⊢ ∀x y. min x y = min y x

⊢ ∀x. min x +∞ = x ∧ min +∞ x = x ∧ min −∞ x = −∞ ∧ min x −∞ = −∞

⊢ ∀z x y. min x y ≤ z ⇔ x ≤ z ∨ y ≤ z

⊢ ∀x y. min x y ≤ x

⊢ ∀x y. min x y ≤ y

⊢ ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ min x1 x2 ≤ min y1 y2

⊢ ∀x a c. min a c ≤ x ∧ x < a ⇒ c ≤ x

⊢ ∀x y. x ≤ y ∨ x < y ⇒ min x y = x ∧ min y x = x

⊢ ∀x. min x x = x

⊢ ∀x y z. x * (y * z) = x * y * z

⊢ ∀x y. x * y = y * x

⊢ ∀x r. r ≠ 0 ⇒ x = x * Normal r / Normal r

⊢ ∀x. 0 < x ⇒ +∞ * x = +∞ ∧ x * +∞ = +∞ ∧ −∞ * x = −∞ ∧ x * −∞ = −∞

⊢ ∀x. x < 0 ⇒ +∞ * x = −∞ ∧ x * +∞ = −∞ ∧ −∞ * x = +∞ ∧ x * −∞ = +∞

⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ⇒ (x * y = x * z ⇔ x = 0 ∨ y = z)

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

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

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

⊢ ∀x. x ≠ 0 ∧ x ≠ +∞ ∧ x ≠ −∞ ⇒ x⁻¹ * x = 1

⊢ ∀x. 0 < x ∧ x ≠ +∞ ⇒ x⁻¹ * x = 1

⊢ ∀x y. -x * y = -(x * y)

⊢ ∀x. 1 * x = x

⊢ ∀x. 0 < x ⇒ +∞ * x = +∞

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

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

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

⊢ ∀x. 0 * x = 0

⊢ (∀c y. 0 ≤ c ∧ y ≠ −∞ ⇒ Normal c * y ≠ −∞) ∧
  (∀c y. 0 ≤ c ∧ y ≠ +∞ ⇒ Normal c * y ≠ +∞) ∧
  (∀c y. c ≤ 0 ∧ y ≠ −∞ ⇒ Normal c * y ≠ +∞) ∧
  ∀c y. c ≤ 0 ∧ y ≠ +∞ ⇒ Normal c * y ≠ −∞

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ x * y ≠ −∞ ∧ x * y ≠ +∞

⊢ ∀x y z. x ≠ +∞ ∧ x ≠ −∞ ⇒ (y * x = z * x ⇔ x = 0 ∨ y = z)

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ real (x * y) = real x * real y

⊢ ∀x y. x * -y = -(x * y)

⊢ ∀x. x * 1 = x

⊢ ∀x. 0 < x ⇒ x * +∞ = +∞

⊢ ∀x. x * 0 = 0

⊢ 0 ≠ 1

⊢ 0 ≠ 2

⊢ -0 = 0

⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ -(x + y) = -x + -y

⊢ ∀x. -x = 0 ⇔ x = 0

⊢ ∀x. -x = -1 * x

⊢ ∀x. -x = Normal (-1) * x

⊢ ∀x y. -x * -y = x * y

⊢ ∀x. --x = x

⊢ ∀x. x ≤ 0 ⇒ x ≠ +∞

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∨ y ≠ −∞ ∧ y ≠ +∞ ⇒ -(x − y) = y − x

⊢ Normal 0 = 0

⊢ Normal 1 = 1

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

⊢ ∀x. x ≠ −∞ ∧ x ≠ +∞ ⇒ Normal (real x) = x

⊢ ∀s. s ∩ IMAGE Normal 𝕌(:real) = IMAGE Normal (real_set s)

⊢ ∀n. &n < +∞

⊢ ∀n. &n ≠ −∞ ∧ &n ≠ +∞

⊢ ∀n. 1 pow n = 1

⊢ ∀x. 0 ≤ x ⇒ x ≠ −∞

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ (x ≤ y ⇔ x² ≤ y²)

⊢ ∀x. 0 ≤ x ⇒ sqrt x² = x

⊢ ∀x. x pow 0 = 1

⊢ ∀x. x pow 1 = x

⊢ ∀x. x² = x * x

⊢ ∀x. x² = abs x * abs x

⊢ ∀x n m. x pow (n + m) = x pow n * x pow m

⊢ ∀n x y. x ≠ +∞ ∧ x ≠ −∞ ∧ 0 < y ⇒ (x / y) pow n = x pow n / y pow n

⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ 0 ≤ y ⇒ (x = y ⇔ x pow n = y pow n)

⊢ ∀n y. y ≠ 0 ⇒ (y pow n)⁻¹ = y⁻¹ pow n

⊢ ∀n x y. 0 ≤ x ∧ x ≤ y ⇒ x pow n ≤ y pow n

⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ 0 ≤ y ⇒ (x ≤ y ⇔ x pow n ≤ y pow n)

⊢ ∀x n m. 1 ≤ x ∧ n ≤ m ⇒ x pow n ≤ x pow m

⊢ ∀n x y. 0 ≤ x ∧ x < y ⇒ x pow SUC n < y pow SUC n

⊢ ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ x < y ⇒ x pow n < y pow n

⊢ ∀n. -1 pow (2 * n) = 1

⊢ ∀n x y. (x * y) pow n = x pow n * y pow n

⊢ ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)

⊢ ∀n x. x ≠ −∞ ∧ x ≠ +∞ ⇒ x pow n ≠ −∞ ∧ x pow n ≠ +∞

⊢ ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)

⊢ ∀n x. 0 ≤ x ⇒ 0 ≤ x pow n

⊢ ∀n x. 0 < x ⇒ 0 < x pow n

⊢ ∀x m n. (x pow m) pow n = x pow (m * n)

⊢ ∀x n. x ≠ +∞ ∧ x ≠ −∞ ⇒ real x pow n = real (x pow n)

⊢ ∀n x. x pow SUC n = 0 ⇔ x = 0

⊢ ∀n x. x pow n = 0 ⇒ x = 0

⊢ ∀n m. m ≠ 0 ⇒ &n / &m = Normal (&n / &m)

⊢ ∀r. r ∈ ℚ꙳ ⇒ r ≠ −∞ ∧ r ≠ +∞

⊢ ∀x y z. 0 < z ∧ z < +∞ ⇒ (x = y / z ⇔ x * z = y)

⊢ real 0 = 0

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ (real x = real y ⇔ x = y)

⊢ real +∞ = 0 ∧ real −∞ = 0

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ (real x ≤ real y ⇔ x ≤ y)

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ (real x < real y ⇔ x < y)

⊢ ∀x. real (Normal x) = x

⊢ ∀x. 0 ≤ x ⇒ 0 ≤ real x

⊢ ∀s t. real_set (s ∩ t) = real_set s ∩ real_set t

⊢ ∀s t. real_set (s ∪ t) = real_set s ∪ real_set t

⊢ real_set ∅ = ∅

⊢ real_set {+∞} = ∅ ∧ real_set {−∞} = ∅

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

⊢ sqrt 0 = 0

⊢ sqrt 1 = 1

⊢ ∀n. sqrt (&n) ≤ &n

⊢ ∀x. 1 ≤ x ⇒ sqrt x ≤ x

⊢ ∀x y. 0 ≤ x ∧ x ≤ y ⇒ sqrt x ≤ sqrt y

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ sqrt (x * y) = sqrt x * sqrt y

⊢ ∀x. 0 ≤ x ⇒ 0 ≤ sqrt x

⊢ ∀x. 0 < x ⇒ 0 < sqrt x

⊢ ∀x. 0 < x ⇒ sqrt x ≠ 0

⊢ ∀x. (sqrt x)² = x ⇔ 0 ≤ x

⊢ ∀x y. x − y = 0 ⇒ x = y

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ x − y + y = x

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ x + (y − x) = y

⊢ ∀x r. x − Normal r + Normal r = x

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ x = y ⇒ x − y = 0

⊢ (∀x. x ≠ −∞ ⇒ x − −∞ = +∞) ∧ (∀x. x ≠ +∞ ⇒ x − +∞ = −∞) ∧
  (∀x. x ≠ +∞ ⇒ +∞ − x = +∞) ∧ ∀x. x ≠ −∞ ⇒ −∞ − x = −∞

⊢ ∀x y z.
    x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒
    x * (y − z) = x * y − x * z

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y − x ≤ z ⇔ y ≤ z + x)

⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ∧ x ≠ −∞ ∧ z ≠ −∞ ⇒ (y − x ≤ z ⇔ y ≤ z + x)

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≤ z + x ⇒ y − x ≤ z

⊢ ∀x y z. y ≠ −∞ ∧ y ≠ +∞ ∧ y ≤ z + x ⇒ y − x ≤ z

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒ (y − x ≤ z ⇔ y − z ≤ x)

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ (y − x ≤ z ⇔ y − z ≤ x)

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ⇒ (x ≤ y ⇔ x − y ≤ 0)

⊢ ∀x y. x ≠ −∞ ∧ y ≠ −∞ ∨ x ≠ +∞ ∧ y ≠ +∞ ⇒ -x − y = -(x + y)

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ⇒ (y − x < z ⇔ y < z + x)

⊢ ∀x y z. x ≠ −∞ ∧ x ≠ +∞ ∧ y < z + x ⇒ y − x < z

⊢ ∀x y z. z ≠ −∞ ∧ z ≠ +∞ ∧ y < z + x ⇒ y − x < z

⊢ ∀x y. x < y ⇒ x − y < 0

⊢ ∀x y. y ≠ −∞ ∧ y ≠ +∞ ∧ x − y < 0 ⇒ x < y

⊢ ∀x. 0 − x = -x

⊢ ∀x y. (x ≠ −∞ ∧ y ≠ +∞ ⇒ x − y ≠ −∞) ∧ (x ≠ +∞ ∧ y ≠ −∞ ⇒ x − y ≠ +∞)

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ⇒ (x − y)² = x² + y² − 2 * x * y

⊢ ∀x y z.
    x ≠ −∞ ∧ x ≠ +∞ ∧ y ≠ −∞ ∧ y ≠ +∞ ∧ z ≠ −∞ ∧ z ≠ +∞ ⇒
    (x − y) * z = x * z − y * z

⊢ ∀x y. x ≠ +∞ ∧ x ≠ −∞ ∧ y ≠ +∞ ∧ y ≠ −∞ ⇒ real (x − y) = real x − real y

⊢ ∀x. x ≠ −∞ ∧ x ≠ +∞ ⇒ x − x = 0

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

⊢ ∀x. x − 0 = x

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ⇒ (x ≤ y ⇔ 0 ≤ y − x)

⊢ ∀x y. x < y ⇒ 0 < y − x

⊢ ∀x y. x ≠ −∞ ∧ x ≠ +∞ ∧ 0 < y − x ⇒ x < y

⊢ 3 * (1 / 3) = 1

⊢ ((0 < 1 / 3 ∧ 1 / 3 < 1) ∧ 0 < 2 / 3 ∧ 2 / 3 < 1) ∧
  (0 ≤ 1 / 3 ∧ 1 / 3 ≤ 1) ∧ 0 ≤ 2 / 3 ∧ 2 / 3 ≤ 1

⊢ ∀x. 1 / 2 * x + 1 / 2 * x = x

⊢ ∀x. x ≠ 0 ⇒ 0 / x = 0

⊢ ∀n. 0 < n ⇒ 0 pow n = 0