theorem Th27: :: NAT_D:27

for i, j being natural Number st i < j holds
i div j = 0