(def-theorem nn-addition-rewrite"forall(x,y:zz, #(x+y,nn) iff 0<=x+y)"(theory h-o-real-arithmetic) (usages rewrite) (proof (direct-and-antecedent-inference-strategy (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)))

(def-theorem ()"forall(x,y:nn,#(x+y,nn ))"(theory h-o-real-arithmetic) (proof ( (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic) simplify )) (usages d-r-convergence))

(def-theorem ()"forall(x,y:nn, #(x*y,nn ))"(theory h-o-real-arithmetic) (proof ( (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic) simplify (apply-macete-with-minor-premises positivity-for-products) simplify )) (usages d-r-convergence))

(def-theorem ()"forall(x,y:ind,#(x,nn) and #(y,nn) and y<=x implies #(x-y,nn ))"(theory h-o-real-arithmetic) (proof ( (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic) simplify )) (usages d-r-convergence))

(def-theorem ()"forall(x,y:ind,#(x,nn) and #(y,nn) and 1<=y implies #(x^y,nn ))"(theory h-o-real-arithmetic) (proof ( (cut-with-single-formula"forall(x,y:zz,1<=y and 0<=x implies #(x^y,zz) and 0<=x^y)") direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic) (instantiate-universal-antecedent"forall(x,y:zz,1<=y and 0<=x implies #(x^y,zz) and 0<=x^y);"("x""y")) (contrapose"with(x:ind,not(0<=x));") simplify beta-reduce-repeatedly (induction integer-inductor ("y")) (force-substitution"x^(1+t)""x^t*x"(0 1)) direct-inference simplify (apply-macete-with-minor-premises positivity-for-products) direct-and-antecedent-inference-strategy simplify )) (usages d-r-convergence))

(def-theorem ()"forall(j:zz, 0<=j implies #(j,nn))"(theory h-o-real-arithmetic) (proof ( (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic) simplify )) (usages d-r-convergence))

(def-theorem ()"forall(x:rr, 0<=x and #(x,zz) implies #(x,nn))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic) beta-reduce-repeatedly )) (usages d-r-convergence))

(def-theorem ()"forall(n:nn,#(n+[-1],nn) iff 0<n)"(theory h-o-real-arithmetic) (proof ( (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic) simplify direct-and-antecedent-inference-strategy simplify simplify )) (usages rewrite))

(def-theorem ()"forall(x:rr, #(abs(x)))"(theory h-o-real-arithmetic) (proof ( (unfold-single-defined-constant (0) abs) insistent-direct-inference beta-reduce-repeatedly )) (usages d-r-convergence))

(def-theorem ()"forall(x,y:rr, #(max(x,y)))"(theory h-o-real-arithmetic) (proof ( unfold-defined-constants insistent-direct-inference beta-reduce-repeatedly )) (usages d-r-convergence))

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

(def-theorem triangle-inequality"forall(x,y:rr,abs(x+y)<=abs(x)+abs(y))"(theory h-o-real-arithmetic) (proof ( unfold-defined-constants (prove-by-logic-and-simplification 3) )))

(def-theorem non-negativity-of-absolute-value"forall(x:rr,0<=abs(x))"(theory h-o-real-arithmetic) (proof ( unfold-defined-constants (prove-by-logic-and-simplification 3) )))

(def-theorem min-definedness"forall(x,y:rr,#(min(x,y)))"(theory h-o-real-arithmetic) (proof ( unfold-defined-constants insistent-direct-inference beta-reduce-repeatedly )) (usages d-r-convergence))

(def-theorem maximum-1st-arg"forall(x,y:rr,x<=max(x,y))"(theory h-o-real-arithmetic) (proof ( unfold-defined-constants (prove-by-logic-and-simplification 3) ) ))

(def-theorem maximum-2nd-arg"forall(x,y:rr,y<=max(x,y))"(theory h-o-real-arithmetic) (proof ( unfold-defined-constants (prove-by-logic-and-simplification 3) ) ))

(def-theorem minimum-1st-arg"forall(x,y:rr,min(x,y)<=x)"(theory h-o-real-arithmetic) (proof ( unfold-defined-constants (prove-by-logic-and-simplification 3) ) ))

(def-theorem minimum-2nd-arg"forall(x,y:rr,min(x,y)<=y)"(theory h-o-real-arithmetic) (proof ( unfold-defined-constants (prove-by-logic-and-simplification 3) ) ))

(def-theorem min-lemma"forall(a,b,c:rr, a<b and a<c implies forsome(d:rr, a<d and d<=b and d<=c))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (instantiate-existential ("min(b,c)")) (unfold-single-defined-constant-globally min) (case-split ("b<=c")) simplify simplify (apply-macete-with-minor-premises minimum-1st-arg) (apply-macete-with-minor-premises minimum-2nd-arg) )))

(def-theorem max-lemma"forall(a,b,c:rr, b<a and c<a implies forsome(d:rr, d<a and b<=d and c<=d))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (instantiate-existential ("max(b,c)")) (unfold-single-defined-constant-globally max) (case-split ("b<=c")) simplify simplify (apply-macete-with-minor-premises maximum-1st-arg) (apply-macete-with-minor-premises maximum-2nd-arg) )))