theorem :: INT_1:75

for m, n being natural Number st m ^2 <= n & n < (m + 1) ^2 holds
[\(sqrt n)/] = m