for a, n being non zero Nat holds (n div a) * a <= n