theorem Th2: :: NAT_2:2

for n being Nat holds 0 div n = 0