theorem :: COUNTERS:20

for N, M, K being ExtNat st M <= N holds
M * K <= N * K by XXREAL_3:71;