```
"forall(x,y:zz, #(x+y,nn) iff 0<=x+y)"
(theory h-o-real-arithmetic)
(usages  rewrite)
(proof (direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises nn-in-quasi-sort_h-o-real-arithmetic)
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify)))
```

```(def-theorem ()
"forall(x,y:nn,#(x+y,nn ))"
(theory  h-o-real-arithmetic)
(proof
(
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify
))
(usages d-r-convergence))
```

```(def-theorem ()
"forall(x,y:nn,  #(x*y,nn ))"
(theory h-o-real-arithmetic)
(proof
(
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify
(apply-macete-with-minor-premises positivity-for-products)
simplify
))
(usages d-r-convergence))
```

```(def-theorem ()
"forall(x,y:ind,#(x,nn) and #(y,nn) and y<=x implies #(x-y,nn ))"
(theory h-o-real-arithmetic)
(proof
(
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify
))
(usages d-r-convergence))
```

```(def-theorem ()
"forall(x,y:ind,#(x,nn) and #(y,nn) and 1<=y implies #(x^y,nn ))"
(theory h-o-real-arithmetic)
(proof
(
(cut-with-single-formula "forall(x,y:zz,1<=y and 0<=x implies #(x^y,zz) and 0<=x^y)")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
(instantiate-universal-antecedent "forall(x,y:zz,1<=y and 0<=x implies #(x^y,zz) and 0<=x^y);" ("x" "y"))
(contrapose "with(x:ind,not(0<=x));")
simplify
beta-reduce-repeatedly
(induction integer-inductor ("y"))
(force-substitution "x^(1+t)" "x^t*x" (0 1))
direct-inference
simplify
(apply-macete-with-minor-premises positivity-for-products)
direct-and-antecedent-inference-strategy
simplify
))
(usages d-r-convergence))
```

```(def-theorem ()
"forall(j:zz, 0<=j implies #(j,nn))"
(theory h-o-real-arithmetic)
(proof
(
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify
))
(usages d-r-convergence))
```

```(def-theorem ()
"forall(x:rr, 0<=x and #(x,zz) implies #(x,nn))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
beta-reduce-repeatedly
))
(usages d-r-convergence))
```

```(def-theorem ()
"forall(n:nn,#(n+[-1],nn) iff 0<n)"
(theory h-o-real-arithmetic)
(proof
(
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify
direct-and-antecedent-inference-strategy
simplify
simplify
))
(usages rewrite))
```

```(def-theorem ()
"forall(x:rr, #(abs(x)))"
(theory h-o-real-arithmetic)
(proof
(
(unfold-single-defined-constant (0) abs)
insistent-direct-inference
beta-reduce-repeatedly
))
(usages d-r-convergence))
```

```(def-theorem ()
"forall(x,y:rr, #(max(x,y)))"
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
insistent-direct-inference
beta-reduce-repeatedly
))
(usages d-r-convergence))
```

```
(def-theorem positivity-for-squares
"forall(x:rr, 0<=x^2)"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(force-substitution "x^2" "x*x" (0))
(cut-with-single-formula "0<=x or 0<=[-1]*x")
(antecedent-inference "with(x:rr,0<=x or 0<=[-1]*x);")
(apply-macete-with-minor-premises positivity-for-products)
(force-substitution "x*x" "([-1]*x)*([-1]*x)" (0))
(apply-macete-with-minor-premises positivity-for-products)
simplify
simplify
simplify
)))
```

```
(def-theorem triangle-inequality
"forall(x,y:rr,abs(x+y)<=abs(x)+abs(y))"
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
(prove-by-logic-and-simplification 3)
)))
```

```
(def-theorem non-negativity-of-absolute-value
"forall(x:rr,0<=abs(x))"
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
(prove-by-logic-and-simplification 3)
)))
```

```
(def-theorem min-definedness
"forall(x,y:rr,#(min(x,y)))"
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
insistent-direct-inference
beta-reduce-repeatedly
))
(usages d-r-convergence))
```

```
(def-theorem maximum-1st-arg
"forall(x,y:rr,x<=max(x,y))"
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
(prove-by-logic-and-simplification 3)
)
))
```

```
(def-theorem maximum-2nd-arg
"forall(x,y:rr,y<=max(x,y))"
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
(prove-by-logic-and-simplification 3)
)
))
```

```
(def-theorem minimum-1st-arg
"forall(x,y:rr,min(x,y)<=x)"
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
(prove-by-logic-and-simplification 3)
)
))
```

```
(def-theorem minimum-2nd-arg
"forall(x,y:rr,min(x,y)<=y)"
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
(prove-by-logic-and-simplification 3)
)
))
```

```
(def-theorem min-lemma
"forall(a,b,c:rr, a<b and a<c implies forsome(d:rr, a<d and d<=b and d<=c))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-existential ("min(b,c)"))
(unfold-single-defined-constant-globally min)
(case-split ("b<=c"))
simplify
simplify
(apply-macete-with-minor-premises minimum-1st-arg)
(apply-macete-with-minor-premises minimum-2nd-arg)
)))
```

```
(def-theorem max-lemma
"forall(a,b,c:rr, b<a and c<a implies forsome(d:rr, d<a and b<=d and c<=d))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-existential ("max(b,c)"))
(unfold-single-defined-constant-globally max)
(case-split ("b<=c"))
simplify
simplify
(apply-macete-with-minor-premises maximum-1st-arg)
(apply-macete-with-minor-premises maximum-2nd-arg)
)))
```