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