(def-theorem sqrt-is-an-nth%root-special-case
*Remark: This entry is multiply defined. See: [1] [2]*
*"forall(x:rr,sqrt(x)==nth%root(2,x))"*
reverse
(usages rewrite)
(theory h-o-real-arithmetic)
(proof
(
unfold-defined-constants
simplify
)))

(def-theorem defined-nth%root-is-nonnegative
*Remark: This entry is multiply defined. See: [1] [2]*
*"forall(n:zz,x:rr, 1<=n implies #(nth%root(n,x)) iff 0<=x)"*
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(block
(script-comment
*"`direct-and-antecedent-inference-strategy' at (0 0 0)"*)
(cut-with-single-formula *"forsome(y:rr, nth%root(n,x)=y)"*)
(block
(script-comment *"`cut-with-single-formula' at (0)"*)
(antecedent-inference *"with(p:prop,forsome(y:rr,p));"*)
(incorporate-antecedent *"with(y,r:rr,r=y);"*)
(apply-macete-with-minor-premises
iota-free-characterization-of-nth%root)
direct-and-antecedent-inference-strategy
(backchain-backwards *"with(x,r:rr,r=x);"*)
(apply-macete-with-minor-premises weak-positivity-for-r^n)
simplify)
(instantiate-existential (*"nth%root(n,x)"*)))
(block
(script-comment
*"`direct-and-antecedent-inference-strategy' at (0 0 1)"*)
(apply-macete-with-minor-premises nth%root%existence)
simplify)
)))