theorem :: NEWTON02:76

for a, b, n being Nat st a,b are_coprime holds
((a - b) |^ 2) gcd (((a |^ 2) + (b |^ 2)) + (((n - 2) * a) * b)) = (((a |^ 2) + (b |^ 2)) + (((n - 2) * a) * b)) gcd n