for k, n, m being Nat holds
( ( n divides m & k divides m ) iff n lcm k divides m )