theorem Th55: :: NEWTON02:55

for a, b being Nat st a <> b holds
(2 * a) * b < (a |^ 2) + (b |^ 2)