(def-theorem metric-separation-for-reals  
    "forall(x,y:rr,x=y 
      iff
  forall(r:rr,0<r implies forsome(z:rr, abs(z-x)<=r and abs(z-y)<=r)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (backchain "with(y,x:rr,x=y);")
        (instantiate-existential ("y"))
        (block 
            (script-comment "proving abs(y-y)=0")
            (unfold-single-defined-constant (0) abs)
            (prove-by-logic-and-simplification 3))
        (instantiate-universal-antecedent "with(p:prop,p);" ("abs(x-y)/3"))
        (contrapose "with(p:prop,p);")
        (block 
            (script-comment "prove 0<abs(x-y)/3")
            (unfold-single-defined-constant (0) abs)
            (case-split ("0<=x-y"))
            simplify
            simplify)
        (block 
            (script-comment "the distance from z_$0 to both x and y is less 
                                              than a third of the distance between x and y")
            (apply-macete-with-minor-premises point-separation-for-rr-distance)
            beta-reduce-repeatedly
            (cut-with-single-formula "abs(x-y)<=abs(z_$0-y)+abs(z_$0-x)")
            simplify)
        (weaken (0 1))
        (force-substitution "x-y" "(x-z_$0)+(z_$0-y)" (0))
        (force-substitution "abs(z_$0-y)+abs(z_$0-x)" "abs(x-z_$0)+abs(z_$0-y)" (0))
        (apply-macete-with-minor-premises triangle-inequality)
        (block 
            (script-comment "another triviality.")
            (force-substitution "z_$0-x" "[-1]*(x-z_$0)" (0))
            (apply-macete-with-minor-premises absolute-value-product)
            (apply-macete absolute-value-non-positive)
            simplify
            simplify)
        simplify
        )))

(def-constant lim%rr 
    "lambda(s:[zz,rr],iota(x:rr, forall(eps:rr,0<eps implies forsome(n:zz, 
                forall(p:zz, n<=p implies abs(x-s(p))<=eps)))))"
    (theory h-o-real-arithmetic))

(def-theorem characterization-of-real-limit 
    "forall(s:[zz,rr],x:rr,lim%rr(s)=x iff forall(eps:rr,0<eps implies forsome(n:zz, 
forall(p:zz, n<=p implies abs(x-s(p))<=eps))))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant (0) lim%rr)
        direct-and-antecedent-inference-strategy
        (contrapose "with(x,r:rr,r=x);")
        (block 
            (eliminate-defined-iota-expression 0 w)
            (contrapose "with(p:prop,forall(eps:rr,0<eps implies forsome(n:zz,p)));")
            auto-instantiate-existential
            (backchain "with(x,w:rr,w=x);")
            (backchain "with(p:prop,forall(n:zz,forsome(p:zz,with(p:prop,p))));"))
        (apply-macete-with-minor-premises eliminate-iota-macete)
        direct-and-antecedent-inference-strategy
        (block 
            (script-comment "uniqueness.")
            (apply-macete-with-minor-premises metric-separation-for-reals)
            direct-and-antecedent-inference-strategy
              
            (instantiate-universal-antecedent
              "with(p:prop,forall(eps:rr,0<eps implies forsome(n:zz,p)));"
              ("r"))
            (instantiate-universal-antecedent
              "with(p:prop,forall(eps:rr,0<eps implies forsome(n:zz,p)));"
              ("r"))
            (instantiate-existential ("s(max(n,n_$0))"))
            (cut-with-single-formula "forall(x,y:rr,abs(x-y)=abs(y-x))")
            (backchain "with(p:prop,forall(x,y:rr,p));")
            (backchain "with(r:rr,s:[zz,rr],b_$0:rr,n:zz,
    forall(p:zz,n<=p implies abs(b_$0-s(p))<=r));")
            (apply-macete-with-minor-premises maximum-1st-arg)
            (cut-with-single-formula "abs(b_$0-s(max(n,n_$0)))<=r")
            (script-comment "we needed definedness here.")
            (force-substitution "y-x" "[-1]*(x-y)" (0))
            (apply-macete-with-minor-premises absolute-value-product)
            (apply-macete absolute-value-non-positive)
            simplify
            simplify
            (cut-with-single-formula "forall(x,y:rr, abs(x-y)=abs(y-x))")
            (backchain "with(p:prop,forall(x,y:rr,p));")
            (backchain "with(r:rr,s:[zz,rr],x:rr,n_$0:zz,
    forall(p:zz,n_$0<=p implies abs(x-s(p))<=r));")
            (apply-macete-with-minor-premises maximum-2nd-arg)
            (cut-with-single-formula "abs(b_$0-s(max(n,n_$0)))<=r")
            (backchain "with(r:rr,s:[zz,rr],b_$0:rr,n:zz,
    forall(p:zz,n<=p implies abs(b_$0-s(p))<=r));")
            (apply-macete-with-minor-premises maximum-1st-arg))
        )))

(def-theorem abs-free-characterization-of-real-limit 
    "forall(s:[zz,rr],x:rr,
          lim%rr(s)=x
            iff 
          forall(eps:rr,
              0<eps
                implies 
              forsome(n:zz,
                  forall(p:zz,
                      n<=p implies x-eps<=s(p) and s(p)<=x+eps))))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (apply-macete-with-minor-premises characterization-of-real-limit)
        (force-substitution "abs(x-s(p))<=eps" "x-eps<=s(p) and s(p)<=x+eps" (0))
        (case-split ("#(s(p))"))
        (unfold-single-defined-constant (0) abs)
        (case-split ("s(p)<=x"))
        simplify
        simplify
        direct-and-antecedent-inference-strategy
        )))

(def-theorem existence-of-real-limit 
    "forall(s:[zz,rr],
        #(lim%rr(s))
          iff 
        forsome(x:rr,
            forall(eps:rr,
                0<eps
                  implies 
                forsome(n:zz,
                    forall(p:zz,n<=p implies abs(x-s(p))<=eps)))))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "lim%rr(s)=lim%rr(s)")
        (incorporate-antecedent "with(s:[zz,rr],lim%rr(s)=lim%rr(s));")
        (apply-macete-with-minor-premises characterization-of-real-limit)
        direct-inference
        (instantiate-existential ("lim%rr(s)"))
        (cut-with-single-formula "lim%rr(s)=x")
        (apply-macete-with-minor-premises characterization-of-real-limit)
        )
      ))

(def-theorem homogeneity-of-real-limit 
    "forall(a:[zz,rr], b:rr, #(lim%rr(a)) implies 
                    lim%rr(lambda(n:zz,b*a(n)))=b*lim%rr(a))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(s:rr, lim%rr(a)=s)")
        (antecedent-inference "with(a:[zz,rr],forsome(s:rr,lim%rr(a)=s));")
        (backchain "with(s:rr,a:[zz,rr],lim%rr(a)=s);")
        (apply-macete-with-minor-premises characterization-of-real-limit)
        direct-and-antecedent-inference-strategy
        beta-reduce-with-minor-premises
        (force-substitution "b*s-b*a(p)" "b*(s-a(p))" (0))
        (apply-macete-with-minor-premises absolute-value-product)
        (case-split ("abs(b)=0"))
        simplify
        (incorporate-antecedent "with(a:[zz,rr],#(lim%rr(a)));")
        (apply-macete-with-minor-premises existence-of-real-limit)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent 
          "with(p:prop, forall(eps:rr, 0<eps implies p))" ("1"))
        (simplify-antecedent "not(0<1);")
        (instantiate-existential ("n"))
        (instantiate-universal-antecedent "with(a:[zz,rr],x:rr,n:zz,
    forall(p:zz,n<=p implies abs(x-a(p))<=1));" ("p"))
        (force-substitution "abs(b)*abs(s-a(p))<=eps" "abs(s-a(p))<=eps/abs(b)" (0))
        (incorporate-antecedent "with(s:rr,a:[zz,rr],lim%rr(a)=s);")
        (apply-macete-with-minor-premises characterization-of-real-limit)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent 
            "with(p:prop, forall(eps:rr, 0<eps implies p))" ("eps/abs(b)"))
        (contrapose "with(b,eps:rr,not(0<eps/abs(b)));")
        simplify
        (cut-with-single-formula "0<abs(b)")
        simplify
        (apply-macete-with-minor-premises positivity-of-inverse)
        simplify
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        simplify
        (instantiate-existential ("lim%rr(a)"))
        )))

(def-theorem lim%rr-negative 
    "forall(a:[zz,rr], b:rr,
                    lim%rr(lambda(n:zz,[-1]*a(n)))==-lim%rr(a))"  
    (theory h-o-real-arithmetic)
    (proof
      (
        insistent-direct-inference-strategy
        (antecedent-inference "with(a:[zz,rr],
    #(lim%rr(lambda(n:zz,[-1]*a(n)))) or #(-lim%rr(a)));")
        (force-substitution "a" "lambda(n:zz,[-1]*lambda(n:zz,[-1]*a(n))(n))" (1))
        (apply-macete-locally homogeneity-of-real-limit (0) "lim%rr(lambda(n:zz,[-1]*lambda(n:zz,[-1]*a(n))(n)))")
        simplify
        insistent-direct-inference
        extensionality
        direct-and-antecedent-inference-strategy
        beta-reduce-repeatedly
        simplify
        (apply-macete-with-minor-premises homogeneity-of-real-limit)
        simplify
        )))

(def-theorem lim%rr-preserves-upper-bound 
    "forall(a:[nn,rr], b:rr, forall(i:nn, a(i)<=b) and #(lim%rr(a)) implies lim%rr(a)<=b)"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(s:rr, lim%rr(a)=s)")
        (antecedent-inference "with(a:[nn,rr],forsome(s:rr,lim%rr(a)=s));")
        (backchain "with(s:rr,a:[nn,rr],lim%rr(a)=s);")
        (incorporate-antecedent "with(s:rr,a:[nn,rr],lim%rr(a)=s);")
        (apply-macete-with-minor-premises abs-free-characterization-of-real-limit)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent
          "with(p:prop,  forall(eps:rr, 0<eps implies p))"
          ("(s-b)/2"))
        simplify
        (instantiate-universal-antecedent "with(a:[nn,rr],b,s:rr,n_$0:zz,
    forall(p_$0:zz,
        n_$0<=p_$0
          implies 
        s-(s-b)/2<=a(p_$0) and a(p_$0)<=s+(s-b)/2));" ("n_$0"))
        (simplify-antecedent "with(n_$0:zz,not(n_$0<=n_$0));")
        (instantiate-universal-antecedent "with(b:rr,a:[nn,rr],forall(i:nn,a(i)<=b));" ("n_$0"))
        simplify
        (instantiate-existential ("lim%rr(a)"))
        )))

(def-theorem lim%rr-preserves-lower-bound 
    "forall(a:[nn,rr], b:rr, forall(i:nn, b<=a(i)) and #(lim%rr(a)) 
                            implies
                  b<=lim%rr(a))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "lim%rr(lambda(n:zz,[-1]*a(n)))<=-b")
        (incorporate-antecedent "with(b:rr,a:[nn,rr],lim%rr(lambda(n:zz,[-1]*a(n)))<=-b);")
        (apply-macete-with-minor-premises homogeneity-of-real-limit)
        simplify
        (apply-macete-with-minor-premises lim%rr-preserves-upper-bound)
        direct-and-antecedent-inference-strategy
        simplify
        (apply-macete-with-minor-premises homogeneity-of-real-limit)
        simplify
        (weaken (0 1))
        sort-definedness
        direct-and-antecedent-inference-strategy
        (case-split ("#(xx_0,zz)"))
        (beta-reduce-antecedent "with(xx_0:ind,a:[nn,rr],#(lambda(n:zz,[-1]*a(n))(xx_0)));")
        )))

(def-constant bounded%non%decreasing%seq 
    "lambda(a:[nn,rr], forsome(b:rr, forall(n:nn, a(n)<=a(n+1) and a(n)<=b)))"
    (theory h-o-real-arithmetic))

(def-theorem bounded%non%decreasing%seq-convergent 
    "forall(a:[nn,rr], bounded%non%decreasing%seq(a) 
                                                implies
                                          forall(n:nn, a(n)<=lim%rr(a)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant (0) bounded%non%decreasing%seq)
        direct-and-antecedent-inference-strategy
        (instantiate-theorem completeness ("lambda(x:rr, forsome(n:nn, x=a(n)))"))
        (contrapose "with(a:[nn,rr],
    forall(x_0:rr,not(lambda(x:rr,forsome(n:nn,x=a(n)))(x_0))));")
        (instantiate-existential ("a(0)"))
        beta-reduce-with-minor-premises
        (instantiate-existential ("0"))
        simplify
        (instantiate-universal-antecedent "with(b:rr,a:[nn,rr],forall(n:nn,a(n)<=a(n+1) and a(n)<=b));" ("0"))
        (beta-reduce-antecedent "with(a:[nn,rr],
    forall(alpha:rr,
        forsome(theta:rr,
            lambda(x:rr,forsome(n:nn,x=a(n)))(theta)
              and 
            not(theta<=alpha))));")
        (contrapose "with(a:[nn,rr],
    forall(alpha:rr,
        forsome(theta:rr,
            forsome(n:nn,theta=a(n)) and not(theta<=alpha))));")
        (instantiate-existential ("b"))
        (antecedent-inference "with(a:[nn,rr],theta:rr,forsome(n:nn,theta=a(n)));")
        (backchain "with(n_$0:nn,a:[nn,rr],theta:rr,theta=a(n_$0));")
        (beta-reduce-antecedent "with(gamma:rr,a:[nn,rr],
    forall(theta:rr,
        lambda(x:rr,forsome(n:nn,x=a(n)))(theta)
          implies 
        theta<=gamma));")
        (cut-with-single-formula "lim%rr(a)=gamma")
        (backchain "with(gamma:rr,a:[nn,rr],lim%rr(a)=gamma);")
        (backchain "with(gamma:rr,a:[nn,rr],
    forall(theta:rr,
        forsome(n:nn,theta=a(n)) implies theta<=gamma));")
        (instantiate-existential ("n"))
        (apply-macete-with-minor-premises abs-free-characterization-of-real-limit)
        direct-and-antecedent-inference-strategy
        (beta-reduce-antecedent "with(gamma:rr,a:[nn,rr],
    forall(gamma_1:rr,
        forall(theta:rr,
            lambda(x:rr,forsome(n:nn,x=a(n)))(theta)
              implies 
            theta<=gamma_1)
          implies 
        gamma<=gamma_1));")
        (instantiate-universal-antecedent "with(gamma:rr,a:[nn,rr],
    forall(gamma_1:rr,
        forall(theta:rr,
            forsome(n:nn,theta=a(n)) implies theta<=gamma_1)
          implies 
        gamma<=gamma_1));" ("gamma-eps"))
        (contrapose "with(eps,gamma,theta_$0:rr,not(theta_$0<=gamma-eps));")
        (backchain "with(n_$0:nn,a:[nn,rr],theta_$0:rr,theta_$0=a(n_$0));")
        (instantiate-universal-antecedent "with(a:[nn,rr],eps,gamma:rr,
    forall(n:zz,
        forsome(p:zz,
            n<=p
              and 
            (not(gamma-eps<=a(p)) or not(a(p)<=gamma+eps)))));" ("n_$0"))
        (cut-with-single-formula "a(n_$0)<=a(p)")
        simplify
        (weaken (0 2 3 4))
        (induction integer-inductor ("p"))
        (instantiate-universal-antecedent "with(b:rr,a:[nn,rr],forall(n:nn,a(n)<=a(n+1) and a(n)<=b));" ("t"))
        simplify
        (instantiate-universal-antecedent "with(gamma:rr,a:[nn,rr],
    forall(theta:rr,
        forsome(n:nn,theta=a(n)) implies theta<=gamma));" ("a(p)"))
        (instantiate-universal-antecedent "with(p:zz,a:[nn,rr],forall(n_$0:nn,not(a(p)=a(n_$0))));" ("p"))
        (simplify-antecedent "with(p:zz,a:[nn,rr],not(a(p)=a(p)));")
        (instantiate-universal-antecedent "with(b:rr,a:[nn,rr],forall(n:nn,a(n)<=a(n+1) and a(n)<=b));" ("p"))
        (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
        simplify
        (cut-with-single-formula "0<=n_$0")
        simplify
        (apply-macete-with-minor-premises nn-in-quasi-sort_h-o-real-arithmetic)
        (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
        simplify
        (cut-with-single-formula "0<=n_$0")
        simplify
        (apply-macete-with-minor-premises nn-in-quasi-sort_h-o-real-arithmetic)
        (simplify-antecedent "with(eps,gamma:rr,p:zz,a:[nn,rr],not(a(p)<=gamma+eps));")
        (cut-with-single-formula "a(n_$0)<=a(p)")
        (weaken (0 2 3 4))
        (simplify-antecedent "with(eps,gamma:rr,gamma<=gamma-eps);")
        )))

(def-constant bounded%non%increasing%seq 
    "lambda(a:[nn,rr], forsome(b:rr, forall(n:nn, a(n+1)<=a(n) and b<=a(n))))"
    (theory h-o-real-arithmetic))

(def-theorem bounded%nonincreasing%seq-convergent 
    "forall(a:[nn,rr], bounded%non%increasing%seq(a) 
                                                implies
                                          forall(n:nn, lim%rr(a)<=a(n)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant (0) bounded%non%increasing%seq)
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "lambda(n:zz,[-1]*a(n))(n)<=lim%rr(lambda(n:zz,[-1]*a(n))) ")
        (cut-with-single-formula "#(lim%rr(lambda(n:zz,[-1]*a(n))))")
        (incorporate-antecedent "with(n:nn,a:[nn,rr],
    lambda(n:zz,[-1]*a(n))(n)<=lim%rr(lambda(n:zz,[-1]*a(n))));")
        (apply-macete-with-minor-premises homogeneity-of-real-limit)
        simplify
        (incorporate-antecedent "with(a:[nn,rr],#(lim%rr(lambda(n:zz,[-1]*a(n)))));")
        (apply-macete-with-minor-premises lim%rr-negative)
        simplify
        (apply-macete-with-minor-premises bounded%non%decreasing%seq-convergent)
        (unfold-single-defined-constant (0) bounded%non%decreasing%seq)
        beta-reduce-with-minor-premises
        (instantiate-existential ("-b"))
        beta-reduce-repeatedly
        simplify
        (instantiate-universal-antecedent "with(b:rr,a:[nn,rr],forall(n:nn,a(n+1)<=a(n) and b<=a(n)));" ("n_$0"))
        simplify
        beta-reduce-repeatedly
        simplify
        (weaken (0))
        sort-definedness
        direct-and-antecedent-inference-strategy
        (case-split ("#(xx_0,zz)"))
        simplify
        )))

(def-theorem additivity-of-real-limit 
    "forall(a,b:[zz,rr],  #(lim%rr(a)) and #(lim%rr(b)) implies 
                    lim%rr(lambda(n:zz,a(n)+b(n)))=lim%rr(a)+lim%rr(b))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(s,t:rr, lim%rr(a)=s and lim%rr(b)=t)")
        (antecedent-inference "with(b,a:[zz,rr],
    forsome(s,t:rr,lim%rr(a)=s and lim%rr(b)=t));")
        (backchain "with(t:rr,b:[zz,rr],s:rr,a:[zz,rr],
    lim%rr(a)=s and lim%rr(b)=t);")
        (backchain "with(t:rr,b:[zz,rr],s:rr,a:[zz,rr],
    lim%rr(a)=s and lim%rr(b)=t);")
        (apply-macete-with-minor-premises abs-free-characterization-of-real-limit)
        direct-and-antecedent-inference-strategy
        beta-reduce-repeatedly
        (incorporate-antecedent "with(t:rr,b:[zz,rr],s:rr,a:[zz,rr],
    lim%rr(a)=s and lim%rr(b)=t);")
        (apply-macete-with-minor-premises abs-free-characterization-of-real-limit)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(p:prop,  forall(eps:rr, 0<eps  implies p))" ("eps/2"))
        (simplify-antecedent "with(eps:rr,not(0<eps/2));")
        (instantiate-universal-antecedent "with(p:prop,  forall(eps:rr, 0<eps  implies p))" ("eps/2"))
        (simplify-antecedent "with(eps:rr,not(0<eps/2));")
        (cut-with-single-formula "forsome(s:zz, n_$1<=s and n_$0<=s)")
        (antecedent-inference "with(n_$0,n_$1:zz,forsome(s:zz,n_$1<=s and n_$0<=s));")
        (instantiate-existential ("s_$0"))
        (instantiate-universal-antecedent "with(a:[zz,rr],eps,s:rr,n_$1:zz,
    forall(p_$0:zz,
        n_$1<=p_$0 implies 
        s-eps/2<=a(p_$0) and a(p_$0)<=s+eps/2));" ("p"))
        (simplify-antecedent "with(p,n_$1:zz,not(n_$1<=p));")
        (instantiate-universal-antecedent "with(b:[zz,rr],eps,t:rr,n_$0:zz,
    forall(p_$0:zz,
        n_$0<=p_$0 implies 
        t-eps/2<=b(p_$0) and b(p_$0)<=t+eps/2));" ("p"))
        (simplify-antecedent "with(p,n_$0:zz,not(n_$0<=p));")
        simplify
        (instantiate-universal-antecedent "with(a:[zz,rr],eps,s:rr,n_$1:zz,
    forall(p_$0:zz,
        n_$1<=p_$0 implies 
        s-eps/2<=a(p_$0) and a(p_$0)<=s+eps/2));" ("p"))
        (simplify-antecedent "with(p,n_$1:zz,not(n_$1<=p));")
        (instantiate-universal-antecedent "with(b:[zz,rr],eps,t:rr,n_$0:zz,
    forall(p_$0:zz,
        n_$0<=p_$0 implies 
        t-eps/2<=b(p_$0) and b(p_$0)<=t+eps/2));" ("p"))
        (simplify-antecedent "with(p,n_$0:zz,not(n_$0<=p));")
        simplify
        (instantiate-existential ("max(n_$1,n_$0)"))
        simplify
        simplify
        (instantiate-existential ("lim%rr(a)" "lim%rr(b)"))
        )))

(def-theorem real-convergent-bounded 
    "forall(a:[zz,rr], #(lim%rr(a))  
          implies 
      forsome(u:rr, k:zz, forall(n:zz, k<=n implies  abs(a(n))<=u)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (apply-macete-with-minor-premises existence-of-real-limit)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(p:prop,
    forall(eps:rr,  0<eps implies p))" ("1"))
        (simplify-antecedent "not(0<1);")
        (instantiate-existential ("abs(x)+1" "n"))
        (cut-with-single-formula "abs(a(n_$0))-abs(x)<=abs(x-a(n_$0))")
        (instantiate-universal-antecedent "with(q:prop,forall(p:zz,q))" ("n_$0"))
        simplify
        (cut-with-single-formula "forall(a,b:rr, abs(a)-abs(b)<=abs(b-a))")
        (backchain "forall(a,b:rr,abs(a)-abs(b)<=abs(b-a));")
        (instantiate-universal-antecedent "with(a:[zz,rr],x:rr,n:zz,
    forall(p:zz,n<=p implies abs(x-a(p))<=1));" ("n_$0"))
        (weaken (0 1))
        unfold-defined-constants
        (prove-by-logic-and-simplification 3)
        )))

(def-theorem limit-of-constants 
    "forall(s:rr, lim%rr(lambda(k:zz, s))=s)"
    (theory h-o-real-arithmetic)
    (proof
      (
        (apply-macete-with-minor-premises abs-free-characterization-of-real-limit)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("0"))
        beta-reduce-repeatedly
        simplify
        simplify
        )))

(def-theorem real-limit-square 
    "forall(a:[zz,rr],  #(lim%rr(a))  implies 
                    lim%rr(lambda(n:zz,a(n)^2))=lim%rr(a)^2)"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(s:rr,lim%rr(a)=s)")
        (move-to-sibling 1)
        (instantiate-existential ("lim%rr(a)"))
        (antecedent-inference "with(a:[zz,rr],forsome(s:rr,lim%rr(a)=s));")
        (backchain-repeatedly ("with(s:rr,a:[zz,rr],lim%rr(a)=s);"))
        (incorporate-antecedent "with(s:rr,a:[zz,rr],lim%rr(a)=s);")
        (apply-macete-with-minor-premises characterization-of-real-limit)
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(m:rr,p:zz, forall(k:zz,p<=k implies abs(s+a(k))<=m))")
        (move-to-sibling 1)
        (force-substitution "s+a(k)" "lambda(k:zz,s+a(k))(k)" (0))
        (move-to-sibling 1)
        beta-reduce-repeatedly
        (apply-macete-with-minor-premises real-convergent-bounded)
        (force-substitution "s" "lambda(k:zz,s)(k)" (0))
        (apply-macete-with-minor-premises additivity-of-real-limit)
        simplify
        (apply-macete-with-minor-premises limit-of-constants)
        simplify
        beta-reduce-repeatedly
        (antecedent-inference "with(a:[zz,rr],s:rr,
    forsome(m:rr,p:zz,
        forall(k:zz,p<=k implies abs(s+a(k))<=m)));")
        (instantiate-universal-antecedent "with(a:[zz,rr],s:rr,
    forall(eps:rr,
        0<eps
          implies 
        forsome(n:zz,
            forall(p:zz,n<=p implies abs(s-a(p))<=eps))));" ("eps/max(1,m)"))
        (contrapose "with(m,eps:rr,not(0<eps/max(1,m)));")
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        (instantiate-existential ("max(n_$0,p)"))
        (force-substitution "s^2-a(p_$0)^2" "(s-a(p_$0))*(s+a(p_$0))" (0))
        (move-to-sibling 1)
        (cut-with-single-formula "#(a(p_$0))")
        simplify
        (instantiate-universal-antecedent "with(m:rr,a:[zz,rr],s:rr,p:zz,
    forall(k:zz,p<=k implies abs(s+a(k))<=m));" ("p_$0"))
        (cut-with-single-formula "p<=max(n_$0,p)")
        simplify
        (apply-macete-with-minor-premises maximum-2nd-arg)
        (apply-macete-with-minor-premises transitivity-of-<=)
        (instantiate-existential ("(eps/max(1,m))*m"))
        (apply-macete-with-minor-premises absolute-value-product)
        (apply-macete-with-minor-premises monotone-product-lemma)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises non-negativity-of-absolute-value)
        (backchain "with(m,eps:rr,a:[zz,rr],s:rr,n_$0:zz,
    forall(p_$0:zz,
        n_$0<=p_$0 implies abs(s-a(p_$0))<=eps/max(1,m)));")
        (cut-with-single-formula "n_$0<=max(n_$0,p)")
        simplify
        (apply-macete-with-minor-premises maximum-1st-arg)
        (apply-macete-with-minor-premises non-negativity-of-absolute-value)
        (backchain "with(m:rr,a:[zz,rr],s:rr,p:zz,
    forall(k:zz,p<=k implies abs(s+a(k))<=m));")
        (cut-with-single-formula "p<=max(n_$0,p)")
        simplify
        (apply-macete-with-minor-premises maximum-2nd-arg)
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        )))

(def-theorem product-in-terms-of-squares-lemma 
  Remark: This entry is multiply defined. See:  [1] [2]
    "forall(a,b:rr, a*b=1/2*((a+b)^2+[-1]*(a^2+b^2)))"
    
    (proof
      (
        simplify
        ))
    (theory h-o-real-arithmetic))

(def-schematic-macete abstraction-builder-for-sums-of-sequences
    "with(a,b:rr,
              lim%rr(lambda(x:zz,a+b))=lim%rr(lambda(x:zz,lambda(x:zz,a)(x)+lambda(x:zz,b)(x))))"
    (theory h-o-real-arithmetic)
    null)

(def-schematic-macete abstraction-builder-for-products-of-sequences
    "with(a,b:rr,
              lim%rr(lambda(x:zz,a*b))=lim%rr(lambda(x:zz,lambda(x:zz,a)(x)*lambda(x:zz,b)(x))))"
    (theory h-o-real-arithmetic)
    null)

(def-schematic-macete abstraction-builder-for-squares-of-sequences
    "with(a:rr, lim%rr(lambda(x:zz,a^2))=lim%rr(lambda(x:zz,lambda(x:zz,a)(x)^2)))"
    (theory h-o-real-arithmetic)
    null)

(def-compound-macete abstraction-for-sequences 
    (series
      (sound
        abstraction-builder-for-sums-of-sequences
        beta-reduce-repeatedly
        beta-reduce-repeatedly)
      (sound
        abstraction-builder-for-products-of-sequences
        beta-reduce-repeatedly
        beta-reduce-repeatedly)
      (sound
        abstraction-builder-for-squares-of-sequences
        beta-reduce-repeatedly
        beta-reduce-repeatedly)))

(def-theorem homogeneity-of-real-limit-corollary 
    "forall(a:[zz,rr], s,b:rr, b*lim%rr(a)=s implies 
                                                          lim%rr(lambda(n:zz,b*a(n)))=s)"
    (theory h-o-real-arithmetic)
    (proof
      (
        (apply-macete-with-minor-premises homogeneity-of-real-limit)
        )))

(def-theorem additivity-of-real-limit-corollary 
    "forall(a,b:[zz,rr], s:rr, lim%rr(a)+lim%rr(b)=s
                                                  implies 
                                                  lim%rr(lambda(n:zz,a(n)+b(n)))=s)"
    (theory h-o-real-arithmetic)
    (proof
      (
        (apply-macete-with-minor-premises additivity-of-real-limit)
        )))

(def-theorem real-limit-square-corollary 
    "forall(a:[zz,rr], s:rr, lim%rr(a)^2=s
                        implies 
                    lim%rr(lambda(n:zz,a(n)^2))=s)"
    (theory h-o-real-arithmetic)
    (proof
      (
        (apply-macete-with-minor-premises real-limit-square)
        )))

(def-theorem equal-arguments-implies-equal 
    "forall(op:[rr,rr,rr],a,b,c,d:rr, a=c and b=d and #(op(a,b)) implies op(a,b)=op(c,d))"
    (theory h-o-real-arithmetic)
    (proof
      (
        simplify
        )))

(def-theorem real-limit-product 
    "forall(a,b:[zz,rr],  #(lim%rr(a))  and  #(lim%rr(b))implies 
                    lim%rr(lambda(n:zz,a(n)*b(n)))=lim%rr(a)*lim%rr(b))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises product-in-terms-of-squares-lemma)
        (force-substitution "((a(n)+b(n))^2+[-1]*(a(n)^2+b(n)^2))" "lambda(n:zz,((a(n)+b(n))^2+[-1]*(a(n)^2+b(n)^2)))(n)" (0))
        (move-to-sibling 1)
        beta-reduce-repeatedly
        (apply-macete homogeneity-of-real-limit-corollary)
        (apply-macete-with-minor-premises equal-arguments-implies-equal)
        direct-and-antecedent-inference-strategy
        simplify
        (apply-macete-with-minor-premises abstraction-for-sequences)
        (apply-macete additivity-of-real-limit-corollary)
        (apply-macete-with-minor-premises equal-arguments-implies-equal)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises abstraction-for-sequences)
        (apply-macete real-limit-square-corollary)
        (apply-macete-with-minor-premises abstraction-for-sequences)
        (apply-macete-with-minor-premises equal-arguments-implies-equal)
        direct-and-antecedent-inference-strategy
        beta-reduce-repeatedly
        (weaken (0))
        (apply-macete-with-minor-premises additivity-of-real-limit-corollary)
        simplify
        definedness
        (force-substitution "(a(n)^2+b(n)^2)" "lambda(n:zz,(a(n)^2+b(n)^2))(n)" (0))
        (apply-macete homogeneity-of-real-limit-corollary)
        (apply-macete-with-minor-premises equal-arguments-implies-equal)
        direct-and-antecedent-inference-strategy
        (weaken (2 1 0))
        (apply-macete-with-minor-premises abstraction-for-sequences)
        (apply-macete additivity-of-real-limit-corollary)
        (apply-macete equal-arguments-implies-equal)
        direct-and-antecedent-inference-strategy
        (apply-macete real-limit-square-corollary)
        simplify
        (weaken (0))
        (apply-macete real-limit-square-corollary)
        simplify
        definedness
        definedness
        beta-reduce-repeatedly
        definedness
        definedness
        )))