theorem Th8: :: PYTHTRIP:8

for k, m, n being Nat holds (k * m) gcd (k * n) = k * (m gcd n)