Theory RealFieldContext

⊢ x pow n ≠ 0 ⇔ x ≠ 0 ∨ &n = 0 ∨ x pow n ≠ 0

⊢ (∀x. 0 * x = 0) ∧ (∀x y z. x + y = x + z ⇔ y = z) ∧
  ∀w x y z. w * y + x * z = w * z + x * y ⇔ w = x ∨ y = z

⊢ &x = &x / 1 ∧ -&x = -&x / 1 ∧ unint (&x / &y) = &x / &y ∧
  -unint (&x / &y) = -&x / &y

⊢ ∀x y. x ≠ y ⇔ ∃z. (x − y) * z = 1

⊢ abs (&n) = &n ∧ abs (-&n) = &n ∧ abs (&m / &n) = &m / &n ∧
  abs (-&m / &n) = &m / &n ∧ abs (unint (&m / &n)) = &m / &n ∧
  abs (-unint (&m / &n)) = &m / &n

⊢ 0 < y1 ⇒
  0 < y2 ⇒
  0 < y3 ⇒
  (x1 * y2 + x2 * y1) * y3 = x3 * (y1 * y2) ⇒
  x1 / y1 + x2 / y2 = x3 / y3

⊢ x / y = x * y⁻¹

⊢ 0 < y1 ⇒ 0 < y2 ⇒ (x1 / y1 = x2 / y2 ⇔ x1 * y2 = x2 * y1)

⊢ 0⁻¹ = 0 ∧ 1⁻¹ = 1 ∧ (-1)⁻¹ = -1 ∧ (1 / &n)⁻¹ = &n ∧ (-1 / &n)⁻¹ = -&n

⊢ (&n)⁻¹ = 1 / &n ∧ (-&n)⁻¹ = -1 / &n ∧ (&m / &n)⁻¹ = &n / &m ∧
  (-&m / &n)⁻¹ = -&n / &m ∧ (unint (&m / &n))⁻¹ = &n / &m ∧
  (-unint (&m / &n))⁻¹ = -&n / &m

⊢ 0 < y1 ⇒ 0 < y2 ⇒ (x1 / y1 ≤ x2 / y2 ⇔ x1 * y2 ≤ x2 * y1)

⊢ 0 < y1 ⇒ 0 < y2 ⇒ (x1 / y1 < x2 / y2 ⇔ x1 * y2 < x2 * y1)

⊢ d1 ≠ 0 ∧ d2 ≠ 0 ∧ d1 * u1 = x1 ∧ d2 * u2 = x2 ∧ d2 * v1 = y1 ∧
  d1 * v2 = y2 ⇒
  x1 / y1 * (x2 / y2) = u1 * u2 / (v1 * v2)

⊢ x1 / y1 * (x2 / y2) = x1 * x2 / (y1 * y2)

⊢ -0 = 0 ∧ --&n = &n ∧ -(&m / &n) = -&m / &n ∧ -(-&m / &n) = &m / &n ∧
  -unint (&m / &n) = -&m / &n

⊢ (x / y) pow n = x pow n / y pow n

⊢ x − y = x + -y