theorem Th24: :: NAT_D:24

for k, n being natural Number st k < n holds
k mod n = k