given m, n being positive Nat such that A1: (m ^2) - (n ^2) = 1 ; :: thesis: contradiction

A2: now :: thesis: not m ^2 <= n ^2

assume m ^2 <= n ^2 ; :: thesis: contradiction
then (m ^2) - (n ^2) <= (n ^2) - (n ^2) by XREAL_1:9;
then (m ^2) - (n ^2) <= 0 ;
hence contradiction by A1; :: thesis: verum

end;

A3: sqrt (1 + (n * n)) <= (sqrt 1) + (sqrt (n ^2)) by SQUARE_1:59;
( sqrt (m ^2) = m & sqrt (n ^2) = n ) by SQUARE_1:def 2;
then ( m < 1 + n or m = 1 + n ) by A1, A3, XXREAL_0:1, SQUARE_1:18;

per cases then ( m <= n or m = 1 + n ) by NAT_1:13;

suppose m <= n ; :: thesis: contradiction

hence contradiction by A2, SQUARE_1:15; :: thesis: verum

end;

suppose m = 1 + n ; :: thesis: contradiction

then ((1 + n) ^2) - (n ^2) = 1 by A1;
then 2 * n = 0 ;
hence contradiction ; :: thesis: verum

end;

end;