let a, b be Nat; :: thesis: ( a <> b implies (2 * a) * b < (a |^ 2) + (b |^ 2) )
A0: ( a * a = a |^ 2 & b * b = b |^ 2 ) by NEWTON:81;
assume a <> b ; :: thesis: (2 * a) * b < (a |^ 2) + (b |^ 2)
then ( not a - b is zero & a - b is real & 2 is even ) ;
then A1: (a - b) |^ 2 > 0 ;
assume not (2 * a) * b < (a |^ 2) + (b |^ 2) ; :: thesis: contradiction
then ((2 * a) * b) - ((2 * a) * b) >= ((a |^ 2) + (b |^ 2)) - ((2 * a) * b) by XREAL_1:9;
then 0 >= (a - b) * (a - b) by A0;
hence contradiction by A1, NEWTON:81; :: thesis: verum