theorem :: NAT_D:7

for i, j being natural Number st 0 < j & i divides j holds
i <= j by INT_2:27;