theorem :: NAT_2:4

for n being Nat holds n div 1 = n