for k, m, n being Element of NAT st k gcd m = 1 holds
k gcd (m * n) = k gcd n