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