Intuitionize sqrtsq in iset.mm
Intuitionize sqrtsq in iset.mm

This is different from most of the square root theorems because we
know that A ^ 2 has a square root even without completeness.
Therefore a simple proof suffices even before we have tackled
completeness (we're doing things in this order on the theory
that absolute value - defined in terms of square root - will
be useful in proving completeness).

metamath/set.mm,metamath/set.mm,metamath/set.mm