let a, b be Nat; :: thesis: ( a gcd b = 1 implies (a + b) gcd b = 1 )
assume A1: a gcd b = 1 ; :: thesis: (a + b) gcd b = 1
set n = (a + b) gcd b;
A2: (a + b) gcd b divides b by NAT_D:def 5;
(a + b) gcd b divides a + b by NAT_D:def 5;
then (a + b) gcd b divides a by A2, NAT_D:10;
then (a + b) gcd b divides a gcd b by A2, NEWTON:50;
then A3: (a + b) gcd b <= 1 + 0 by A1, NAT_D:7;

per cases ( (a + b) gcd b = 1 or (a + b) gcd b = 0 ) by A3, NAT_1:9;

suppose (a + b) gcd b = 1 ; :: thesis: (a + b) gcd b = 1

hence (a + b) gcd b = 1 ; :: thesis: verum

end;

suppose (a + b) gcd b = 0 ; :: thesis: (a + b) gcd b = 1

then b = 0 by INT_2:5;
hence (a + b) gcd b = 1 by A1; :: thesis: verum

end;

end;