for m, n being natural Ordinal st n <> {} holds
(m *^ n) div^ (m lcm n) divides m