theorem :: WSIERP_1:16

for a, b, d being Nat st d divides a & a gcd b = 1 holds
d gcd b = 1 by Th15, NEWTON:57;