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

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