theorem Th8: :: PYTHTRIP:8
for k, m, n being Element of NAT holds (k * m) gcd (k * n) = k * (m gcd n)