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

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;

then A2: m > n by SQUARE_1:15;

per cases ( m is even or m is odd ) ;

suppose m is even ; :: thesis: contradiction

then consider a being Nat such that
A3: m = 2 * a ;

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: contradiction

then consider b being Nat such that
A4: n = 2 * b ;
((4 * a) * a) - ((4 * b) * b) = 4 by A1, A3, A4;
then A5: (a ^2) - (b ^2) = 1 ;
( a is positive & b is positive ) by A3, A4;
hence contradiction by A5, Th34; :: thesis: verum

end;

suppose n is odd ; :: thesis: contradiction

then consider b being Nat such that
A6: n = (2 * b) + 1 by ABIAN:9;
((4 * a) * a) - ((((4 * b) * b) + (4 * b)) + 1) = 4 by A1, A3, A6;
then ((a * a) - (b * b)) - b = 5 / 4 ;
hence contradiction by Lm2; :: thesis: verum

end;

end;

end;

suppose m is odd ; :: thesis: contradiction

then consider a being Nat such that
A7: m = (2 * a) + 1 by ABIAN:9;

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: contradiction

then consider b being Nat such that
A8: n = 2 * b ;
((((4 * a) * a) + (4 * a)) + 1) - ((4 * b) * b) = 4 by A1, A7, A8;
then ((a * a) + a) - (b * b) = 3 / 4 ;
hence contradiction by NAT_D:33; :: thesis: verum

end;

suppose n is odd ; :: thesis: contradiction

then consider b being Nat such that
A9: n = (2 * b) + 1 by ABIAN:9;
A10: ((((4 * a) * a) + (4 * a)) + 1) - ((((4 * b) * b) + (4 * b)) + 1) = 4 by A1, A7, A9;
((2 * b) + 1) - 1 < ((2 * a) + 1) - 1 by A2, A7, A9, XREAL_1:9;
then A11: b < a by XREAL_1:64;
then b ^2 < a ^2 by XREAL_1:96;
then (a ^2) - (b ^2) > (b ^2) - (b ^2) by XREAL_1:9;
then A12: (a ^2) - (b ^2) >= 0 + 1 by INT_1:7;
a - b > b - b by A11, XREAL_1:9;
then a - b >= 0 + 1 by INT_1:7;
then ((a ^2) - (b ^2)) + (a - b) >= 1 + 1 by A12, XREAL_1:7;
hence contradiction by A10; :: thesis: verum

end;

end;

end;

end;