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;

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;