let a, b be Nat; :: thesis: ( a is even & a,b are_coprime implies a - b,a + b are_coprime )
assume A1: ( a is even & a,b are_coprime ) ; :: thesis: a - b,a + b are_coprime
then not 2 divides a gcd b by NAT_D:7;
then A2: b is odd by A1, INT_2:def 2;
then A3: (a + b) gcd (a - b) is odd by A1, Th9;
A4: (a + b) gcd (a - b) <> 0 by A2, INT_2:5;

per cases ( a > b or a < b ) by A1, A2, XXREAL_0:1;

suppose a > b ; :: thesis: a - b,a + b are_coprime

then (a + b) gcd (a - b) <= 2 by A1, Th8;
then (a + b) gcd (a - b) < 2 by A3, XXREAL_0:1;
hence a - b,a + b are_coprime by A4, NAT_1:23; :: thesis: verum

end;

suppose a < b ; :: thesis: a - b,a + b are_coprime

then (a + b) gcd (b - a) <= 2 by A1, Th8;
then (a + b) gcd (- (b - a)) <= 2 by Th1;
then (a + b) gcd (a - b) < 2 by A3, XXREAL_0:1;
hence a - b,a + b are_coprime by A4, NAT_1:23; :: thesis: verum

end;

end;