for k, n, m being Nat holds m lcm (n lcm k) = (m lcm n) lcm k