theorem :: COUNTERS:19

for N, M, K being ExtNat st K <> 0 & N = M * K holds
M <= N