(def-theorem positivity-of-rr-distance
*"forall(x,y:rr,0<=lambda(x,y:rr,abs(x-y))(x,y))"*
(theory h-o-real-arithmetic)
(proof
(simplify)))

(def-theorem point-separation-for-rr-distance
*"forall(x,y:rr,x=y iff lambda(x,y:rr,abs(x-y))(x,y)=0)"*
(theory h-o-real-arithmetic)
(proof
(
beta-reduce-repeatedly
(apply-macete-with-minor-premises absolute-value-zero)
simplify
)))

(def-theorem symmetry-of-rr-distance
*"forall(x,y:rr, lambda(x,y:rr,abs(x-y))(x,y)=
lambda(x,y:rr,abs(x-y))(y,x))"*
(proof
(
beta-reduce-repeatedly
(force-substitution *"y-x"* *"[-1]*(x-y)"* (0))
(apply-macete-with-minor-premises absolute-value-product)
(unfold-single-defined-constant (1) abs)
simplify
simplify
))
(theory h-o-real-arithmetic))

(def-theorem triangle-inequality-for-rr-distance
*"forall(x,y,z:rr, lambda(x,y:rr,abs(x-y))(x,z)<=
lambda(x,y:rr,abs(x-y))(x,y)+lambda(x,y:rr,abs(x-y))(y,z))"*
(proof
(
beta-reduce-repeatedly
(force-substitution *"(x-z)"* *"(x-y)+(y-z)"* (0))
(apply-macete-with-minor-premises triangle-inequality)
simplify
))
(theory h-o-real-arithmetic))

(def-theorem sub-is-diff
*"sub=lambda(x,y:rr,-y+x)"*
(theory h-o-real-arithmetic)
(proof
(
(prove-by-logic-and-simplification 3)
)))