theorem LCM1: :: NEWTON03:6

for a, b being Integer holds
( a divides b iff a lcm b = |.b.| )