```
(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)
)))
```