theorem Th74: :: NEWTON02:74

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