theorem :: NAT_1:24

for i, j, h being natural Number st i <> 0 & h = j * i holds
j <= h