for k, l being Integer st k <> 0 holds
( k divides l iff l / k is Integer )