for a, b being positive Nat holds (2 * a) * b divides ((a + b) |^ 2) - ((a |^ 2) + (b |^ 2)) by Th55, INT_2:28;