let y be Real; :: thesis: ( 1 <= y implies 0 < y - (sqrt ((y ^2) - 1)) )
assume A1: 1 <= y ; :: thesis: 0 < y - (sqrt ((y ^2) - 1))
then 1 * y <= y * y by XREAL_1:64;
then 1 <= y ^2 by A1, XXREAL_0:2;
then A2: 1 - 1 <= (y ^2) - 1 by XREAL_1:13;
(- 1) + (y ^2) < 0 + (y ^2) by XREAL_1:8;
then sqrt ((y ^2) - 1) < sqrt (y ^2) by A2, SQUARE_1:27;
then sqrt ((y ^2) - 1) < y by A1, SQUARE_1:22;
then (sqrt ((y ^2) - 1)) - (sqrt ((y ^2) - 1)) < y - (sqrt ((y ^2) - 1)) by XREAL_1:14;
hence 0 < y - (sqrt ((y ^2) - 1)) ; :: thesis: verum