theorem SDC: :: NEWTON06:46

for a, b being Integer st a,b are_coprime holds
((a - b) * (a + b)) gcd (a * b) = 1