for n, m being Nat holds m lcm n divides m * n