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