opaque define abs : (fn Real -> Real)

opaque define max : (fn (Real, Real) -> Real)

opaque define min : (fn (Real, Real) -> Real)

opaque define operator - : (fn (Real, Real) -> Real)

opaque define operator / : (fn (Real, Real) -> Real)

opaque define operator < : (fn (Real, Real) -> bool)

define operator > : (fn (Real, Real) -> bool) = fun x:Real, y:Real {
      y < x
    }

define operator ≥ : (fn (Real, Real) -> bool) = fun x:Real, y:Real {
      y ≤ x
    }

real_abs_def: (all x:Real. abs(x) = (if real(+0) ≤ x then x else - x))

real_div_def: (all x:Real, y:Real. x / y = x * inv(y))

real_less_def: (all x:Real, y:Real. (x < y) = ((x ≤ y) and x ≠ y))

real_max_def: (all x:Real, y:Real. max(x, y) = (if x ≤ y then y else x))

real_min_def: (all x:Real, y:Real. min(x, y) = (if x ≤ y then x else y))

real_sub_def: (all x:Real, y:Real. x - y = x + - y)