prove that given a nonnegative integer n, there is a unique nonnegative integer m such that m^2 less than or equal to n less than (m+1)^2
This response is best in practice, but having encountered this problem in my research, I'd like to show a "conceptually-minimal" proof. The thing is that square root involves real numbers, and they are pretty complex objects since they are infinite. My proof uses only logic and properties of natural numbers, including induction.
So, suppose n is given. Towards contradiction, we assume that for every m, it is not the case that m^2 <= n < (m + 1)^2. Then we prove that for all m, m^2 <= n. We do it by induction.
Obviously, 0^2 <= n. Suppose that for some m, m^2 <= n, and we need to show that (m + 1)^2 <= n. Well, if n < (m + 1)^2, then we have m that contradicts our assumption in the previous paragraph.
Having proved that m^2 <= n for all n, we now get a contradiction by instantiating m with, say, n + 1.