(def-constant quadratic%bound 
    "lambda(f:[pp_0,pp_1], 
                          forsome(a:rr, 0<=a and forall(x,y:pp_0,#(f(x)) and #(f(y)) implies dist_1(f(x),f(y))<=dist_0(x,y)*(a+dist_0(x,y)))))"
    (theory metric-spaces-2-tuples))

(def-theorem quadratic-is-uniformly-continuous 
    "forall(f:[pp_0,pp_1], quadratic%bound(f) implies uniformly%continuous(f))"
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("min(1,eps/(1+a))"))
        (weaken (0))
        (unfold-single-defined-constant (0) min)
        (case-split ("1<=eps/(1+a)"))
        simplify
        simplify
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        (antecedent-inference "with(a,eps:rr,y_$0,x_$0:pp_0,f:[pp_0,pp_1],
    #(f(x_$0))
      and 
    #(f(y_$0))
      and 
    dist_0(x_$0,y_$0)<=min(1,eps/(1+a)));")
        (apply-macete-with-minor-premises transitivity-of-<=)
        (instantiate-existential ("dist_0(x_$0,y_$0)*(a+dist_0(x_$0,y_$0))"))
        (backchain "with(a:rr,f:[pp_0,pp_1],
    forall(x,y:pp_0,
        #(f(x)) and #(f(y))
          implies 
        dist_1(f(x),f(y))<=dist_0(x,y)*(a+dist_0(x,y))));")
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises transitivity-of-<=)
        (instantiate-existential ("(eps/(1+a))*(a+1)"))
        (apply-macete-with-minor-premises monotone-product-lemma)
        (cut-with-single-formula "min(1,eps/(1+a))<=1 and min(1,eps/(1+a))<=eps/(1+a)")
        simplify
        (apply-macete-with-minor-premises minimum-2nd-arg)
        (apply-macete-with-minor-premises minimum-1st-arg)
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        (instantiate-universal-antecedent "with(a:rr,f:[pp_0,pp_1],
    forall(x,y:pp_0,
        #(f(x)) and #(f(y))
          implies 
        dist_1(f(x),f(y))<=dist_0(x,y)*(a+dist_0(x,y))));" ("x_$0" "y_$0"))
        ))
    
    (usages transportable-macete)
    (theory metric-spaces-2-tuples))