given x, y being positive Nat such that A1: x * (x + 1) = (4 * y) * (y + 1) ; :: thesis: contradiction
((2 * ((2 * y) + 1)) ^2) - (((2 * x) + 1) ^2) = (((4 * y) - (2 * x)) + 1) * (((4 * y) + (2 * x)) + 3) ;
then A2: ((4 * y) + (2 * x)) + 3 divides 3 by A1;
0 + 3 < ((4 * y) + (2 * x)) + 3 by XREAL_1:8;
hence contradiction by A2, NAT_D:7; :: thesis: verum