The square root of x is defined to be a nonnegative number y such that (= (exp y (2)) x) /edit/peano_new/arithmetic/reals/sqrt_min.gh/df-sqrt.
Every positive number has no more than one square root as square roots are never
negative.
Theorems
(= (sqrt (/ a b)) (/ (sqrt a) (sqrt b))) /edit/peano_new/arithmetic/reals/sqrt.gh/sqrtdivi
(= (* (sqrt a) (sqrt b)) (sqrt (* a b))) /edit/peano_new/arithmetic/reals/sqrt.gh/sqrtmul