for n being Nat holds 0 div n = 0