for n, m being natural Ordinal holds
( m divides n iff n = m *^ (n div^ m) )