(def-constant monotone%between 
    "lambda(a,b:rr, f:[rr,rr],
          forall(x,y:rr,
              a <= x
                and 
              x <= b
                and 
              a <= y
                and 
              y <= b
                and 
              x <= y
                implies 
              f(x) <= f(y)))"
    (theory h-o-real-arithmetic))

(def-theorem monotone-fixed-point-theorem 
    "forall(b,a:rr,f:[rr,rr],
          a <= b
            and 
          a <= f(a)
            and 
          f(b) <= b
            and 
          monotone%between(a,b,f)
            implies 
          forsome(z:rr,(a <= z and z <= b) and f(z)=z))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant (0) monotone%between)
        (apply-macete-with-minor-premises tr%knaster-fixed-point-theorem-corollary)
        )))

(def-constant weakly%lipschitz%between 
    "lambda(a,b:rr,f:[rr,rr], forsome(k:rr, 
                  forall(x,y:rr, x<=y and a<=x and y<=b implies f(y)-f(x)<=k*(y-x))))"
    (theory h-o-real-arithmetic))

(def-theorem weak-lipschitz-constant-positive  
    "forall(a,b:rr,f:[rr,rr], weakly%lipschitz%between(a,b,f) iff forsome(k:rr, 0<k and 
                  forall(x,y:rr, x<=y and a<=x and y<=b implies f(y)-f(x)<=k*(y-x))))"
    (theory h-o-real-arithmetic)
    (proof (
	    (unfold-single-defined-constant-globally weakly%lipschitz%between)
	    direct-and-antecedent-inference-strategy
	    (case-split ("0<k"))
	    auto-instantiate-existential
	    (instantiate-existential ("1"))
	    simplify
	    (apply-macete-with-minor-premises transitivity-of-<=)
	    (instantiate-existential ("0"))
	    (case-split ("k=0"))
	    (incorporate-antecedent "with(p:prop,forall(x,y:rr,p));")
	    simplify
	    (cut-with-single-formula "k*(y-x)<=0")
	    (auto-instantiate-universal-antecedent "with(k:rr,f:[rr,rr],b,a:rr,
    forall(x,y:rr,
        x<=y and a<=x and y<=b implies f(y)-f(x)<=k*(y-x)));")
	    simplify
	    (force-substitution "k*(y-x)<=0" "(-k)*0<=(-k)*(y-x)" (0))
	    (apply-macete-with-minor-premises monotonicity-for-multiplication)
	    simplify
	    simplify
	    simplify
	    simplify
	    auto-instantiate-existential)))

(def-theorem weak-intermediate-value-thm 
    "forall(a,b:rr, f:[rr,rr], f(a)<=0 and 0<=f(b) 
                            and
                          a<=b
                            and
                          weakly%lipschitz%between(a,b,f)
                            implies
                          forsome(x:rr, a<=x and x<=b and f(x)=0))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (apply-macete-with-minor-premises weak-lipschitz-constant-positive)
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(x:rr, (a<=x and x<=b) and lambda(z:rr,z-f(z)/k)(x)=x)")
        (block (script-comment "first use the assertion.")
	      (instantiate-existential ("x"))
	      (incorporate-antecedent "with(p:prop,p and p);")
	      (apply-macete-with-minor-premises fractional-expression-manipulation)
	      simplify)
        (block (script-comment "now prove the assertion useing the knaster fp theorem.")
	      (apply-macete-with-minor-premises tr%knaster-fixed-point-theorem-corollary)
	      (incorporate-antecedent "with(p:prop,forall(x,y:rr,p));")
	      (apply-macete-with-minor-premises fractional-expression-manipulation)
	      simplify
	      direct-and-antecedent-inference-strategy-with-simplification
	      (instantiate-universal-antecedent "with(p:prop,forall(x,y:rr,p));"
        ("x_$0" "y_$0")
    )
	      simplify)
        )))

(def-theorem power-fn-is-monotone 
    "forall(n:zz, x,y:rr, 1<=n and 0<=x and x<=y implies x^n <= y^n)"
    (theory h-o-real-arithmetic)
    lemma
    (proof
      (
        
        
        (induction integer-inductor ("n"))
        (apply-macete-with-minor-premises exp-out)
        (apply-macete-with-minor-premises monotone-product-lemma)
        simplify
        (case-split ("x=0"))
        simplify
        (cut-with-single-formula "0<x^t")
        simplify
        (apply-macete-with-minor-premises positivity-for-r^n)
        simplify
        )))

(def-theorem power-fn-is-weakly%lipschitz 
    "forall(r:rr, n:zz, 1<=n implies weakly%lipschitz%between(0,r, lambda(x:rr,x^n)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (unfold-single-defined-constant (0) weakly%lipschitz%between)
        (case-split ("r=0"))
        (instantiate-existential ("1"))
        (cut-with-single-formula "x_$0=y_$0")
        simplify
        simplify
        (instantiate-existential ("n*r^(n-1)"))
        (induction trivial-integer-inductor ("n"))
        simplify
        (cut-with-single-formula
          "y_$1*(y_$1^t-x_$1^t)<=t*r^t*(y_$1-x_$1) and x_$1^t*(y_$1-x_$1)<=r^t*(y_$1-x_$1)")
        simplify
        (force-substitution "t*r^t*(y_$1-x_$1)" "r*(t*r^(t-1)*(y_$1-x_$1))" (0))
        (apply-macete-with-minor-premises monotone-product-lemma)
        simplify
        (force-substitution "0" "0^t" (0))
        (move-to-sibling 1)
        simplify
        (apply-macete-with-minor-premises power-fn-is-monotone)
        simplify
        simplify
        )))

(def-theorem nth-roots-exist 
    "forall(x:rr, n:zz, 1<=n and 0<=x implies forsome(y:rr, 0<=y and y^n=x))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula
          "forsome(a:rr, forsome(y:rr, 0<=y and y<=a and lambda(theta:rr, theta^n-x)(y)=0))")
        (antecedent-inference "with(p:prop,forsome(a:rr,p));")
        (instantiate-existential ("y"))
        (simplify-antecedent "with(p:prop,p and p and p);")
        (apply-macete-with-minor-premises weak-intermediate-value-thm)
        beta-reduce-repeatedly
        (force-substitution "weakly%lipschitz%between(0,a,lambda(theta:rr,theta^n-x))"
			"weakly%lipschitz%between(0,a,lambda(theta:rr,theta^n))"
			(0))
        (move-to-sibling 1)
        (unfold-single-defined-constant-globally weakly%lipschitz%between)
        simplify
        (apply-macete-with-minor-premises power-fn-is-weakly%lipschitz)
        simplify
        (case-split ("x<=1"))
        (instantiate-existential ("1"))
        simplify
        simplify
        (instantiate-existential ("x"))
        (induction integer-inductor ("n"))
        (apply-macete-with-minor-premises exp-out)
        (force-substitution "x" "1*x" (0))
        (apply-macete-with-minor-premises monotone-product-lemma)
        simplify
        simplify    )))
	          

(def-theorem nth-roots-are-unique 
    "forall(x,y:rr, n:zz, 1<=n and 0<=x and 0<=y and x^n=y^n implies x=y)"
    (theory h-o-real-arithmetic)
    (proof
      (
        
        (cut-with-single-formula "forall(x,y:rr, n:zz, 1<=n and 0<=x and x<y implies x^n<y^n)")
        (move-to-sibling 1)
        direct-and-antecedent-inference-strategy
        (case-split ("x=0"))
        simplify
        (apply-macete-with-minor-premises positivity-for-r^n)
        (cut-with-single-formula "forall(t:rr, 1<t implies 1<t^n)")
        (instantiate-universal-antecedent "with(p:prop,forall(t:rr,p));" ("y/x"))
        (contrapose "with(r:rr,not(1<r));")
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        (incorporate-antecedent "with(r:rr,1<r);")
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        (apply-macete-with-minor-premises positivity-for-r^n)
        simplify
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "1+n*(t-1)<=t^n and 0<n*(t-1)")
        simplify
        (force-substitution "t" "1+(t-1)" (1))
        (apply-macete-with-minor-premises bernoullis-inequality)
        simplify
        simplify
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "x<y or x=y or y<x")
        (antecedent-inference "with(p:prop,p or p or p);")
        (instantiate-universal-antecedent "with(p:prop,forall(x,y:rr,n:zz,p));"
				            ("x" "y" "n"))
        simplify
        (instantiate-universal-antecedent "with(p:prop,forall(x,y:rr,n:zz,p));"
				            ("y" "x" "n"))
        simplify
        simplify
        )))

(def-constant nth%root 
    "lambda(n:zz,x:rr, iota(y:rr, 1<=n and 0<=y and y^n=x))"
    (theory h-o-real-arithmetic))

(def-theorem iota-free-characterization-of-nth%root 
    "forall(n:zz,x,y:rr, 1<=n implies (nth%root(n,x)=y iff (0<=y and y^n=x)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant (0) nth%root)
        direct-and-antecedent-inference-strategy
        (contrapose "with(y,r:rr,r=y);")
        (apply-macete-with-minor-premises eliminate-iota-macete)
        (contrapose "with(p:prop,not(p));")
        (contrapose "with(y,r:rr,r=y);")
        (apply-macete-with-minor-premises eliminate-iota-macete)
        (contrapose "with(p:prop,not(p));")
        (apply-macete-with-minor-premises eliminate-iota-macete)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises nth-roots-are-unique)
        (instantiate-existential ("n"))    
        )))

(def-theorem nth%root%existence 
    "forall(n:zz, x:rr, 0 <=x and 1<=n implies #(nth%root(n,x)))"
    (theory h-o-real-arithmetic)
    (usages d-r-convergence)
    (proof
      (
        
        
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(y:rr, 0<=y and nth%root(n,x)=y)")
        (antecedent-inference "with(p:prop,forsome(y:rr,p));")
        (apply-macete-with-minor-premises iota-free-characterization-of-nth%root)
        simplify
        (apply-macete-with-minor-premises nth-roots-exist)
        direct-and-antecedent-inference-strategy
        )))

(def-theorem nth%root-power 
    "forall(a,b:rr,n:zz,0<=a and 1<=n implies nth%root(n,a)^n=a)"
    (theory h-o-real-arithmetic)
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(s:rr, nth%root(n,a)=s)")
        (move-to-sibling 1)
        (instantiate-existential ("nth%root(n,a)"))
        simplify
        (antecedent-inference "with(p:prop,forsome(s:rr,p));")
        (backchain "with(s,r:rr,r=s);")
        (incorporate-antecedent "with(s,r:rr,r=s);")
        (apply-macete-with-minor-premises iota-free-characterization-of-nth%root)
        direct-and-antecedent-inference-strategy
        )))

(def-theorem strict-monotonicity-of-nth%root 
    "forall(a,b:rr, n:zz, 0<=a and a<b and 1<=n implies nth%root(n,a)<nth%root(n,b))"
    (theory h-o-real-arithmetic)
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (case-split ("nth%root(n,b)<=nth%root(n,a)"))
        (move-to-sibling 2)
        simplify
        (cut-with-single-formula "not(b<=a)")
        (move-to-sibling 1)
        simplify
        (contrapose "with(p:prop,not(p));")
        (cut-with-single-formula "(nth%root(n,b))^n<=(nth%root(n,a))^n")
        (move-to-sibling 1)
        (apply-macete-with-minor-premises power-fn-is-monotone)
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(s:rr, nth%root(n,b)=s)")
        (antecedent-inference "with(p:prop,forsome(s:rr,p));")
        (backchain "with(s,r:rr,r=s);")
        (incorporate-antecedent "with(s,r:rr,r=s);")
        (apply-macete-with-minor-premises iota-free-characterization-of-nth%root)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("nth%root(n,b)"))
        (contrapose "with(n:zz,r:rr,r^n<=r^n);")
        (apply-macete-with-minor-premises nth%root-power)
        )))

(def-theorem monotonicity-of-nth%root 
    "forall(a,b:rr, n:zz, 0<=a and a<=b and 1<=n implies nth%root(n,a)<=nth%root(n,b))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (case-split ("a=b"))
        simplify
        (cut-with-single-formula "nth%root(n,a)<nth%root(n,b)")
        simplify
        (apply-macete-with-minor-premises strict-monotonicity-of-nth%root)
        simplify)))
        

(def-theorem nth-root-is-multiplicative 
    "forall(a,b:rr, n:zz,
          0<=a and 0<=b and 1<=n implies nth%root(n,a*b)=nth%root(n,a)*nth%root(n,b))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(s,t:rr, nth%root(n,a)=s and nth%root(n,b)=t)"
			          )
        (move-to-sibling 1)
        (instantiate-existential ("nth%root(n,a)" "nth%root(n,b)"))
        (block 
	(script-comment "`cut-with-single-formula' at (0)")
            (antecedent-inference "with(p:prop,forsome(s,t:rr,p));")
            (backchain "with(p:prop,p and p);") (backchain "with(p:prop,p and p);")
            (incorporate-antecedent "with(p:prop,p and p);")
            (apply-macete-with-minor-premises iota-free-characterization-of-nth%root)
            simplify direct-and-antecedent-inference-strategy
            (block
	    (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0 0)"
			    )
	(apply-macete-with-minor-premises positivity-for-products) simplify
	)
            simplify
            ))))

(def-theorem nth%root-of-zero 
    "forall(n:zz,  1<=n implies nth%root(n,0)=0)"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-inference
        (instantiate-theorem nth%root%existence ("n" "0"))
        (simplify-antecedent "with(p:prop,p);")
        direct-inference
        (incorporate-antecedent "with(p:prop,p);")
        (unfold-single-defined-constant-globally nth%root)
        (eliminate-defined-iota-expression 1 zero)
        simplify)))

(def-theorem nth%root-non-negative 
    "forall(x:rr,n:zz, 0<=x and 1<=n implies 0<= nth%root(n,x))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem strict-monotonicity-of-nth%root ("0" "x" "n"))
        (simplify-antecedent "with(p:prop,not(p));")
        (cut-with-single-formula "x=0")
        simplify
        (apply-macete-with-minor-premises nth%root-of-zero)
        simplify
        (contrapose "with(r:rr,r<r);")
        (apply-macete-with-minor-premises nth%root-of-zero)
        simplify)))

(def-theorem nth%root-positive-for-positive 
    "forall(x:rr,n:zz, 0<x and 1<=n implies 0<nth%root(n,x))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem strict-monotonicity-of-nth%root ("0" "x" "n"))
        (simplify-antecedent "with(p:prop,not(p));")
        (contrapose "with(x:rr,n:zz,nth%root(n,0)<nth%root(n,x));")
        (apply-macete-with-minor-premises nth%root-of-zero))))

(def-theorem iterated-nth%root 
    "forall(x:rr,n,m:zz, 0<=x and 1<=n and 1<=m implies nth%root(n*m,x)=nth%root(n,nth%root(m,x)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (apply-macete-with-minor-premises iota-free-characterization-of-nth%root)
        (apply-macete-with-minor-premises nth%root-non-negative)
        (apply-macete-with-minor-premises nth%root-non-negative)
        (force-substitution "nth%root(n,nth%root(m,x))^(n*m)"
			"(nth%root(n,nth%root(m,x))^(n))^m"
			(0))
        (apply-macete-with-minor-premises nth%root-power)
        (apply-macete-with-minor-premises nth%root-power)
        simplify
        (apply-macete-with-minor-premises nth%root-non-negative)
        simplify
        (apply-macete-with-minor-premises product-power-is-iterated-power)
        (force-substitution "1" "1*1" (0))
        (apply-macete-with-minor-premises monotone-product-lemma)
        simplify
        simplify
        )))