for k, m, n being Nat st n divides m & k divides m & n,k are_coprime holds
n * k divides m