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