theorem :: WSIERP_1:30

for a, b, c being Nat st a gcd b = 1 & a divides b * c holds
a divides c by Th29;