(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)
        )))