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;

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;