let m, n be natural Number ; :: thesis: ( m ^2 <= n & n < (m + 1) ^2 implies [\(sqrt n)/] = m )
assume m ^2 <= n ; :: thesis: ( not n < (m + 1) ^2 or [\(sqrt n)/] = m )
then A1: sqrt (m ^2) <= sqrt n by SQUARE_1:26;
assume n < (m + 1) ^2 ; :: thesis: [\(sqrt n)/] = m
then A2: sqrt n < sqrt ((m + 1) ^2) by SQUARE_1:27;
A3: sqrt (m ^2) = m by SQUARE_1:def 2;
sqrt ((m + 1) ^2) = m + 1 by SQUARE_1:def 2;
then (sqrt n) - 1 < (m + 1) - 1 by A2, XREAL_1:14;
hence [\(sqrt n)/] = m by A1, A3, Def6; :: thesis: verum