theorem :: COUNTERS:8

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