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