let a, b be Integer; :: thesis: ( a,b are_coprime implies ((a - b) * (a + b)) gcd (a * b) = 1 )
assume A1: a,b are_coprime ; :: thesis: ((a - b) * (a + b)) gcd (a * b) = 1
( a gcd b = a gcd (b - (1 * a)) & a gcd b = a gcd (b + (1 * a)) ) by NEWTON02:5;
then ( (- (a - b)) gcd a = 1 & (a + b) gcd a = 1 ) by A1;
then ( a - b,a are_coprime & a + b,a are_coprime ) by NEWTON02:1;
then A2: (a - b) * (a + b),a are_coprime by INT_2:26;
( b gcd a = b gcd (a - (1 * b)) & b gcd a = b gcd (a + (1 * b)) ) by NEWTON02:5;
then ( a - b,b are_coprime & a + b,b are_coprime ) by A1;
then (a - b) * (a + b),b are_coprime by INT_2:26;
then (a - b) * (a + b),a * b are_coprime by A2, INT_2:26;
hence ((a - b) * (a + b)) gcd (a * b) = 1 ; :: thesis: verum