(def-theorem sup-minus-epsilon 
    "forall(s:sets[rr],eps:rr,0<eps implies not(sup(s)-eps majorizes s))"
    (theory h-o-real-arithmetic)
    (proof
      (direct-and-antecedent-inference-strategy
        (cut-with-single-formula "#(sup(s)) or not(#(sup(s)))")
        (antecedent-inference "with(s:sets[rr],#(sup(s)) or not(#(sup(s))));")
        (cut-with-single-formula "not(sup(s)<=sup(s)-eps)")
        (contrapose "with(eps:rr,s:sets[rr],not(sup(s)<=sup(s)-eps));")
        (apply-macete-with-minor-premises tr%lub-property-of-prec%sup)
        direct-and-antecedent-inference-strategy
        simplify
        simplify
        simplify)))

(def-theorem sup-minus-epsilon-corollary 
    "forall(s:sets[rr],eps:rr, 0<eps and #(sup(s)) implies forsome(x:rr, x in s and sup(s)-eps<x))"
    
    (proof
      (direct-and-antecedent-inference-strategy
        (cut-with-single-formula "not(sup(s)-eps majorizes s)")
        (contrapose "with(eps:rr,s:sets[rr],not(sup(s)-eps majorizes s));")
        (unfold-single-defined-constant (0) majorizes)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(p,q:prop,forall(x:rr,p or q))" ("x_$0"))
        simplify
        (apply-macete-with-minor-premises sup-minus-epsilon)))
    (theory h-o-real-arithmetic))

(def-theorem nondecreasing-sequences-converge 
    "forall(f:[zz,rr],nondecreasing(f)
      and 
    forsome(n:zz,forall(k:zz,n<=k implies #(f(k))))
      and 
    #(sup(ran{f}))
      implies 
    forall(eps:rr,
        0<eps
          implies 
        forsome(k:zz,
            forall(j:zz,
                k<=j implies sup(ran{f})-f(j)<=eps))))"
    (proof
      (   
        (unfold-single-defined-constant (0) nondecreasing)
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(x:rr , x in ran{f} and sup(ran{f})-eps<x)")
        (antecedent-inference "with(eps:rr,f:[zz,rr],
    forsome(x:rr,x in ran{f} and sup(ran{f})-eps<x))")
        (antecedent-inference "with(eps,x:rr,f:[zz,rr],x in ran{f} and sup(ran{f})-eps<x)")
        (incorporate-antecedent "with(x:rr,f:[zz,rr],x in ran{f})")
        (apply-macete-with-minor-premises indicator-facts-macete)
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("max(x_$0,n)"))
        (cut-with-single-formula "f(x_$0)<=f(j_$0)")
        simplify
        (backchain "with(f:[zz,rr],
    forall(n,p:zz,
        n<=p and #(f(n)) and #(f(p)) implies f(n)<=f(p)))")
        (cut-with-single-formula "n<=max(x_$0,n) and x_$0<=max(x_$0,n)")
        direct-and-antecedent-inference-strategy
        simplify
        (backchain "with(f:[zz,rr],n:zz,forall(k:zz,n<=k implies #(f(k))))")
        simplify
        (apply-macete-with-minor-premises maximum-1st-arg)
        (apply-macete-with-minor-premises maximum-2nd-arg)
        (apply-macete-with-minor-premises sup-minus-epsilon-corollary)
        direct-and-antecedent-inference-strategy
        ))
    (theory h-o-real-arithmetic))

(def-theorem nondecreasing-sequences-converge-corollary 
    "forall(f:[zz,rr],nondecreasing(f)
      and 
    forsome(n:zz,forall(k:zz,n<=k implies #(f(k))))
      and 
    #(sup(ran{f}))
      implies 
    forall(eps:rr,
        0<eps
          implies 
        forsome(k:zz,
            forall(j,j_1:zz,
                k<=j and j<=j_1 implies f(j_1)-f(j)<=eps))))"
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (instantiate-theorem nondecreasing-sequences-converge ("f"))
        (contrapose "with(f:[zz,rr],forall(n:zz,forsome(k:zz,n<=k and not(#(f(k))))))")
        (instantiate-existential ("n"))
        (instantiate-universal-antecedent "with(p:prop,forall(eps:rr,0<eps implies p))" ("eps"))
        (instantiate-existential ("k"))
        (cut-with-single-formula "f(j_1)<=sup(ran{f}) and sup(ran{f})-f(j)<=eps")
        simplify
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("f(max(j_1,n))"))
        (apply-macete-with-minor-premises indicator-facts-macete)
        beta-reduce-repeatedly
        (instantiate-existential ("max(j_1,n)"))
        (incorporate-antecedent "with(f:[zz,rr],nondecreasing(f));")
        (unfold-single-defined-constant (0) nondecreasing)
        direct-and-antecedent-inference-strategy
        (backchain "with(f:[zz,rr],
    forall(n,p:zz,
        n<=p and #(f(n)) and #(f(p)) implies f(n)<=f(p)));")
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises maximum-1st-arg)
        (instantiate-universal-antecedent "with(eps:rr,f:[zz,rr],k:zz,
    forall(j:zz,k<=j implies sup(ran{f})-f(j)<=eps));" ("j_1"))
        (contrapose "with(j_1,k:zz,not(k<=j_1));")
        simplify
        (instantiate-universal-antecedent "with(eps:rr,f:[zz,rr],k:zz,
    forall(j:zz,k<=j implies sup(ran{f})-f(j)<=eps));" ("j_1"))
        (backchain "with(eps:rr,f:[zz,rr],k:zz,
    forall(j:zz,k<=j implies sup(ran{f})-f(j)<=eps));")
        ))
    (theory h-o-real-arithmetic))

(def-theorem sum-interval-additivity 
    "forall(m,n,p:zz, f:[zz,rr], m<=n and n<=p implies 
                        sum(m,n,f)+sum(n+1,p,f)==sum(m,p,f))"
    (proof
      (
        
        (induction integer-inductor ("p"))
        direct-inference
        (backchain-backwards "with(p,q:prop, p implies q)")
        direct-and-antecedent-inference-strategy
        simplify
        )
      )
    (theory h-o-real-arithmetic))

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

(def-theorem nondecreasing%sums 
    "forall(s:[zz,rr], k:zz, forall(n:zz,k<=n implies 0<=s(n))
	            implies
              nondecreasing(lambda(p:zz,sum(k,p,s))))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant (0) nondecreasing)
        direct-and-antecedent-inference-strategy
        (case-split ("k<=n_$0"))
        (force-substitution "sum(k,p_$0,s)" "sum(k,n_$0,s)+sum(n_$0+1,p_$0,s)" (0))
        simplify
        (apply-macete-with-minor-premises sum-nonnegativity)
        (prove-by-logic-and-simplification 3)
        (apply-macete-with-minor-premises sum-interval-additivity)
        (unfold-single-defined-constant (0) sum)
        simplify
        (case-split ("k<=p_$0"))
        (apply-macete-with-minor-premises sum-nonnegativity)
        (prove-by-logic-and-simplification 3)
        (unfold-single-defined-constant (0) sum)
        simplify
        )
      )   
				    
    )

(def-constant summable%nonnegative 
    "lambda(s:[zz,rr], 
                    forsome(k:zz, forall(n:zz,k<=n implies 0<=s(n) and 
                                                #(sup(ran{lambda(p:zz,sum(k,p,s))})))))"
    (theory h-o-real-arithmetic))

(def-theorem small%tails%of%summable%nonnegative%sequence 
    "forall(s:[zz,rr], summable%nonnegative(s) implies 
                          forall(eps:rr,0<eps
                                            implies 
                                        forsome(p:zz,
                                              forall(j,j_1:zz,
                                                  p<=j and j<=j_1 implies sum(j,j_1,s)<=eps))))"
    (proof
      (
        (unfold-single-defined-constant (0) summable%nonnegative)
        direct-and-antecedent-inference-strategy
        (instantiate-theorem nondecreasing-sequences-converge-corollary ("lambda(j:zz, sum(k,j,s))"))
        (contrapose "with(p:prop, not(p))")
        (apply-macete-with-minor-premises nondecreasing%sums)
        direct-and-antecedent-inference-strategy
        (backchain "with(p:prop, k:zz,   forall(n:zz,  k<=n implies p))")
        (contrapose "with(s:[zz,rr],k:zz,
    forall(n_$0:zz,
        forsome(k_$0:zz,
            n_$0<=k_$0 and not(#(lambda(j:zz,sum(k,j,s))(k_$0))))));")
        beta-reduce-repeatedly
        (instantiate-existential ("k"))
        (cut-with-single-formula "0<=sum(k,k_$1,s)")
        (apply-macete-with-minor-premises sum-nonnegativity)
        (prove-by-logic-and-simplification 3)
        (contrapose "with(p:prop, not(p))")
        (backchain "with(s:[zz,rr],k:zz,
    forall(n:zz,
        k<=n
          implies 
        0<=s(n) and #(sup(ran{lambda(p:zz,sum(k,p,s))}))));")
        (instantiate-existential ("k"))
        simplify
        (beta-reduce-antecedent "with(p:prop,  forall(eps:rr, 0<eps implies p))")
        (auto-instantiate-universal-antecedent "with(p:prop,  forall(eps:rr, 0<eps implies p))")
        (instantiate-existential ("max(k,k_$0)+1"))
        (instantiate-universal-antecedent "with(eps:rr,s:[zz,rr],k,k_$0:zz,
    forall(j_$0,j_$1:zz,
        k_$0<=j_$0 and j_$0<=j_$1
          implies 
        sum(k,j_$1,s)-sum(k,j_$0,s)<=eps));" ("j-1" "j_1"))
        (contrapose "with(p:prop, not(p))")
        (cut-with-single-formula "k_$0<=max(k,k_$0)")
        simplify
        (apply-macete-with-minor-premises maximum-2nd-arg)
        (simplify-antecedent "with(j_1,j:zz,not(j-1<=j_1));")
        (cut-with-single-formula "sum(k,j_1,s)==sum(k,j-1,s)+ sum((j-1)+1,j_1,s)")
        simplify
        (apply-macete-with-minor-premises sum-interval-additivity)
        (cut-with-single-formula "k<=max(k,k_$0)")
        simplify
        (apply-macete-with-minor-premises maximum-1st-arg)
        )
      )
    (theory h-o-real-arithmetic))