theorem Th2: :: FIB_NUM:2

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