theorem :: NEWTON03:71

for a, n being Nat
for b being non zero Nat holds a lcm (((n * a) + 1) * b) = ((n * a) + 1) * (a lcm b)