let k, m, n be Nat; :: thesis: ( k divides n * m & n,k are_coprime implies k divides m )
assume that
A1: k divides n * m and
A2: n,k are_coprime ; :: thesis: k divides m
reconsider k = k, m = m, n = n as Element of NAT by ORDINAL1:def 12;
n gcd k = 1 by A2, INT_2:def 3;
then A3: (n * m) gcd (k * m) = m by EULER_1:5;
k divides k * m ;
hence k divides m by A1, A3, NEWTON:50; :: thesis: verum