(def-theorem exp-out    
  "forall(n:zz,x:rr,2<=n implies x^n=x*x^(n-1))"
  
  (proof
    (
      simplify
      ))
  (theory h-o-real-arithmetic))

(def-theorem monotonicity-for-multiplication 
  "forall(x,y,r:rr, 0<r implies (r*x<=r*y iff x<=y))"
  (proof
    (
      simplify
      ))
  (theory h-o-real-arithmetic))

(def-theorem strict-monotonicity-for-multiplication 
    "forall(x,y,r:rr, 0<r implies (r*x<r*y iff x<y))"
    (proof
      (
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem domain-of-inverse 
    "forall(x:rr,#(x^[-1]) iff (#(x) and not(x=0)))"
    (proof
      (
        direct-inference
        (case-split ("x=0"))
        simplify
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem domain-of-quotient  
    "forall(x,y:rr,#(x/y) iff (#(x) and #(y) and not(y=0)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-inference
        (case-split ("y=0"))
        simplify
        simplify
        )))

(def-theorem domain-of-exponentiation 
    "forall(x:rr,y:zz,#(x^y) iff (#(x) and #(y) and (not(x=0) or 0<y)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (contrapose "with(y:zz,x:rr,#(x^y));")
        simplify
        simplify
        simplify
        ))
    )

(def-theorem totality-of-addition  
    "forall(x,y:rr,#(x+y) iff (#(x) and #(y)))"
    (proof
      (
        simplify
        insistent-direct-inference-strategy
        ))
    (theory h-o-real-arithmetic))

(def-theorem totality-of-multiplication;; simplification. 
    "forall(x,y:rr,#(x*y) iff (#(x) and #(y)))"
    (proof
      (
        simplify
        insistent-direct-inference-strategy 
        ))
    (theory h-o-real-arithmetic))

(def-theorem inverse-replacement ;;;simplification 
    "forall(x:rr,x^[-1] ==1/x)"
    (proof
      (
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem subtraction-replacement  
    "forall(x,y,z,u:rr,x - y =x+[-1]*y)"
    (proof
      (
        simplify
        ))
  
    (theory h-o-real-arithmetic))

(def-theorem negative-replacement 
    "forall(x,y,z,u:rr, - y =[-1]*y)"
    (proof
      (
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem multiplication-of-fractions-left  
  "forall(x,y,u:rr,(x/u)*y == (x*y)/u)"
  (proof
      (
        simplify
        ))
  (theory h-o-real-arithmetic))

(def-theorem multiplication-of-fractions-right 
  "forall(x,y,u:rr,y*(x/u) == (y*x)/u)"
  (proof
      (
        simplify
        ))
  (theory h-o-real-arithmetic))

(def-theorem multiplication-of-fractions  
  "forall(x,y,z,u:rr,x/u*y/z == (x*y)/(u*z))"
  (proof
      (
        simplify
        ))
  (theory h-o-real-arithmetic))

(def-theorem addition-of-fractions-left  
    "forall(x,y,z,u:rr,x/u + y == (x+u*y)/u)"
    (proof
      (
        direct-inference
        (case-split ("u=0"))
        simplify
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem addition-of-fractions-right 
    "forall(x,y,z,u:rr,y+x/u == (x+u*y)/u)"
    (proof
      (
        direct-inference
        (case-split ("u=0"))
        simplify
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem division-of-fractions   
  "forall(x,y,z:rr,(x/y)/z==x/(y*z))"
  (proof
    (
    simplify
    ))
  (theory h-o-real-arithmetic))

(def-theorem division-of-fractions-2  
  "forall(x,y,z:rr,not(z=0) implies x/(y/z)==(x*z)/y)"
  (proof
    (
    simplify
    ))
  (theory h-o-real-arithmetic))

(def-theorem exponents-of-fractions  
    "forall(x,y:rr,n:zz,(x/y)^n ==x^n/y^n)"
    (proof
      (
        direct-inference
        (case-split ("y=0"))
        simplify
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem negative-exponent-replacement  
  "forall(x:rr,n:zz,not(x=0) implies x^([-1]*n)==1/x^n)"
  (proof
    (
      simplify
      ))
  (theory h-o-real-arithmetic))

(def-theorem right-denominator-removal-for-equalities 
    "forall(x,y,z:rr, x = y/z iff (#(z^[-1]) and x*z=y))"
    (proof
      (
        direct-inference
        (force-substitution "x=y/z" "z^[-1]*(x*z-y)=0" (0))
        (case-split ("z=0"))
        simplify
        (apply-macete-with-minor-premises cancel)
        (cut-with-single-formula "not(z^[-1]=0)")
        simplify
        (contrapose "with(z:rr,not(z=0));")
        (force-substitution "z" "z*z^[-1]*z" (0))
        simplify
        (cut-with-single-formula "#(z^[-1])")
        (weaken (1))
        simplify
        (case-split ("z=0"))
        simplify
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem left-denominator-removal-for-equalities  
    "forall(x,y,z:rr, y/z=x iff (#(z^[-1]) and x*z=y))"
    (proof
      (
        (force-substitution "y/z=x" "x=y/z" (0))
        (apply-macete-with-minor-premises right-denominator-removal-for-equalities)
        direct-and-antecedent-inference-strategy
        ))
    (theory h-o-real-arithmetic))

(def-theorem equality-of-fractions 
    "forall(x,y,z,u:rr, x/u = y/z iff (#(u^[-1]) and #(z^[-1]) and x*z=y*u))"
    (proof
      (
        (apply-macete-with-minor-premises right-denominator-removal-for-equalities)
        (apply-macete-with-minor-premises multiplication-of-fractions-left)
        (apply-macete-with-minor-premises left-denominator-removal-for-equalities)
        direct-and-antecedent-inference-strategy
        ))
    (theory h-o-real-arithmetic))

(def-theorem positivity-of-inverse  
    "forall(x:rr,0<x^[-1] iff 0<x)"
    (proof
      (
        (cut-with-single-formula "forall(x:rr, 0<x implies 0<x^[-1])")
        direct-and-antecedent-inference-strategy
        (force-substitution "x" "(x^[-1])^[-1]" (0))
        (backchain "forall(x:rr,0<x implies 0<x^[-1]);")
        simplify
        (backchain "forall(x:rr,0<x implies 0<x^[-1]);")
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "0<x^[-1] or 0=x^[-1] or 0<[-1]*x^[-1]")
        (antecedent-inference "with(x:rr,0<x^[-1] or 0=x^[-1] or 0<[-1]*x^[-1]);")
        (cut-with-single-formula "1=x*x^[-1]")
        (contrapose "with(x:rr,1=x*x^[-1]);")
        simplify
        (weaken (0))
        simplify
        (cut-with-single-formula "0<x*([-1]*x^[-1])")
        (contrapose "with(x:rr,0<x*([-1]*x^[-1]))")
        (weaken (0 1 2))
        (case-split ("x=0"))
        simplify
        simplify
        (apply-macete-with-minor-premises strict-positivity-for-products)
        simplify
        simplify
        ))
    (theory h-o-real-arithmetic))
    

(def-theorem right-denominator-removal-for-strict-inequalities  
    "forall(x,y,z:rr, 0<z implies x < y/z iff x*z<y)"
    (proof
      (
        (force-substitution "x<y/z" "0<z^[-1]*(y-x*z)" (0))
        direct-inference
        direct-inference
        (cut-with-single-formula "0<z^[-1]")
        simplify
        (apply-macete-with-minor-premises positivity-of-inverse)
        (weaken (0))
        (case-split ("z=0"))
        simplify
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem left-denominator-removal-for-strict-inequalities  
    "forall(x,y,z:rr, 0<z implies y/z<x iff y<x*z)"
    (proof
      (
        (force-substitution "y/z<x" "0<z^[-1]*(x*z-y)" (0))
        direct-inference
        direct-inference
        (cut-with-single-formula "0<z^[-1]")
        simplify
        (apply-macete-with-minor-premises positivity-of-inverse)
        (weaken (0))
        (case-split ("z=0"))
        simplify
        simplify
        ))
  
    (theory h-o-real-arithmetic))

(def-theorem right-denominator-removal-for-inequalities 
  "forall(x,y,z:rr, 0<z implies x <= y/z iff x*z<=y)"
  (theory h-o-real-arithmetic)
      (proof
      (
        (force-substitution "x<=y/z" "0<=z^[-1]*(y-x*z)" (0))
        direct-inference
        direct-inference
        (cut-with-single-formula "0<z^[-1]")
        simplify
        (apply-macete-with-minor-premises positivity-of-inverse)
        (weaken (0))
        (case-split ("z=0"))
        simplify
        simplify
        )))

(def-theorem left-denominator-removal-for-inequalities   
    "forall(x,y,z:rr, 0<z implies y/z<=x iff y<=x*z)"
    (theory h-o-real-arithmetic)
    (proof
      (
        (force-substitution "y/z<=x" "0<=z^[-1]*(x*z-y)" (0))
        direct-inference
        direct-inference
        (cut-with-single-formula "0<z^[-1]")
        simplify
        (apply-macete-with-minor-premises positivity-of-inverse)
        (weaken (0))
        (case-split ("z=0"))
        simplify
        simplify
        )))

(def-theorem positivity-for-r^n 
    "forall(r:rr,n:zz,0<r implies 0<r^n)"
    (theory h-o-real-arithmetic)
    (proof
      (
        
        (cut-with-single-formula "forall(r:rr,n:zz,0<r and 0<=n implies 0<r^n)")
        direct-and-antecedent-inference-strategy
        (case-split ("0<=n"))
        (backchain "forall(r:rr,n:zz,0<r and 0<=n implies 0<r^n);")
        direct-and-antecedent-inference-strategy
        (force-substitution "r^n" "(r^[-1])^([-1]*n)" (0))
        (backchain "forall(r:rr,n:zz,0<r and 0<=n implies 0<r^n);")
        (apply-macete-with-minor-premises positivity-of-inverse)
        simplify
        simplify
        (induction integer-inductor ("n"))
        (force-substitution "r^(1+t)" "r^t*r" (0))
        (apply-macete-with-minor-premises strict-positivity-for-products)
        direct-inference
        simplify
        
        )))

(def-compound-macete fractional-expression-manipulation 
    (series
      beta-reduce
      (repeat
        inverse-replacement
        subtraction-replacement
        negative-replacement
        addition-of-fractions-left
        addition-of-fractions-right
        multiplication-of-fractions-left
        multiplication-of-fractions-right
        division-of-fractions
        division-of-fractions-2
        exponents-of-fractions
        negative-exponent-replacement)
      (repeat
        left-denominator-removal-for-equalities
        right-denominator-removal-for-equalities
        right-denominator-removal-for-strict-inequalities
        left-denominator-removal-for-strict-inequalities
        right-denominator-removal-for-inequalities
        left-denominator-removal-for-inequalities
        multiplication-of-fractions-left
        multiplication-of-fractions-right)))

(def-theorem non-zero-product 
    "forall(x,y:rr, #(x) and #(y) and not(x=0) and not(y=0) implies not(x*y=0))"
    (proof
      (
        (apply-macete-with-minor-premises cancel)
        
        ))
    (theory h-o-real-arithmetic))

(def-script prove-iteration-operator-definedness 3 
    (
      direct-inference
      (case-split ((% "~a<=~a" $1 $2)))
      (induction integer-inductor ())
      (prove-by-logic-and-simplification 3)
      (unfold-single-defined-constant (0) $3)
      simplify
      ))

(def-theorem sum-definedness 
    "forall(m,n:zz,f:[zz,rr],forall(k:zz,m<=k and k<=n implies #(f(k))) 
                          implies  
                          #(sum(m,n,f)))"
    (theory h-o-real-arithmetic)
    
    (proof
      
      (
        (prove-iteration-operator-definedness "m" "n" sum)
        
        ))
    (usages d-r-convergence))

(def-theorem prod-definedness  
    "forall(m,n:zz,f:[zz,rr],forall(k:zz,m<=k and k<=n implies #(f(k))) 
                          implies
                        #(prod(m,n,f)))"
    (theory h-o-real-arithmetic)
    
    (proof
      
      (
        (prove-iteration-operator-definedness "m" "n" prod)
        ))
    
    (usages d-r-convergence))

(def-theorem prod-non-zero   
    "forall(m,n:zz,f:[zz,rr],forall(k:zz,m<=k and k<=n implies not(f(k)=0))
                        implies 
                  not(prod(m,n,f)=0))"
    (proof
      (
        direct-inference
        (case-split ("m<=n"))
        (induction integer-inductor ())
        (case-split ("#(f(1+t)) and #(prod(m,t,f))"))
        (apply-macete-with-minor-premises cancel)
        (contrapose "with(t,m:zz,m<=t);")
        (antecedent-inference "with(m,t:zz,f:[zz,rr],f(1+t)=0 or prod(m,t,f)=0);")
        (contrapose "with(t:zz,f:[zz,rr],f(1+t)=0);")
        (prove-by-logic-and-simplification 3)
        (contrapose "with(f:[zz,rr],t,m:zz,prod(m,t,f)=0);")
        (prove-by-logic-and-simplification 3)
        (contrapose "with(m,t:zz,f:[zz,rr],not(#(f(1+t)) and #(prod(m,t,f))));")
        simplify
        (unfold-single-defined-constant (0) prod)
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem monotonicity-for-sum 
    "forall(f,g:[zz,rr], a,b:zz, forall(z:zz,a<=z and z<=b implies f(z)<=g(z))
                                              implies sum(a,b,f)<=sum(a,b,g))"
    (proof
      (
        direct-and-antecedent-inference-strategy
        (case-split ("a<=b"))
        (induction integer-inductor ())
        direct-inference
        (cut-with-single-formula "f(1+t)<=g(1+t) and sum(a,t,f)<=sum(a,t,g)")
        simplify
        (prove-by-logic-and-simplification 3)
        (unfold-single-defined-constant (0 1) sum)
        simplify
        )
      )
    (theory h-o-real-arithmetic))

(def-theorem monotonicity-of-inverse 
    "forall(x,y:rr,0<x and 0<y implies y^[-1]<=x^[-1] iff x<=y)"
  
    (proof
      (
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        ))
    
    (theory h-o-real-arithmetic))

(def-theorem strict-monotonicity-of-inverse   
  "forall(x,y:rr,0<x and 0<y implies y^[-1]<x^[-1] iff x<y)"
    (proof
      (
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem absolute-value-inversion  
    "forall(x:rr, abs(x^[-1])==abs(x)^[-1])"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-inference
        unfold-defined-constants
        (cut-with-single-formula "0<x or 0=x or x<0")
        (antecedent-inference "with(x:rr,0<x or 0=x or x<0);")
        (cut-with-single-formula "0<x^[-1]")
        simplify
        (apply-macete-with-minor-premises positivity-of-inverse)
        simplify
        (cut-with-single-formula "x^[-1]<0")
        simplify
        (force-substitution "x^[-1]<0" "0<([-1]*x)^[-1]" (0))
        (apply-macete-with-minor-premises positivity-of-inverse)
        simplify
        simplify
        simplify
        )))

(def-theorem absolute-value-product 
    "forall(x,y:rr,abs(x*y)=abs(x)*abs(y))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-inference
        unfold-defined-constants
        (cut-with-single-formula "0<x and 0<y and 0<x*y or 0<x and y<0 and 0<[-1]*y*x or 
  0<y and x<0 and 0<[-1]*x*y or x<0 and y<0 and 0<([-1]*y)*([-1]*x) or (x=0 or y=0) and x*y=0")
        (prove-by-logic-and-simplification 3)
        (apply-macete-with-minor-premises strict-positivity-for-products)
        (apply-macete-with-minor-premises cancel)
        (prove-by-logic-and-simplification 3)
        )))

(def-theorem absolute-value-quotient 
    "forall(x,y:rr,abs(x/y)==abs(x)/abs(y))"
    (theory h-o-real-arithmetic)
    (proof
      (
        simplify
        (apply-macete-with-minor-premises absolute-value-product)
        (apply-macete-with-minor-premises absolute-value-inversion)
        )))

(def-theorem absolute-value-zero 
    "forall(x:rr,abs(x)=0 iff x=0)"
    (theory h-o-real-arithmetic)
    (proof
      (
        unfold-defined-constants
        direct-inference
        (case-split ("0<=x"))
        simplify
        simplify
        )))

(def-theorem absolute-value-non-negative 
    "forall(x:rr,0<=x implies abs(x)=x)"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        unfold-defined-constants
        simplify
        ))
    )

(def-theorem absolute-value-non-positive 
    "forall(x:rr,x<=0 implies abs(x)=-x)"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        unfold-defined-constants
        (case-split ("x<0"))
        simplify
        simplify
        ))
    )

(def-theorem absolute-value-absolute-value 
    "forall(x:rr,abs(abs(x))=abs(x))"
    (theory h-o-real-arithmetic)
    (usages rewrite)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete absolute-value-non-negative)
        )))

(def-compound-macete integer-induction 
    (sequential
      (sound
        abstraction-for-induction
        beta-reduce
        beta-reduce)
      induct))

(def-theorem ()
    "forall(x,y:zz, #(max(x,y),zz))"
    (theory h-o-real-arithmetic)
    (usages d-r-convergence)
    (proof
      (
        unfold-defined-constants
        ))
    )

(def-theorem ()
    "forall(x,y:zz,#(min(x,y),zz))"
  (theory h-o-real-arithmetic)
  (proof
      (
        unfold-defined-constants
        ))
  (usages d-r-convergence))

(def-theorem factorial-non-zero 
    "forall(m:zz,not(m!=0))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant (0) factorial)
        (apply-macete-with-minor-premises prod-non-zero)
        simplify
        )))

(def-theorem factorial-non-zero-1 
    "forall(m:zz, y:rr, m!=y implies not(y=0))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (backchain-backwards "with(y:rr,m:zz,m!=y);")
        (apply-macete-with-minor-premises factorial-non-zero)
        ))
    (usages d-r-value))

(def-theorem factorial-out 
    "forall(m:zz,1<=m implies m!=(m-1)!*m)"
    (proof
      (
        (unfold-single-defined-constant (0 1) factorial)
        (unfold-single-defined-constant (0) prod)
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-theorem factorial-definedness 
    "forall(m:zz,#(m!))"
    (proof
      (
        (unfold-single-defined-constant (0) factorial)
        insistent-direct-inference
        beta-reduce-repeatedly
        (apply-macete-with-minor-premises prod-definedness)
        simplify
        )
      )
    (theory h-o-real-arithmetic)
    (usages d-r-convergence))

(def-compound-macete definedness-manipulations 
    (series
      (repeat
        totality-of-addition
        totality-of-multiplication
        domain-of-exponentiation
        domain-of-inverse
        non-zero-product
        factorial-non-zero
        sum-definedness
        factorial-definedness)
      simplify))

(def-theorem monotone-product-lemma 
    "forall(x,y,z,u:rr, 0<=x and x<=y and 0<=u and u<=z implies x*u<=y*z)"
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises transitivity-of-<=)
        (instantiate-existential ("x*z"))
        (cut-with-single-formula "0<=x*(z-u)")
        simplify
        (apply-macete-with-minor-premises positivity-for-products)
        simplify
        (cut-with-single-formula "0<=(y-x)*z")
        simplify
        (apply-macete-with-minor-premises positivity-for-products)
        simplify
        )
      )
    (theory h-o-real-arithmetic))

(def-theorem prod-definedness-converse 
    "forall(m,n:zz,f:[zz,rr], 
            #(prod(m,n,f))
                  implies
            forall(k:zz,m<=k and k<=n implies #(f(k))))"
    (theory h-o-real-arithmetic)
    
    (proof
      
      (
        direct-inference
        direct-inference
        (case-split ("m<=n"))
        (induction integer-inductor ())
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "k_$0=m")
        simplify
        simplify
        (case-split ("k=1+t"))
        simplify
        simplify
        direct-and-antecedent-inference-strategy
        (simplify-antecedent "with(p:prop,not(p));")
        ))
    )

(def-theorem monotonicity-of-exponentiation 
    "forall(a:rr, x,y:zz, x<=y and 0<a and a<=1 implies a^y<=a^x)"
    (theory h-o-real-arithmetic)
    (proof
      (
        (induction integer-inductor ("y"))
        (force-substitution "a^(1+t)<=a^x" "a*a^t<=1*a^x" (0))
        (block 
            (script-comment "`force-substitution' at (0)")
            (apply-macete-with-minor-premises monotone-product-lemma)
            (cut-with-single-formula "0<a^t")
            simplify
            (apply-macete-with-minor-premises positivity-for-r^n))
        (block 
            (script-comment "`force-substitution' at ()")
            direct-inference
            simplify)
        )))

(def-theorem strict-monotonicity-of-exponentiation 
    "forall(a:rr, x,y:zz, x<y and 0<a and a<1 implies a^y<a^x)"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "a^y<=a^(x+1)")
        (move-to-sibling 1)
        (block 
            (script-comment "`cut-with-single-formula' at (1)")
            (apply-macete-with-minor-premises monotonicity-of-exponentiation)
            simplify)
        (cut-with-single-formula "a^(x+1)<a^x")
        simplify
        (force-substitution "a^(x+1)<a^x" "0<(1-a)*a^x" (0))
        (move-to-sibling 1)
        (block 
            (script-comment "`force-substitution' at (1)")
            (weaken ("a<1"))
            simplify)
        (block 
            (script-comment "`force-substitution' at (0)")
            simplify
            (apply-macete-with-minor-premises positivity-for-r^n))
        )))