Recently i was asked to formalize the following sqroot definition:

We define the sqroot of a non negative No x ( x>=0),symbolized as sqroot(x), another non negative No y such that when we raise y to the power of two we get x.

Real Nos of course

Although i have an idea your ideas will be appreciated

And then to prove the relevant theorems in a formalized manner