let a, b, c be Nat; :: thesis: ( c divides a * b & a,c are_coprime implies c divides b )
assume that
A1: c divides a * b and
A2: a,c are_coprime ; :: thesis: c divides b
A3: c divides c * b by NAT_D:9;
a gcd c = 1 by A2, INT_2:def 3;
then (a * b) gcd (c * b) = b by Th5;
hence c divides b by A1, A3, NEWTON:50; :: thesis: verum