```
(def-theorem exponential-monotonicity-lemma
"forall(n:zz,2<=n implies (1+1/(n-1))^(n-1)<=(1+1/n)^n)"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "1-1/n<=(1-1/n^2)^n")
(cut-with-single-formula "n^(2*n)*(n-1)<=n*(n^2-1)^n")
(weaken (1))
(cut-with-single-formula "n*(n^2-1)^n=n*(n+1)^n*(n-1)^(n-1)*(n-1)")
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(contrapose "with(n:zz,n^(2*n)*(n-1)<=n*(n^2-1)^n);")
(backchain "with(n:zz,n*(n^2-1)^n=n*(n+1)^n*(n-1)^(n-1)*(n-1));")
(force-substitution "n^(2*n)" "n^(2*n-1)*n" (0))
simplify
simplify
(apply-macete-with-minor-premises positivity-for-r^n)
(apply-macete-with-minor-premises positivity-for-r^n)
simplify
(cut-with-single-formula "forall(x,y:rr,m:zz,1<=m implies x^m*y^m=(x*y)^m)")
(backchain "forall(x,y:rr,m:zz,1<=m implies x^m*y^m=(x*y)^m);")
simplify
simplify
(incorporate-antecedent "with(n:zz,1-1/n<=(1-1/n^2)^n);")
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(apply-macete-with-minor-premises positivity-for-r^n)
(cut-with-single-formula "1+n*(-1/n^2)<=(1+(-1/n^2))^n")
simplify
(apply-macete-with-minor-premises bernoullis-inequality)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(force-substitution "1<n^2" "0<(n-1)*(n+1)" (0))
(apply-macete-with-minor-premises strict-positivity-for-products)
simplify
direct-and-antecedent-inference-strategy
simplify
(apply-macete-with-minor-premises positivity-for-r^n)
simplify
)))
```

```
(def-theorem sum-lte-product
"forall(x,y:rr, 2<=x and 2<=y implies x+y<=x*y)"
(theory h-o-real-arithmetic)
(proof
(

direct-and-antecedent-inference-strategy
(cut-with-single-formula "1/x+1/y<=1")
(incorporate-antecedent "with(r:rr,r<=1);")
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
(cut-with-single-formula "1/x<=1/2 and 1/y<=1/2")
simplify
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify
)))
```