theorem :: NAT_2:2

for n being Nat holds 0 div n = 0 ;