let x, y be real number ; :: thesis: ( 1 <= x & 1 <= y & abs y <= abs x implies 0 < y - (sqrt ((y ^2 ) - 1)) )
assume A1: ( 1 <= x & 1 <= y & abs y <= abs x ) ; :: thesis: 0 < y - (sqrt ((y ^2 ) - 1))
then 1 * y <= y * y by XREAL_1:66;
then 1 <= y ^2 by A1, XXREAL_0:2;
then A2: 1 - 1 <= (y ^2 ) - 1 by XREAL_1:15;
(- 1) + (y ^2 ) < 0 + (y ^2 ) by XREAL_1:10;
then sqrt ((y ^2 ) - 1) < sqrt (y ^2 ) by A2, SQUARE_1:95;
then sqrt ((y ^2 ) - 1) < y by A1, SQUARE_1:89;
then (sqrt ((y ^2 ) - 1)) - (sqrt ((y ^2 ) - 1)) < y - (sqrt ((y ^2 ) - 1)) by XREAL_1:16;
hence 0 < y - (sqrt ((y ^2 ) - 1)) ; :: thesis: verum