theorem :: NAT_2:3

for n being non zero Nat holds n div n = 1