theorem :: COUNTERS:19
for N, M, K being ExtNat st K <> 0 & N = M * K holds
M <= N