theorem Th21: :: INT_2:21

for a, b being Integer holds a gcd b divides a by Def2;