for k, m, n being Integer st m gcd n = 1 & k gcd n = 1 holds
(m * k) gcd n = 1